ANR a sélectionné le projet DISCONT (Correct Integration of DIScrete and CONTinous models) dans la cadre de l’appel à projets générique 2017.
- DURÉE : 42 mois
- PARTENAIRES: LORIA (leader), IRIT, CLEARSY, LACL, TSP-SAMOVAR
DISCONT vise à fournir des techniques et des outils de raffinement et de preuve efficaces et faciles à utiliser, qui s’adaptent aux systèmes complexes et offrent des plates-formes de preuve plus pratiques et automatiques centrées sur B et Event-B, avec Atelier-B et Rodin. Le principal défi théorique consiste à mieux formaliser la vérification de la transition entre les modèles réels et les modèles discrets, en utilisant le raffinement. Le principal défi technique est de savoir comment étendre/intégrer au mieux les outils existants afin de mieux soutenir les ingénieurs CPS dans le processus de développement formel.