TuMult est un partenariat international d’Inria entre l’équipe Kairos à Inria Sophia Antipolis Méditerranée, FR et East China Normal University (E.C.N.U.) à Shanghai, CN

Aperçu

L’équipe Kairos de l’INRIA (et précédemment les équipes Oasis et Aoste) et le Software Engineering Institute de l’E.C.N.U. ont une longue histoire de collaboration autour des modèles, méthodes et outils pour la programmation sécurisée de systèmes critiques, y compris les systèmes réactifs et / ou distribués, les systèmes cyber-physiques (CPS) et l’Internet des Objets (IoT).

Programme de travail pour les années à venir

• Modélisation des environnements incertains des systèmes cyber-physiques

Le Temps Logique est l’un des principaux fondements scientifiques de l’équipe AOSTE. Dans le contexte de la théorie de la concurrence, nous avons principalement utilisé des systèmes de contrôle discrets capables de garantir un déterminisme fonctionnel indépendamment de toute variation temporelle dépendant de l’implémentation. S’attaquer aux systèmes cybernétiques consiste à élargir ces hypothèses pour prendre en compte l’environnement externe dans le cadre de la conception. L’environnement obéit aux lois de la physique qui dépendent habituellement de la considération du temps physique avec des modèles qui sont une approximation de la réalité et qui introduisent nécessairement une grande incertitude sur le comportement. Cette tâche explore la définition d’extensions consistantes au temps logique pour capturer à la fois le comportement physique continu et construire une caractérisation abstraite par une approximation statistique [FACS’16].

• SMT pour l’heure logique

Alors que les systèmes synchrones se concentrent généralement sur des systèmes de contrôle basés sur des états finis, notre abstraction du temps logique repose à la fois sur l’algèbre booléenne (pour les opérations synchrones) et l’arithmétique entière (pour les mécanismes de synchronisation). Nous nous efforçons de trouver des algorithmes efficaces pour résoudre des sous-classes de systèmes bien définis. Dans ce contexte, SMT (Satisfiabilité modulo théories) est une solution prometteuse pour combiner et résoudre des systèmes qui combinent plusieurs théories. Nous avons eu les premiers résultats sur cet aspect [SCP’17] mais nous devons encore augmenter le sous-ensemble de contraintes qui peuvent être traitées efficacement ainsi que les performances des outils de résolution.

• Spécification spatio-temporelle pour des systèmes fiables de transport intelligents

En se concentrant sur les systèmes de transport intelligents en tant que sous-ensemble des systèmes cyber-physiques, nous rencontrons des problèmes spécifiques. Outre le facteur temporel omni-présent dans les systèmes temps réel et les systèmes intégrés, un emplacement physique joue également un rôle central. Les fonctions du système (comme par exemple un train) doivent être effectuées au bon moment ET au bon endroit. Cette tâche se focaliserait sur les extensions de notre framework pour une logique spatio-temporelle basée sur le temps logique. Cela signifie une description de l’emplacement des infrastructures ainsi que la capacité à créer des contraintes qui dépendent à la fois du temps (logique ou physique) et des emplacements (logiques ou physiques).

• Open pNets

Les méthodes d’analyse et de garantie des propriétés des systèmes critiques et complexes, y compris leurs aspects liés aux données et au temps, ont fortement évolué avec l’émergence de moteurs efficaces de contrôle de la satisfiabilité (SAT et SMT). Nous travaillons sur de nouvelles méthodes combinant des paradigmes de vérification classiques (construction et minimisation de l’espace d’états, vérification de modèles) avec des approches SMT pour créer des méthodes de vérification symboliques et compositionnelles et des plates-formes d’outils. Nous avons des résultats préliminaires intéressants [Forte’16, Avocs’18] et collaborons activement à la fois sur les résultats fondamentaux et le développement de prototypes.