ANR has selected the project DISCONT (Correct Integration of DIScrete and CONTinous models) under the framework “appel à projets générique 2017”.
- DURATION : 42 months
- PARTNERS: LORIA (leader), IRIT, CLEARSY, LACL, TSP-SAMOVAR
DISCONT aims to provide efficient and easy to use refinement and proof-based techniques and tools that scale to complex systems and offer more convenient and automatic proof platforms centered around B and Event-B, with Atelier-B and Rodin. The main theoretical challenge is in how to better formalize the verification of the transition from the real to the discrete models, using refinement. The main technical challenge is in how best to extend/integrate existing tools in order to better support the CPS engineers in the formal development process.
We aim to bridge the gap between the discrete and continuous worlds of formal methods and control theory. We will lift the level of abstraction above that which is found in current bridging techniques. In order to achieve this, we propose to focus on 5 high-level objectives:
- develop a formal hybrid model;
- demonstrate refinement steps for different types of control requirements;
- propose a rational step-wise design method and support bf tools;
- validate the theory/models, based on classic problems from the discrete controller corpus;
- validate the rational process, based on use cases from a range of application domains.
