Correctness Issues on MARTE/CCSL constraints

Frédéric Mallet 1 Robert De Simone 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 : The UML Profile for Modeling and Analysis of Real-Time and Embedded systems promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on available verification techniques. The Clock Constraint Specification Language (CCSL), first introduced as a companion language for MARTE, was devised to offer a formal support to conduct causal and temporal analysis on MARTE models. This work relies on a state-based semantics for CCSL to establish correctness properties on MARTE/CCSL specifications. We propose and compare two different techniques to build the state-space of a specification. One is an extension of some previous work and is based on extended finite state machines. It relies on integer linear programming to solve the constraints and reduce the state-space. The other one is based on an intentional representation and uses pure Boolean abstractions but offers no guarantee to terminate when the specification is not safe. The approach is illustrated on one simple example where the architecture plays an important role. We describe a process where the logical description of the application is progressively refined to take into account the execution platform through allocation.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2015, 106, pp.78-92. 〈10.1016/j.scico.2015.03.001〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger
Contributeur : Frédéric Mallet <>
Soumis le : mardi 19 janvier 2016 - 14:06:34
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : mercredi 20 avril 2016 - 10:30:10


Fichiers produits par l'(les) auteur(s)




Frédéric Mallet, Robert De Simone. Correctness Issues on MARTE/CCSL constraints. Science of Computer Programming, Elsevier, 2015, 106, pp.78-92. 〈10.1016/j.scico.2015.03.001〉. 〈hal-01257978〉



Consultations de la notice


Téléchargements de fichiers