Intégration correcte de modèles discrets et continus – DISCONT

Les systèmes cyber-physiques (CPS) interconnectent le monde réel au travers de réseaux de capteurs et d’actionneurs: des composants physiques et logiques (calculatoires) interagissent selon différentes voies, dépendant du contexte selon des échelles spatiales et temporelles différentes. Les domaines d’applications des CPS comprennent un large choix de domaines incluant la santé, l’énergie, les véhicules autonomes et la robotique; de plus, beaucoup de ces CPS impliquent des exigences critiques de sûreté. Une des plus communes architectures dans les CPS est un contrôleur logiciel discret qui commu- nique avec son environnement physique selon le schéma de la boucle fermée dans lequel les données provenant des capteurs sont traitées et les résultats sont fournis et communiqués à des actionneurs. Nous nous intéressons à la vérification de la correction par construction de tels contrôleurs discrets qui exige une intégration correcte de modèles discrets et continus. La correction doit ‘émerger du processus de conception fondé sur des abstractions sûres et des modèles des lois physiques concernées. En général, de tels systèmes physiques sont caractérisés par des équations différentielles supposant des solutions dans des domaines continus; ainsi, des pas de discrétisation sont nécessaires. Une telle discrétisation peut être réalisée, en trouvant des solutions approximant des solutions à ces équations dans le modèle du domaine continu (en fait par intégration). Par conséquent, l’opération correcte d’un contrôleur doit être maintenant établie avec une borne spécifique d’erreur de l’approximation. Globalement, nous envisageons de combler l’espace entre les deux mondes discret et continu par l’utilisation de méthodes formelles et de la théorie du contrôle. Nous souhaitons accroître le niveau d’abstraction que l’on trouve dans les méthodes usuelles assurant ce lien. Afin de réussir cette en- treprise, nous proposons de nous concentrer sur des objectifs de haut niveau (O1) développer un modèle formel hybride; (O2) démontrer des étapes de raffinement pour différents types d’exigences de contrôle; (O3) proposer une méthode rationnelle de conception incrémentale et des outils associés; (04) valider la théorie/les modèles fondés sur des problèmes classiques à partir du corpus du contrôleur discret; et (O5) valider le processus rationnel fondé sur des cases d’étude à partir d’éléments des domaines d’applications.