Automatic Generation of Observers from MARTE/CCSL

Frédéric Mallet 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, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The UML (Unified Modeling Language) Profile for Modeling and Analysis of Real-Time and Embedded (MARTE) systems promises a general modeling framework to design and analyze embedded systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. The Clock Constraint Specification Language (CCSL) has been defined in an annex of MARTE precisely to address semantic issues on time and causal aspects in relation with MARTE models. In the context of System-on-Chip design, some early work was proposed to use CCSL as a high-level specification language from which an observation network could be built. That observation network was used to observe early prototype implementations of the system under design and verify its compliance with respect to the CCSL specification. The proposed approach consisted in manually building a library of observer nodes for each CCSL operator and defining a generic mechanism to compose these nodes. This paper introduces a technique to generate a complete observer directly from a CCSL specification without requiring the manual construction of a library. The technique relies on a new state-based semantics given to a selected subset of CCSL operators. The study focuses specifically on boundedness issues with some CCSL operators that were previously artificially bounded to allow for exhaustive analyses.
Type de document :
Communication dans un congrès
RSP 2012 - International Symposium on Rapid System Prototyping, Oct 2012, Tampere, Finland. IEEE, 2012, <10.1109/RSP.2012.6380695>
Liste complète des métadonnées

https://hal.inria.fr/hal-00764066
Contributeur : Frédéric Mallet <>
Soumis le : mercredi 12 décembre 2012 - 11:41:49
Dernière modification le : mercredi 7 octobre 2015 - 01:15:03

Identifiants

Collections

Citation

Frédéric Mallet. Automatic Generation of Observers from MARTE/CCSL. RSP 2012 - International Symposium on Rapid System Prototyping, Oct 2012, Tampere, Finland. IEEE, 2012, <10.1109/RSP.2012.6380695>. <hal-00764066>

Partager

Métriques

Consultations de la notice

237