DISCONT

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 :

  1. développer un modèle hybride formel ;
  2. démontrer les étapes de raffinement pour différents types d’exigences de contrôle ;
  3. proposer une méthode de conception rationnelle par étapes et soutenir les outils de BF ;
  4. valider la théorie/les modèles, en se basant sur des problèmes classiques du corpus des contrôleurs discrets ;
  5. valider le processus rationnel, en se basant sur des cas d’utilisation d’une gamme de domaines d’application.

Besoin d'un système sur-mesure ?

Nous sommes des créateurs de logiciels et de systèmes sécuritaires. Conçus et fabriqués en France. Contactez-nous et discutons ensemble de votre projet !