David Camarazo fera une répétition de sa soutenance de thèse le lundi 8/12 après-midi à 14h, amphi Gevrey.
Titre : Vérification semi-automatisée pour la conception de systèmes complexes critiques – SOLAR-FU (Second Order Logic And Reasoning For Unification)
Résumé: Dans des contextes industriels, la modélisation de systèmes complexes implique la production de nombreux modèles dans différents formats. Ces modèles permettent à des acteurs de différentes spécialités de communiquer entre eux. Pour assurer le bon fonctionnement du système, il est alors nécessaire d’assurer la cohérence de ces modèles hétérogènes. De plus, dans le cas de systèmes critiques, dont la défaillance peut avoir des conséquences graves sur la santé des usagers, la cohérence de ces modèles est essentielle pour garantir la sécurité et la fiabilité du système. Cependant, en pratique, la vérification de cette cohérence est une tâche difficile en raison de l’hétérogénéité des modèles. Les travaux actuels reposent principalement sur ce qu’on appelle les méthodes formelles. Ces méthodes de vérification interviennent à la fin du processus de modélisation. Elles consistent à traduire le modèle dans un formalisme formel i.e. dans une syntaxe qui explicite la sémantique. Cela permet à un ordinateur de traiter automatiquement les informations des modèles pour simuler le comportement du système et vérifier que toutes les contraintes de sécurité sont respectées. Bien que les méthodes formelles proposent aujourd’hui une solution satisfaisante en termes de vérification à l’issue du processus de modélisation, elles ne permettent pas une vérification continue et une assistance satisfaisante pour structurer les données pendant le processus de modélisation. C’est dans cette optique que nous proposons une nouvelle approche de vérification basée sur des structures de données explicites et formelles : des ontologies. Dans ce travail, nous proposons une approche de vérification semi-automatisée basée sur une unification de bases de connaissances, permettant d’intégrer les connaissances de différents modèles dans une structure cohérente, et un mécanisme de raisonnement utilisant des règles logiques du second ordre permettant la formulation et l’application de règles de vérification réutilisables et généralisables. Nous appelons ce mécanisme « SOLAR-FU » pour « Second Order Logic And Reasoning For Unification ». Nous illustrons et évaluons notre approche sur des cas d’usage ferroviaires. Nous discutons également de son implémentation, ainsi que des perspectives d’évolution vers des applications industrielles plus larges.