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.
Nous visons à combler le fossé entre les mondes discret et continu des méthodes formelles et de la théorie du contrôle. Nous élèverons le niveau d’abstraction au-dessus de celui que l’on trouve dans les techniques de pontage actuelles. Pour y parvenir, nous proposons de nous concentrer sur 5 objectifs de haut niveau :
- développer un modèle hybride formel ;
- démontrer les étapes de raffinement pour différents types d’exigences de contrôle ;
- proposer une méthode de conception rationnelle par étapes et soutenir les outils de BF ;
- valider la théorie/les modèles, en se basant sur des problèmes classiques du corpus des contrôleurs discrets ;
- valider le processus rationnel, en se basant sur des cas d’utilisation d’une gamme de domaines d’application.
