A tour of MARTE/CCSL: usage, simulation and verification

Frédéric Mallet
Université Nice Sophia Antipolis
Friday, 21 February, 2014 - 14:00
Forum E

In the development of safety-critical embedded systems, the ability to
formally analyze system behavior models, based on timing and causality, helps
the designer to get insight into the systems overall timing behavior. To support the
design and analysis of real-time embedded systems, the UML modeling profile
for MARTE provides CCSL – a time model and a clock constraint specification language.
CCSL is an expressive language that supports specification of both logical
and chronometric constraints for MARTE models. On the other hand, semantic
frameworks such as timed automata provide verification support for real-time systems.
To address the challenge of verifying CCSL-based behavior models, we have proposed a
technique for transforming MARTE/CCSL mode behaviors
into Timed Automata for model-checking using the UPPAAL tool. This enables
verification of both logical and chronometric properties of the system, which has
not been possible before.