Analysis Support for TADL2 Timing Constraints on EAST-ADL Models

Arda Goknil 1 Jagadish Suryadevara 2 Marie-Agnès Peraldi-Frati 1 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
2 MDH - Mälardalen University College
Abstract : It is critical to analyze characteristics of real-time embedded systems, such as timing behavior, early in the development. In the automotive domain, EAST-ADL is a concrete example of the model-based approach for the architectural modeling of real-time systems. The Timing Augmented Description Language v2 (TADL2) allows for the specification of timing constraints on top of EAST-ADL models. In this paper we propose a formal validation & verification methodology for timing behaviors given with TADL2. The formal semantics of the timing constraints is given as a mapping to the Clock Constraint Specification Language (CCSL), a formal language that implements the MARTE Time Model. Based on such a mapping, the validation is carried out by the simulation of TADL2 specifications. The simulation allows for a rapid prototyping of TADL2 specifications. The verification is performed based on a TADL2 mapping to timed automata modeling using the UPPAAL model-checker. The whole process is illustrated on a Brake-By-Wire application.
Mots-clés : Automotive Executable Requirements Verification Timed Automata MARTE CCSL
Type de document :
Communication dans un congrès
Khalil Drira. ECSA 2013 - 7th European Conference on Software Architecture, Jul 2013, Montpellier, France. Springer, LNCS, 7957, pp.89-105, 2013, ECSA 2013: Software Architecture. 〈10.1007/978-3-642-39031-9_8〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00839963
Contributeur : Frédéric Mallet <>
Soumis le : lundi 1 juillet 2013 - 11:44:54
Dernière modification le : mardi 17 avril 2018 - 11:23:42

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | I3S | UNICE | UNIV-COTEDAZUR

Citation

Arda Goknil, Jagadish Suryadevara, Marie-Agnès Peraldi-Frati, Frédéric Mallet. Analysis Support for TADL2 Timing Constraints on EAST-ADL Models. Khalil Drira. ECSA 2013 - 7th European Conference on Software Architecture, Jul 2013, Montpellier, France. Springer, LNCS, 7957, pp.89-105, 2013, ECSA 2013: Software Architecture. 〈10.1007/978-3-642-39031-9_8〉. 〈hal-00839963〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

320

Contact


archive-ouverte@inria.fr