Towards SMV model checking of signal (multi-clocked) specifications

Julio C. Peralta 1 Thierry Gautier 1
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Signal is a high-level data-flow specification language that equally allows multi-clocked descriptions as well as single-clocked ones. It has a formal semantics and is supported by several formal tools for simulation and static validation. This generality renders it useful for various specification, simulation, and verification tasks in embedded system design. SMV, in turn, is a language and model checker where synchronous models are single-clocked by definition. Roughly, we use standard techniques to describe clocks by Boolean variables, with the advantage that the number of such variables is kept to a minimum through a static analysis provided by the Signal compiler. In particular, we propose a translation from possibly multi-clocked Signal specifications into SMV specifications for their corresponding verification by model checking.
Type de document :
Communication dans un congrès
Ninth International Workshop on Automated Verification of Critical Systems, Sep 2009, Swansea, United Kingdom. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00788406
Contributeur : Ist Rennes <>
Soumis le : jeudi 14 février 2013 - 13:46:30
Dernière modification le : jeudi 11 janvier 2018 - 06:20:09

Identifiants

  • HAL Id : hal-00788406, version 1

Collections

Citation

Julio C. Peralta, Thierry Gautier. Towards SMV model checking of signal (multi-clocked) specifications. Ninth International Workshop on Automated Verification of Critical Systems, Sep 2009, Swansea, United Kingdom. 2009. 〈hal-00788406〉

Partager

Métriques

Consultations de la notice

139