Model-checking and formal modeling are now techniques with a certain academic recognition, but their applicability in practice remain somewhat inferior to expectations. This is in part due to two main problems: rather rigid modeling of the systems impairing abstraction and scalability, and insufficient feedback from the verification process. In this project, we address these issues by lifting these techniques to the more flexible and rich setting of parametrised formal models.
In that setting, some features of the system like the number of processes, the size of some buffers, communication delays, deadlines, energy consumption, and so on, may be not numerical constants, but rather unknown parameters. The model-checking questions then become more interesting: is some property true for all values of the parameters? Or does there exist some value such that it is? Or even what are all the possible values such that it is?
Building on the skills of the consortium on topics like regular model-checking, timed systems, probabilistic systems, and our previous contributions in model-checking of systems with a parametrised number of processes and parametrised timed systems, including the development of software tool prototypes, we develop in this project new models, techniques, and tools to extend the applicability of parameters in formal methods.
To achieve this objective, we study parameters in the context of discrete and timed/hybrid systems, both of them possibly augmented with quantitative information relating to costs (e.g. energy consumption), and probabilities. This gives the following six tasks:
- Discrete parameters
- Timing parameters
- Discrete and timing parameters
- Parameters in cost-based models
- Parameters in discrete models with probabilities
- Parameters in timed models with probabilities
Parametrised models are of obvious interest but the associated theoretical problems are hard. For instance, in the model of parametric timed automata, the basic model for timed systems with time parameters, the mere existence of a parameter value such that the system can reach some given state, is generally undecidable, even with only one parameter.
As a consequence, in all these tasks, we follow a common methodology, acknowledging these difficulties, and consisting in formalising the problem, studying decidable subclasses and designing efficient algorithms for the the parametrised model-checking problems (including in particular parameter synthesis), building efficient semi-algorithms for the general class that behave well in realistic cases, and finally implement the techniques in tool prototypes.
This raises many challenging and original problems like extending regular model-checking to graphs to model parametrised systems with an arbitrary topology, using infinite-state automata to represent sets of configurations, finding useful decidable classes of parametrised timed/hybrid systems or properties, provide techniques for approximate synthesis of parameter values, study models with parametrised costs, study probabilistic parametric models, and extend statistical verification techniques to parametric systems.
Beyond the classical application fields of formal methods (e.g. embedded systems), we envision new applications domains like smart homes, where parameters may account for the specifics of the residents. In that setting, cost-based parametrised models are particularly interesting for a focus on optimising energy consumption.
- Project end (maximal date)
- Project meeting #4 / AFSEC day in Paris 7
- SynCoP 2016 in Eindhoven, The Netherlands
- Project meeting #3 in Nantes
- SynCoP 2015 in London, UK
- Project meeting #2 in Paris 7
- Project meeting #1 in Paris 13
- Project start
|LIPN (Paris 13)||IRCCyN (Nantes)||IRIF (Paris 7)||LINA (Nantes)||Aalborg|
|Étienne André||Nicolas David||Peter Habermehl||Benoît Delahaye||Kim G. Larsen|
|Nguyễn Hoàng Gia||Loïg Jézéquel||Prateek Karandikar||Yrvann Emzivat||Jiří Srba|
|Laure Petrucci||Didier Lime||Arnaud Sangnier||Claude Jard|
|Tayssir Touili||Olivier H. Roux|
|[DSJ16]||Benoît Delahaye, Jiří Srba and Loïg Jezequel: Proceedings of the 3rd International Workshop on the Synthesis of Complex Parameters (SynCoP 2016). EPTCS.|
|[BHJL16]||Béatrice Bérard, Serge Haddad, Aleksandra Jovanović and Didier Lime: Interrupt Timed Automata with Auxiliary Clocks and Parameters. Fundamenta Informaticae, IOS Press, volume 143:3–4, pages 235–239.|
|[DLP16]||Benoît Delahaye, Didier Lime and Laure Petrucci: Parameter Synthesis for Parametric Interval Markov Chains. Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS volume 9583, pages 372–390.|
|[AKPP16]||Étienne André, Michał Knapik, Wojciech Penczek and Laure Petrucci: Controlling Actions and Time in Parametric Timed Automata. Proceedings of the 16th International Conference on Application of Concurrency to System Design (ACSD), IEEE, to appear.|
|[AG15]||Étienne André and Goran Frehse: Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters (SynCoP 2015). Volume 44 of OASIcs, Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH.||[PDF]|
|[JLR15]||Aleksandra Jovanović, Didier Lime and Olivier H. Roux: Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering (TSE), IEEE Computer Society Press, volume 41:5, pages 445–461.|
|[DJLR15]||Nicolas David, Claude Jard, Didier Lime and Olivier H. Roux: Discrete Parameters in Petri Nets. In proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2015), Springer LNCS volume 9115, pages 137–156.|
|[ACN15]||Étienne André, Camille Coti and Nguyễn Hoàng Gia: Enhanced Distributed Behavioral Cartography of Parametric Timed Automata. ICFEM’15, Springer LNCS 9407, pages 319–335.||[PDF]|
|[ACR15]||Étienne André, Thomas Chatain and César Rodríguez: Preserving Partial Order Runs in Parametric Time Petri Nets. ACSD’15, IEEE, pages 120–129.||[PDF]|
|[ALNS15]||Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng: Reachability Preservation Based Parameter Synthesis for Timed Automata. NFM’15, LNCS 9058, Springer, pages 50–65.||[PDF]|
|[ALR15]||Étienne André, Didier Lime and Olivier H. Roux: Integer-Complete Synthesis for Bounded Parametric Timed Automata. RP’15, LNCS 9328, Springer, pages 7–19.||[PDF]|
|[AM15]||Étienne André and Nicolas Markey: Language Preservation Problems in Parametric Timed Automata. FORMATS’15, Springer LNCS 9268, pages 27–43.||[PDF]|
|[And16]||Étienne André: What’s decidable about parametric timed automata?. FTSCS’15, Springer CCIS 596, pages 1–17.||[PDF]|
|[AP15]||Étienne André and Laure Petrucci: Unifying Patterns for Modelling Timed Relationships in Systems and Properties. PNSE’15, CEUR-WS volume 1372, pages 25–40.||[PDF]|
|[Del15]||Benoît Delahaye: Consistency for Parametric Interval Markov Chains. In the proceedings of the 2nd International Workshop on Synthesis of Complex Parameters (SynCoP 2015), volume 44 of OASIcs, pages 17–32.||[PDF]|
|[SAL15]||Sun Youcheng, Étienne André and Giuseppe Lipari: Verification of Two Real-Time Systems Using Parametric Timed Automata. In the informal proceedings of WATERS’15.||[PDF]|
|[ALSD14]||Étienne André, Liu Yang, Sun Jun and Dong Jin Song: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. Real-Time Systems Journal 50(5–6), pages 620–679.||[PDF]|