Improving the Efficiency of Synchronized Product with Infinite Transition Systems

Yuliia Romenska 1 Frédéric Mallet 1, *
* Auteur correspondant
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 : Embedded System Design is becoming a field of choice for Model-Driven Engineering techniques. On the engineering side, models bring an abstraction of the code that can then be generated (and regenerated) at will. On the semantic side, they bring a reasoning framework to guarantee or verify properties on the generated code. We focus here on the Clock Constraint Specification Language, initially defined as a companion language of the uml Profile for marte. More specifically, we propose a state-based data-structure inspired by lazy evaluation technique to represent the unbounded ccsl operators. Lazy evaluation allows for an intentional representation of infinite transition systems. We provide an algorithm to compute the synchronized product of such transition systems. Even though the transition systems are infinite, the result of the composition may become finite, in which case the (semi)algorithm terminates and exhaustive analysis becomes possible. We also study the time complexity and show that it is exponential in the number of clocks. We then explore several solutions where this worst-case estimation is not attained and where analyses have a much better complexity in practice.
Type de document :
Chapitre d'ouvrage
Ermolayev, Vadim and Mayr, Heinrich C. Communications in Computer and Information Science, 412, Springer, pp.287-307, 2013, Communications in Computer and Information Science, 978-3-319-03997-8. 〈10.1007/978-3-319-03998-5_15〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00926299
Contributeur : Frédéric Mallet <>
Soumis le : jeudi 9 janvier 2014 - 13:52:16
Dernière modification le : vendredi 25 mai 2018 - 12:02:04

Identifiants

Collections

INRIA | I3S | UNICE | UNIV-COTEDAZUR

Citation

Yuliia Romenska, Frédéric Mallet. Improving the Efficiency of Synchronized Product with Infinite Transition Systems. Ermolayev, Vadim and Mayr, Heinrich C. Communications in Computer and Information Science, 412, Springer, pp.287-307, 2013, Communications in Computer and Information Science, 978-3-319-03997-8. 〈10.1007/978-3-319-03998-5_15〉. 〈hal-00926299〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

257

Contact


archive-ouverte@inria.fr