title = { A {SystemC}/{TLM} semantics in {Promela} and its possible applications },
    author = {Traulsen, Claus and Cornet, J\'er\^ome and Moy, Matthieu and Maraninchi, Florence},
    month = {July},
    year = {2007},
    booktitle = {14th Workshop on Model Checking Software SPIN},
    team = {SYNC},
    abstract = {{SystemC} has become a de-facto standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called transaction level (TL). Verifying properties of a TL model requires that {SystemC} be translated into some formally defined language for which there exist verification back-ends. Since {SystemC} has no formal semantics, this includes a careful encoding of the {SystemC} scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we described LusSy a complete chain from {SystemC} to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the {SystemC} scheduler into a asynchronous formalism, namely Promela (the input language for {Spin}). We comment on the possible uses of this new encoding, and compare it with the synchronous encoding.},


Publication Sections

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 778506