CRAN - Campus Sciences
BP 70239 - 54506 VANDOEUVRE Cedex
Tél : +33 (0)3 72 74 52 90 Fax : +33 (0)3 72 74 53 08
cran-secretariat@univ-lorraine.fr
 
 
Sujet de Thèse : Modélisation, vérification formelle symbolique et évaluation probabiliste du niveau de confiance des systèmes sécuritaires numériques
Dates : 2016/10/01 - 2019/09/30
Etudiant : Margaux DUROEULX
Directeur(s) CRAN : Nicolae BRINZEI
Autre(s) Directeur(s) : Stephan Merz (stephan.merz@loria.fr)
Description : Contexte
Les systèmes numériques sont omniprésents ; ils contrôlent les processus et les transactions critiques pour le fonctionnement de l’économie et de la société des nations industrialisées. Il est donc primordial pour la confiance dans ces systèmes qu’ils assurent des propriétés de sûreté essentielles. Des recherches approfondies dans l’automatique et l’informatique ont été consacrées à l’élaboration des théories et des approches (fondées mathématiquement) qui abordent ces propriétés. Celles-ci comprennent des techniques de vérification formelle permettant de démontrer que les systèmes numériques sont exempts d’erreurs critiques, mais aussi des techniques probabilistes qui permettent d’évaluer le niveau de confiance en ces systèmes. Cependant ces techniques peuvent rarement être utilisées conjointement pour des systèmes industriels : même si elles font généralement intervenir une analyse de propriétés de sûreté exprimées à l’aide d’opérateurs booléens, les modèles sont le plus souvent exprimés à des niveaux différents d’abstraction. La difficulté est due également à la complexité de systèmes numériques industriels engendrée à la fois par un nombre élevé des composants matériels avec des interactions fortes entre eux, mais aussi à la complexité des algorithmes implantés, de logiques de votes multiples et variées qu’ils supportent.
Les propriétés structurelles d’un système donnent souvent lieu à des propriétés de monotonie des fonctions booléennes sous-jacentes aux modèles d’évaluation probabiliste. Les chercheurs du CRAN ont développé des méthodes qui exploitent cette propriété en considérant les liens minimaux et la propagation de leur recouvrement le long du graphe d’état du système qui, de plus, est un graphe ordonné obtenu à partir d’une représentation de type diagramme de Hasse [1,2]. Des problèmes de satisfiabilité se posent dans ce contexte pour analyser le graphe d’état et les chercheurs du LORIA étudient des techniques et outils efficaces pour traiter ces problèmes.

Objectif de la thèse
L’objectif de cette thèse est de faire converger les travaux sur l’évaluation probabiliste et avec ceux sur les techniques symboliques de vérification. Plus concrètement, nous proposons d’adapter ces dernières techniques pour les intégrer dans l’analyse structurelle de modèles de défaillances sur lesquels repose l’évaluation probabiliste des propriétés de sûreté des systèmes sécuritaires numériques permettant de déterminer le niveau de confiance qu’on peut accorder à ces systèmes. Des problèmes de satisfiabilité propositionnelle, voire de satisfiabilité modulo théories (SMT), apparaissent en effet naturellement dans le cadre d’une approche méthodologique qui s’appuie sur la propriété de monotonie du graphe d’état et qui permet une amélioration démontrée par rapport aux techniques traditionnelles utilisées dans ce contexte.

Travail proposé et résultats attendus
Les analyses préliminaires de sûreté aboutissent en général à une spécification sous différents formats (e.g. format OpenPSA, langage Figaro, etc.) issue des modèles type arbre de défaillances, diagramme de fiabilité, BDMP (Boolean Driven Markov Processes). Cette spécification peut être, mathématiquement, traduite dans une ou plusieurs fonctions booléennes. A partir de cette représentation, le travail de thèse consistera à utiliser les approches de vérification formelle, telles que SMT [8] qui en analysant les propriétés de sûreté permettra de déterminer l’ensemble de liens minimaux d’un système cohérent , relatives à ces propriétés. Dans le cas des systèmes non-cohérents, la vérification formelle des propriétés de sûreté devrait permettre de déterminer, l’ensemble des liens terminaux ainsi que les coupes résiduelles. Ces ensembles déterminés permettront ensuite de générer le graphe d’état ordonné et son exploitation probabiliste [1,2] permettra ensuite d’estimer le niveau de confiance du système. On obtiendra ainsi une méthodologie globale permettant de vérifier formellement les propriétés de sûreté et d’évaluer le niveau de confiance effectif d’un système.
De même, les spécifications issues des analyses préliminaires de sureté prennent en compte, dans la plupart des cas, toutes les défaillances possibles (défaillances dangereuses détectées ou non détectées, mais aussi défaillances sûres), la fonction booléenne obtenue ensuite étant plutôt un modèle de fiabilité ou de disponibilité. Or dans les cas des études de sûreté, il faudra simplifier ce modèle en prenant en compte seulement les défaillances relatives à la (les) propriété(s) de sûreté étudiée(s), c’est-à-dire les défaillances dangereuses amenant au non-respect de cette (ces) propriété(s). Les approches de vérification formelle devront permettre de décomposer le système dans des sous-systèmes, dont au moins pour certains, les propriétés de sûreté sont vérifiées. Il deviendra alors possible de générer des sous-graphes d’état ordonnés simplifiés relativement seulement aux sous-systèmes, ce qui simplifiera l’évaluation probabiliste du niveau de confiance de ces sous-systèmes. Néanmoins, il faudra par la suite proposer une méthode pour déterminer le niveau de confiance au niveau du système dans sa globalité à partir de ses sous-systèmes dont leur sûreté a été prouvé et/ou quantifié préalablement.
L’extension de cette approche à des composants (et des variables qui les représentent) qui n’auront plus un comportement binaire, mais un comportement multi-états permettra d’obtenir un graphe d’état multidimensionnel du système. Cette modélisation devrait permettre de prendre en compte des niveaux de dégradation de la sûreté d’un système au fur et à mesure de son exploitation, afin d’avoir une évaluation d’un niveau de confiance dynamique qu’on peut affecter à ce système.
Les développements théoriques qui feront l’objet de cette thèse permettront d’améliorer la confiance dans les systèmes sécuritaires numériques (Safety Instrumented Systems SIS) qui représenteront la cible principale d’application de ces travaux de recherche. Les résultats obtenus seront validés par nos partenaires industriels.
Mots clés : sûreté des systèmes, vérification formelle, satisfiabilité, évaluation probabiliste, graphe ordonné
Département(s) :
Ingénierie des Systèmes Eco-Techniques
Financement : financement LUE
Publications : hal-01147937v1, hal-01242667v1    + CRAN - Publications