Skip to Main content Skip to Navigation
Conference papers

Verification of MARTE/CCSL Time Requirements in Promela/SPIN

Ling Yin 1 Frédéric Mallet 2 Jing Liu 1
1 Software Engineering Institute
Software Engineering Institute [Shangaï]
2 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 : The Clock Constraint Specification Language (CCSL) provides expressions and relations to specify the time requirements and causal dependencies of systems. It was initially proposed, in the context of MARTE: the UML profile for Modeling and Analysis of Real-Time and Embedded Systems. In this paper, we propose a method to verify CCSL specifications. We give a formal state-based interpretation of a fundamental subset of CCSL clock constraints. Based on it, we translate a CCSL specification into a Promela model and feed the result into the model checker SPIN. Then we show some patterns for expressing the properties of the model and do the verification. A digital filter application is used as an example to illustrate the approach.
Document type :
Conference papers
Complete list of metadata
Contributor : Frédéric Mallet Connect in order to contact the contributor
Submitted on : Sunday, December 11, 2011 - 6:23:40 PM
Last modification on : Friday, January 21, 2022 - 3:15:45 AM




Ling Yin, Frédéric Mallet, Jing Liu. Verification of MARTE/CCSL Time Requirements in Promela/SPIN. IEEE ICECCS 2011 - 16th IEEE International Conference on Engineering of Complex Computer Systems, Apr 2011, Las Vegas, United States. ⟨10.1109/ICECCS.2011.14⟩. ⟨hal-00650621⟩



Les métriques sont temporairement indisponibles