Correct Transformation from CCSL to Promela for verification

Frédéric Mallet 1 Ling Yin 1
1 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Transforming a specification language into a language supported by a verification tool is a widely adopted way of doing formal verification. It enables the reuse of existing languages and tools. In this paper, we propose a correct transformation from CCSL to Promela to do formal verification by SPIN. To implement the transformation, we introduce "coincident instant" into Promela to deal with the discrete time in CCSL. Then we define property patterns to ensure that correctness properties are verified "coincident instant" by "coincident instant" during the verification. We define checkpoint transition systems (CTSs) to model source CCSL specifications and transformed Promel models. The proof of the correctness of our transformation relies on the checkpoint bisimulation defined over CTS. If a property is satisfied by a transformed Promela model, then it is satisfied by the source CCSL specification.
Type de document :
[Research Report] RR-7491, INRIA. 2012, pp.33
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
Contributeur : Team Kairos <>
Soumis le : mercredi 8 février 2012 - 14:56:00
Dernière modification le : vendredi 25 mai 2018 - 12:02:04
Document(s) archivé(s) le : mercredi 9 mai 2012 - 02:40:09


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00667849, version 1


Frédéric Mallet, Ling Yin. Correct Transformation from CCSL to Promela for verification. [Research Report] RR-7491, INRIA. 2012, pp.33. 〈hal-00667849〉



Consultations de la notice


Téléchargements de fichiers