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.},


Sections de Publications

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876679