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 :
Reports
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00667849
Contributor : Team Kairos <>
Submitted on : Wednesday, February 8, 2012 - 2:56:00 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Long-term archiving on : Wednesday, May 9, 2012 - 2:40:09 AM

File

RR-7491.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00667849, version 1

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⟩

Share

Metrics

Record views

557

Files downloads

418