@inproceedings{MMJ11,
title = { {E}fficient {E}ncoding of {S}ystem{C}/{TLM} in {P}romela },
author = {Marquet, Kevin and Moy, Matthieu and Jeannet, Bertrand},
month = {03},
year = {2011},
booktitle = {{DATICS}-{IMECS}},
address = {{H}ong-{K}ong},
team = {SYNC},
hal_id = {hal-00557515},
keywords = {{S}ystem{C}, {T}ransaction-{L}evel {M}odeling, {P}romela, {S}pin, {M}odel-checking},
collaboration = {{P}rojet {M}inalogic {O}pen{TLM}},
day = {16},
abstract = {{T}o deal with the ever growing complexity of {S}ystems-on-{C}hip, designers use models early in the design flow. {S}ystem{C} is a commonly used tool to write such models. {I}n order to verify these models, one thriving approach is to encode its semantics into a formal language, and then to verify it with verification tools. {V}arious encodings of {S}ystem{C} into formal languages have already been proposed, with different performance implications. {I}n this paper, we investigate a new, automatic, asynchronous means to formalize models. {O}ur encoding supports the subset of the concurrency and communication constructs offered by {S}ystem{C} used for high-level modeling. {W}e increase the confidence in the fact that encoded programs have the same semantics as the original one by model-checking a set of properties. {W}e give experimental results on our formalization and compare with previous works.},
}
