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 :
Rapport
[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

https://hal.inria.fr/hal-00667849
Contributeur : Team Aoste <>
Soumis le : mercredi 8 février 2012 - 14:56:00
Dernière modification le : jeudi 11 janvier 2018 - 16:04:48
Document(s) archivé(s) le : mercredi 9 mai 2012 - 02:40:09

Fichier

RR-7491.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00667849, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

362

Téléchargements de fichiers

262