Vérication des EFFBDs : Model checking en Ingénierie Système

Systems Engineering (SE) is an interdisciplinary and methodological approach for the design and operation of complex systems. Safety Engineering is a major SE process, yet the use of formal methods such as model checking, however powerful they may be, is hampered by their intrinsic complexity. Our research work, supported by an industrial partnership between the IRCCyN lab and Sodius, aimed at designing a tool which is directly usable during the SE design phase and which formally verifies functional models. To that end, high-level models and behavioral properties are transformed into low-level equivalents on which formal verifications are performed; analysis results are then expressed on the high-level models. To be specific, we considered EFFBDs as input models; this modeling language is indeed widely used in SE and adapted to model checking constraints. We formally established their syntax and semantics, then we were able to describe a translation into time Petri nets (TPNs) which we proved as preserving the model temporal behavior. Simultaneously, we described a quantitative temporal logic adapted to the EFFBDs and its translation into a corresponding logic on TPNs; we then established the computational complexity of its model checking. These successive theoretical results led us to develop a simulation and verification software tool that can analyze both functional and dysfunctional architectures (i.e. modeling functions failures); this tool is deployed and operated in an industrial context.L'Ingénierie Système (IS) est une méthodologie pluridisciplinaire de conception et de mise en oeuvre des systèmes complexes. La maîtrise de la Sûreté de Fonctionnement est un processus essentiel de l'IS et, dans sa poursuite, le recours à des méthodes formelles telles que le model checking se heurte généralement à des diffcultés d'utilisation. Dans cette thèse Cifre, effectuée en collaboration avec l'IRCCyN et Sodius, nous avons cherché à concevoir un outil de vérification formelle d'architectures fonctionnelles qui soit immédiatement utilisable dans des démarches de conception d'IS. Dans ce but, nous transformons des modèles et des propriétés comportementales haut niveau vers des équivalents bas niveau sur lesquels sont effectuées les vérifications formelles, le résultat étant présenté en termes haut niveau. Plus particulièrement, nous avons choisi comme modèles d'entrée les diagrammes EFFBDs : ils constituent un outil de modélisation largement utilisé en IS et adapté aux contraintes du model checking. Nous en avons établi la syntaxe et la sémantique formelles ; nous avons alors pu décrire une transformation vers les réseaux de Petri temporels (TPNs) dont nous avons prouvé qu'elle préserve le comportement temporel des modèles. Parallèlement, nous avons décrit une logique temporelle quantitative adaptée aux EFFBDs et sa traduction vers une logique correspondante sur les TPNs; nous avons alors pu établir la complexité de son model checking. Ces différents résultats théoriques nous ont ensuite permis de réaliser un outil de simulation enfin de vérification d'architectures fonctionnelles et dysfonctionnelles (c.-à-d. modélisant des fonctions défaillantes), déployé et utilisé industriellement