2007.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib matthieu_moy.bib -c year=2007 -ob 2007.bib}}

@inproceedings{systemc-to-spin,
  author = {Claus Traulsen and J\'er\^ome Cornet and Matthieu Moy and Florence Maraninchi},
  title = {A {SystemC}/{TLM} semantics in {Promela} and its possible applications},
  booktitle = {14th Workshop on Model Checking Software SPIN},
  year = 2007,
  month = {July},
  url = {http://www-verimag.imag.fr/~moy/publications/MicMacToSpin.pdf},
  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.}
}

This file was generated by bibtex2html 1.98.