Implementability and Robustness of Timed Systems (ImpRo)

a

News

29/03/2012Annual plenary meeting at IRCCyN
03/11/2011"Concurrency" meeting at LSV
07/10/2011"Concurrency" meeting at IRISA
19/09/2011"Pobabilities and Robustness" meeting at LIAFA (room 6A92)
28/06/2011"General Framework 2" meeting at LSV
30/05/2011"Diagnostic" meeting at LIP6 (room 26-00/332)
17/05/2011"Concurrency issues" meeting at LSV
14/04/2011"General Framework" meeting at LSV
14/03/2011Project kick-off at IRCCyN
01/03/2011Project start
a

Short description

Logo ANR

ImpRo is an academic research project funded by the French national research agency, within its non-thematic ("Blanc") program.

Keywords:Formal models, time, implementability, robustness, semantics, timed automata, time Petri nets
Abstract:This project addresses the issues related to the practical implementation of formal models for the design of communicating embedded systems: such models abstract many complex features or limitations of the execution environment. The modeling of time, in particular, is usually ideal, with infinitely precise clocks, instantaneous tests or mode commutations, etc. Our objective is thus to study to what extent the practical implementation of these models preserves their good properties. We will first define a generic mathematical framework to reason about and measure implementability, and then study the possibility to integrate implementability constraints in the models. We will particularly focus on the combination of several sources of perturbation such as resource allocation, the distributed architecture of applications, etc. We will also study implementability through control and diagnostic techniques. We will finally apply the developed methods to a case study based on the AUTOSAR architecture, a standard of the automotive industry.
Partners (administrative list):IRCCyN (Nantes), IRISA (Rennes), LIP6 (Paris), LSV (Cachan)
Additional Partners:LIAFA (Paris), LIF (Marseilles)
Coordinator:Didier Lime (IRCCyN)
a

Partners and participants

IRCCyN (Nantes)IRISA (Rennes)LIP6 (Paris)LSV (Cachan)LIAFA (Paris)LIF (Marseille)
Franck Cassez
Sébastien Faucou
Aleksandra Jovanovic
Didier Lime
Olivier H. Roux
Charlotte Seidner
Rouwaida Abdallah
Loïc Helouët
Claude Jard
Akshay Sundararaman
Souheib Baarir
Béatrice Bérard
Fabrice Kordon
Yann Thierry-Mieg
Denis Poitrenaud
Mathieu Sassolas
Nathalie (Tali) Sznajder
Sandie Balaguer
Patricia Bouyer
Thomas Chatain
Stefan Haar
Serge Haddad
Nicolas Markey
Ocan Sankur
Stefan Schwoon
François Laroussinie
Arnaud Sangnier
Rémi Jaubert
Pierre-Alain Reynier
a

Deliverables

[D21] S. Akshay, B. Bérard, P. Bouyer, S. Haar, S. Haddad, C. Jard, D. Lime, N. Markey, P.-A. Reynier, O. Sankur, Y. Thierry-Mieg. Overview of Robustness in Timed Systems. 2012 [PDF]
a

Publications

[BBBS11] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye et Amélie Stainer. Emptiness and Universality Problems in Timed Automata with Positive Frequency. In ICALP'11, LNCS 6756, pages 246-257. Springer, 2011. [PDF]
[BMS11] Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robust Model-Checking of Timed Automata via Pumping in Channel Machines. In FORMATS'11, LNCS 6919, pages 97-112. Springer, 2011. [PDF]
[BLM+11]Patricia Bouyer, Kim G. Larsen, Nicolas Markey, Ocan Sankur et Claus Thrane. Timed automata can always be made implementable. In CONCUR'11, LNCS 6901, pages 76-91. Springer, 2011. [PDF]
[SBM11]Ocan Sankur, Patricia Bouyer et Nicolas Markey. Shrinking Timed Automata. In FSTTCS'11, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2011. [PDF]
[Mar11]Nicolas Markey. Robustness in Real-time Systems. In SIES'11, pages 28-34. IEEE Computer Society Press, 2011. [PDF]
[San11]Ocan Sankur. Untimed Language Preservation in Timed Systems. In MFCS'11, LNCS 6907, pages 556-567. Springer, 2011. [PDF]