Vacsim: Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle
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
dont certaines sont décomposées en sous-tâches. Les deux premières tâches visent à proposer des contributions méthodologiques, alors que les résultats des trois tâches suivantes sont de nature formelle. La dernière tâche technique a pour objectif d'utiliser les résultats des cinq tâches précédentes dans un démonstrateur permettant de montrer, sur la base de traitements de cas industriels, 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. La tâche de coordination assure la cohérence entre les travaux des cinq premières tâches techniques et en particulier entre les modèles de simulation et ceux utilisés par les méthodes formelles. Les livrables du projet, documents ou logiciels, sont prévus à T0+12, T0+18, T0+24, T0+30 et T0+36. Un comité de pilotage sera mis en place pour assurer le management du projet ; chaque partenaire du projet y sera représenté par un membre. Outre la tâche de coordination définie précédemment, la complémentarité et la cohérence des travaux des différentes tâches seront assurées par la tenue :
  • 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,...).