Durée: 42 mois (1er Octobre 2011 - 31 Mars 2015)
Axe Thématique: Méthodes, outils et technologies pour les systèmes embarqués (Principal) Ingénierie du logiciel (Secondaire)
Coordinateur du projet: Jean-Marc Faure
Présentation
Le projet VACSIM (Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle) réunit deux industriels, un concepteur et exploitant de systèmes critiques (EDF R&D) et un éditeur de logiciels d'ingénierie numérique (Dassault Systèmes), et quatre laboratoires : un relevant de l'automatique (LURPA) et trois de l'informatique (I3S, INRIA Rennes, LaBRI). Ce partenariat pluridisciplinaire est nécessaire pour résoudre le problème posé dans ce projet qui consiste à tirer profit des avantages respectifs des techniques de simulation, en incluant des modèles des processus commandés, et des méthodes d'analyse formelles, pour la validation de la commande des systèmes critiques.Ce projet fait suite au projet ANR TESTEC (TEst des Systèmes Temps réel Embarqués Critiques - 07 TLOG 022) dont le consortium était le même. Ce projet a fourni de nombreux et importants résultats tant académiques qu'industriels. Il a également montré que les seules approches formelles de test et de vérification n'étaient pas suffisantes pour la validation de commandes de systèmes critiques, mais qu'il convenait de s'intéresser à leur couplage avec des approches de simulation, ces deux approches ayant des avantages complémentaires, notamment en termes de capacité à passer à l'échelle et de maîtrise du taux de couverture de l'analyse.
Le nouveau projet vise à développer des contributions de nature à la fois méthodologique (définition de nouveaux modes d'utilisation des simulateurs, règles de couplage simulation/ méthodes formelles) et formelle (adaptation, extension ou création de méthodes formelles) qui permettront la réalisation d'un démonstrateur, sur la base de l'outil ControlBuild, outil d'ingénierie numérique de la société Dassault Systèmes, illustrant, sur la base d'études de cas industriels, les bénéfices du couplage.
Le but ultime du projet est de proposer un continuum de validation durant le cycle de vie de la commande des systèmes critiques basé sur des environnements d'ingénierie numérique.
Objectifs globaux, verrous scientifiques/techniques
L'objectif final du projet VACSIM est le développement d'un démonstrateur de l'intérêt du couplage simulation / méthodes d'analyse formelles pour l'ingénierie numérique du contrôle-commande des systèmes critiques. Ce démonstrateur sera basé sur les outils de simulation et validation de la société Dassault Systèmes connectés aux résultats obtenus durant le projet et permettra le traitement de plusieurs cas industriels.Pour atteindre cet objectif, plusieurs verrous scientifiques sont à lever afin d'améliorer le niveau de maturité des méthodes d'analyse formelle ; ils concernent la décidabilité et la complexité du model-checking de certaines classes d'automates finis temporisés, la résolution de systèmes de contraintes non linéaires sur les flottants, la détermination de taux de couverture par identification de systèmes à événements discrets, et le développement de stratégies permettant le passage à l'échelle de ces méthodes.
Les verrous techniques auxquels devra s'attaquer ce projet sont relatifs aux méthodologies d'utilisation des simulateurs de processus et au couplage entre méthodes de simulation, vérification et test, en s'intéressant à la problématique de modélisation multi-échelles. Il convient de souligner l'aspect novateur de ce projet, les approches de simulation et d'analyse formelle étant bien souvent opposées, alors que nous pensons qu'aucune de ces approches prise isolément ne peut fournir une solution complète pour la validation des systèmes critiques mais qu'il convient de développer des stratégies d'utilisation combinée.
On pourra noter enfin que le développement de ces stratégies nécessite un partenariat pluridisciplinaire entre automaticiens et informaticiens afin de tirer le meilleur profit des compétences de ces deux communautés en termes d'outils de modélisation et d'analyse. Les résultats du projet pourront être intégrés dans l'outil ControlBuild à sa conclusion. En particulier, les résultats obtenus lors des traitements de cas industriels seront d'une grande utilité pour l'industrialisation.
Programme de travail
Le projet VACSIM comporte six tâches techniques :- Validation par test progressif par parties de systèmes logiques,
- Validation par simulation de partie opérative,
- Apport des techniques d'identification des SED à la validation des systèmes critiques,
- Validation formelle de propriétés quantitatives : approche par automates, -
- Validation formelle de propriétés quantitatives : approche par contraintes,
- Démonstrateur et traitement de cas industriels,
- Coordination
- de réunions mensuelles du comité de pilotage du projet, par visio- ou télé-conférence
- et de réunions bisannuelles, d'une durée de deux jours chacune et se déroulant à tour de rôle chez chacun des partenaires, réunissant tous les acteurs du projet ; ces réunions permettront des exposés suivis de discussions approfondies ainsi que des échanges formels et informels et constitueront les jalons du projet.
Retombées scientifiques
Plusieurs verrous scientifiques sont à lever durant le projet, afin d'améliorer le niveau de maturité des méthodes d'analyse formelle ; ils concernent la décidabilité et la complexité du model-checking de certaines classes d'automates finis temporisés, la résolution de systèmes de contraintes non linéaires sur les flottants, la détermination de taux de couverture par identification de systèmes à événements discrets, et le développement de stratégies permettant le passage à l'échelle de ces méthodes. Les résultats scientifiques obtenus lors de ces travaux seront soumis aux conférences et revues reconnues des domaines considérés, en particulier aux conférences organisées par l'IEEE, l'IFAC et l'IFIP, aux revues IFAC Automatica ou Control Engineering Practice, IEEE TAC, IEEE TASE, LNCS. Les résultats techniques obtenus, en particulier les démonstrateurs qui constituent les livrables 1.2, 2.2 et 6.1, ont vocation à être industrialisés et à faire partie de l'offre logicielle de la société Dassault Systèmes à l'issue du projet. Ceci afin de fournir des aides efficaces aux services d'ingénierie ayant en charge le développement de futurs systèmes critiques, que ce soit dans le domaine de la production d'énergie ou dans d'autres domaines (transport ferroviaire ou maritime, secteur automobile,...).- Compte-rendu de fin de projet
- Livrable L5.3 : Une approche CSP pour l'aide à la localisation d'erreurs
- Livrable L5.2 : Validation formelle de propriétés quantitatives : Approche par contraintes
- Livrable L5.1 : Apport de la bio-informatique à la vérification des systèmes complexes
- Livrable L4.2 : Etudes de techniques de validation à l'exécution pour des systèmes réactifs critiques.
- Livrable L4.1 : Etude de techniques d'analyse quantitative des modèles temporisés
- Livrable L3.1 : Construction de modèles formels de controleurs logiques pour le test de conformité
- Livrable L3.2 : Validation fonctionnelle de contrôleurs logiques : contribution au test de conformité et à l'analyse en boucle fermée
- Livrable L2.2 : validation par simulation de partie opérative.
- Livrable L2.1 : Spécification et validation, sur études de cas, dune méthode d'utilisation des simulateurs de parties opératives : objectifs, propriétés de sûreté de fonctionnement, taux de couverture et limitations de la simulation
- Livrable L1.3 : Evaluation sur études de cas industriels d'un algorithme de test progressif par parties de systèmes logiques non-bouclés dans l'environnement ControlBuild
- Livrable L1.1 : Algorithmes de génération et d'exécution du test des systèmes logiques, séquentiels et temporisés non bouclés
- Document scientifique
- Réunion plénière 6, 14-15 Octobre 2014, Cachan
- Réunion plénière 5, 9-10 Avril 2014, Nice
- Réunion plénière 4, 15 Octobre 2013, Chatou
- Réunion plénière 3, 15-16 Avril 2013, Brest
- Réunion plénière 2, 6-7 Septembre 2012, Rennes
- Réunion plénière 1, 15-16 Mars 2012, Bordeaux
- Réunion de Lancement, 30 Septembre 2011, Cachan (Compte-rendu
)
- ANR
- ...