Skip to Main content Skip to Navigation

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, Laboratoire I3S - 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.
Document type :
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Team Kairos Connect in order to contact the contributor
Submitted on : Wednesday, February 8, 2012 - 2:56:00 PM
Last modification on : Friday, January 21, 2022 - 3:18:04 AM
Long-term archiving on: : Wednesday, May 9, 2012 - 2:40:09 AM


Files produced by the author(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⟩



Les métriques sont temporairement indisponibles