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.