ANR ImpRo Workshop

As we are approaching the end of the project, an open workshop is organized at LIP6 the 18th of June 2014, co-located with the annual meeting of the CNRS work groups "GT Verif (GDR IM)" and "GT Forwal (GDR GPL)". All contributions are welcome (CFP in french) and more information is available on the dedicated page.

News

18/06/2014	ImpRo Open Workshop at LIP6
06/12/2013	Review of the project at ANR + preparatory meeting at LIP6
09/04/2013	Annual plenary meeting at LIP6
23/10/2012	"Probabilities" meeting at ENS Cachan
19/10/2012	"Concurrency" meeting at IRCCyN
29/03/2012	Annual 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/2011	Project kick-off at IRCCyN
01/03/2011	Project start

Short description

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)

Partners and participants

IRCCyN (Nantes)

IRISA (Rennes)

LIP6 (Paris)

LSV (Cachan)

LIAFA (Paris)

LIF (Marseille)

Didier Lime

Rouwaida Abdallah

Loïc Helouët

Akshay Sundararaman

Béatrice Bérard

Nathalie (Tali) Sznajder

Serge Haddad

Arnaud Sangnier

Pierre-Alain Reynier

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]
[D22]	Jean-Luc Béchennec, Sébastien Faucou, Richard Urunuela. Spécifications du démonstrateur. 2012	[PDF]
[D23]	Jean-Luc Béchennec, Sébastien Faucou, Richard Urunuela, Armel Mangean, Benjamin Sientzoff. Implémentation du démonstrateur. 2014	[PDF]
[D31]	Béatrice Bérard, Patricia Bouyer, Kim G. Larsen, Nicolas Markey, John Mullins, Ocan Sankur, Mathieu Sassolas, and Claus Thrane. Measuring the robustness. 2013	[PDF]
[D32]	Pierre-Alain Reynier. Measuring Robustness with Probabilities. 2014	[PDF]
[D41]	Sandie Balaguer, Thomas Chatain and Stefan Haar. Concurrent semantics of timed distributed systems. 2012	[PDF]
[D42]	S. Akshay, Loïc Hélouët, Claude Jard, Pierre-Alain Reynier, Didier Lime, and Olivier H. Roux. Concurrent behaviors with architectural constraints or imperfect clocks. 2013	[PDF]
[D43]	Loïc Hélouët. Robustness in scenarios. 2014	[PDF]
[D51]	Patricia Bouyer, Sébastien Faucou, Stefan Haar, Aleksandra Jovanović, Didier Lime, Nicolas Markey, Olivier H. Roux and Ocan Sankur. Control tasks for Timed System; Robustness issues. 2013	[PDF]
[D53]	N. Bertrand, É. Fabre, S. Haar, S. Haddad, L. Hélouët, E. Lefaucheux. Supervision and Probabilities. 2014	[PDF]

Publications

