Exploitation de contextes et d'observateurs pour la validation formelle de modèles

Le travail présenté dans le cadre de cette thèse concerne l'utilisation de techniques formelles pour la vérification de systèmes temps réel dans un contexte industriel. La technique mise en avant est la simulation exhaustive à base d'automates temporisés et d'observateurs. Ce travail cherche à réduire la distance qui existe entre les technologies formelles et le développement d'applications industrielles. Cette distance est liée à la rupture entre modèles de conception et modèles de vérification, rupture ne facilitant pas l'intégration des méthodes formelles dans un processus industriel. Une autre difficulté est l'explosion combinatoire, inhérente aux techniques de simulation exhaustive. Dans un contexte applicatif précis, choisissant des informations spécifiques au système à analyser, il est possible de réduire les comportements à un ensemble pertinent, en vue de réduire cette explosion. L'objectif de ce travail est d'une part de proposer un formalisme, inspiré des technologies utilisées dans l'industrie. Ce formalisme permet de décrire à la fois les propriétés à vérifier sous forme d'observateurs et le contexte représentant le comportement de l'environnement du système analysé. D'autre part, le but est de proposer la mise en oeuvre de ce formalisme au travers d'un outil et d'un guide méthodologique.RENNES1-BU Sciences Philo (352382102) / SudocBREST-Télécom Bretagne (290192306) / SudocSudocFranceF