About PACS
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.
News
- 1/10/2019
- Project end
- 6-7/04/2019
- SynCoP 2019 in Prag, Czech Republic
- 11/02/2019
- Project meeting #9 in Nantes
- 28/08/2018
- Project meeting #8 in Paris 13
- 14-15/04/2018
- SynCoP 2018 in Thessaloniki, Greece
- 03/04/2018
- Project meeting #7 in Paris 7
- 30/08/2017
- Project meeting #6 in Paris 7
- 06/2017
- Tutorial at Petri Nets 2017
- 22-23/04/2017
- SynCoP 2017 in Uppsala, Sweden
- 13/03/2017
- Project meeting #5 in Nantes
- 01/03/2017
- We are very glad to hire Louis Fippo-Fitime as a post-doc at LIPN
- 04/10/2016
- ANR review
- 19/10/2016
- Presentation of the CoPaS project by Benoît Delahaye [video]
- 26/09/2016
- Video-meeting in Paris 13 / LINA
- 7/09/2016
- Video-meeting in Paris 13 / LINA
- 21/06/2016
- Tutorial at Petri Nets 2016 (videos of session 1, documents for practical session 2, videos of session 3)
- 26/05/2016
- Project meeting #4 / AFSEC workshop day in Paris 7
- 3/04/2016
- SynCoP 2016 in Eindhoven, The Netherlands
- 16/10/2015
- Project meeting #3 in Nantes
- 11/04/2015
- SynCoP 2015 in London, UK
- 27/03/2015
- Project meeting #2 in Paris 7
- 6/10/2014
- Project meeting #1 in Paris 13
- 1/10/2014
- Project start
Partners
| LIPN (Paris 13) | LS2N (IRCCyN) (Nantes) | IRIF (Paris 7) | LS2N (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 | |||
| Mathias Ramparison | ||||
| Louis Fippo-Fitime |