Verification of MARTE/CCSL Time Requirements in Promela/SPIN - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Verification of MARTE/CCSL Time Requirements in Promela/SPIN

(1) , (2) , (1)
1
2

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.
Not file

Dates and versions

hal-00650621 , version 1 (11-12-2011)

Identifiers

Cite

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⟩
175 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More