[BMS14]	Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robust Reachability in Timed Automata and Games: A Game-based Approach. In Theoretical Computer Science, 2014. Elsevier.	[PDF]
[BHL14]	N. Bertrand, S. Haddad and E. Lefaucheux. Foundation of Diagnosis and Predictability in Probabilistic Systems. In FSTTCS'14, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2014.	[PDF]
[JLR14b]	Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer Parameter Synthesis for Real-Time Systems. In IEEE Transactions on Software Engineering, 2014. IEEE Computer Society Press.	[PDF]
[JLR14a]	Didier Lime (with Aleksandra Jovanović and Olivier H. Roux), Integer Parameter Synthesis for Timed Automata. Invited talk at SynCoP'14. April 2014, Grenoble, France. Volume 145 of EPTCS
[SBM14]	Ocan Sankur, Patricia Bouyer et Nicolas Markey. Shrinking Timed Automata. In Information and Computation 234, pages 107-132, 2014.	[PDF]
[ORS14]	Youssouf Oualhadj, Pierre-Alain Reynier and Ocan Sankur. Probabilistic Robust Timed Games. In CONCUR'14, LNCS 8704, pages 203-217, Springer 2014.	[PDF]
[BFH+14]	N. Bertrand, É. Fabre, S. Haar, S. Haddad and L. Hélouët. Active diagnosis for probabilistic systems. In FoSSaCS'14, LNCS 8412, pages 29-42. Springer, 2014	[PDF]
[LMR13]	Didier Lime, Claude Martinez and Olivier H. Roux. Shrinking of time Petri nets. In Journal of Discrete Event Dynamic Systems - Theory and Applications (jDEDS), 23(4):419-438, 2013. Springer	[PDF]
[ABHH13]	S. Akshay, N. Bertrand, S. Haddad and L. Hélouët. The steady-state control problem for Markov decision processes. In QEST'13, pages 290-304. IEEE Computer Society Press, 2013.	[PDF]
[AHJ13]	Rouweida Abdallah, Loïc Hélouët and Claude Jard. Distributed Implementation of Message Sequence Charts. Software and System Modeling journal (SoSyM), 2013.	[PDF]
[SCH13]	Sandie Balaguer, Thomas Chatain and Stefan Haar. Building Occurrence Nets from Reveals Relations. Fundamenta Informaticae 123(3), pages 245-272, 2013.	[PDF]
[BHJL13]	Béatrice Bérard, Serge Haddad, Aleksandra Jovanović and Didier Lime. Parametric Interrupt Timed Automata In RP'13, LNCS 8169, pages 59-69, Springer 2013.	[PDF]
[CJ13]	Thomas Chatain and Claude Jard. Back in Time Petri Nets. In FORMATS'13, LNCS 8053, pages 91-105, Springer 2013.	[PDF]
[HHMS13]	Stefan Haar, Serge Haddad, Tarek Melliti, Stefan Schwoon. Optimal Constructions for Active Diagnosis. In FSTTCS'13, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2013.	[PDF]
[JLR13b]	Aleksandra Jovanovic, Didier Lime and Olivier H. Roux. Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games. In ATVA'13. LNCS 8172, pages 87-101, Springer, 2013.	[PDF]
[JLR13a]	Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer Parameter Synthesis for Timed Automata. In TACAS'13, LNCS 7795, pages 403-417, Springer 2012.	[PDF]
[SBMR13]	Ocan Sankur, Patricia Bouyer, Nicolas Markey et Pierre-Alain Reynier. Robust Controller Synthesis in Timed Automata. In CONCUR'13, LNCS 8052, pages 546-560. Springer, 2013	[PDF]
[AGHY13]	S. Akshay, Blaise Genest, Loïc Hélouët, Shaofa Yang. Symbolically bounding the drift in time-constrained MSC graphs. In ICTAC'12, LNCS 7521, pages 1-15, Springer 2012.	[PDF]
[CH13]	Thomas Chatain and Stefan Haar. A Canonical Contraction for Safe Petri Nets. In PNSE'13, CEUR Workshop Proceedings 969, pages 25-39. 2013.	[PDF]
[BMS13b]	Patricia Bouyer, Nicolas Markey and Ocan Sankur. Robustness in timed automata. Invited paper. In RP'13, LNCS 8169, pages 1-18. Springer, 2013.	[PDF]
[BMS13a]	Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robust Weighted Timed Automata and Games. In FORMATS'13, LNCS 8053, pages 31-46. Springer, 2013.	[PDF]
[FH13]	E. Fraca and S. Haddad. Complexity Analysis of Continuous Petri Nets. In ICATPN'13, LNCS 7927, pages 170-189. Springer, 2013.	[PDF]
[San13]	Ocan Sankur. Shrinktech: A Tool for the Robustness Analysis of Timed Automata. In CAV'13, LNCS 8044, pages 1006-1012. Springer, 2013.	[PDF]
[CBKT13]	Maximilien Colange, Souheib Baarir, Fabrice Kordon and Yann Thierry-Mieg. Towards Distributed Software Model-Checking Using Decision Diagrams. In CAV'13, LNCS 8044, pages 1006-1012. Springer, 2013.	[PDF]
[BBJM12]	Patricia Bouyer, Thomas Brihaye, Marcin Jurdziński et Quentin Menet. Almost-Sure Model-Checking of Reactive Timed Automata. In QEST'12, pages 138-147. IEEE Computer Society Press, 2012.	[PDF]
[JFLR12]	Aleksandra Jovanović, Sébastien Faucou, Didier Lime, and Olivier H. Roux. Real-Time Control with Parametric Timed Reachability Games. In WODES'12, IFAC 2012.	[PDF]
[AHJR12]	S Akshay, Loïc Hélouët, Claude Jard, Pierre-Alain Reynier. Robustness of time Petri nets under guard enlargement. In RP'12, LNCS 7550, pages 92-106, Springer 2012.	[PDF]
[AHJ+12]	S Akshay, Loïc Hélouët, Claude Jard, Didier Lime and Olivier H. Roux. Robustness of Time Petri Nets under Architectural Constraints. In FORMATS'12, LNCS 7595, pages 11-26, Springer 2012.	[PDF]
[BHSS12]	Béatrice Bérard, Serge Haddad, Mathieu Sassolas and Nathalie Sznajder. Concurrent Games on VASS with Inhibition In CONCUR'12, LNCS 7454, pages 39-52, Springer 2012.	[PDF]
[BCH12b]	Sandie Balaguer and Thomas Chatain. Avoiding Shared Clocks in Networks of Timed Automata. In CONCUR'12, LNCS 7454, Springer 2012.	[PDF]
[BMS12]	Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robust Reachability in Timed Automata: A Game-based Approach. In ICALP'12, LNCS 7392, pages 128-140. Springer, 2012.	[PDF]
[BCH12a]	Sandie Balaguer, Thomas Chatain and Stefan Haar. A Concurrency Preserving Translation from Time Petri Nets to Networks of Timed Automata. In Formal Methods in System Design 40(3):330-355, Kluwer Academic Publishers, 2012.	[PDF]
[AJ11]	Rouweida Abdallah and Claude Jard. An Experiment in Automatic Generation of Protocols from HMSCs. In NOTERE'11, pp. 1-8, 2011.
[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]