Vérification des propriétés temps réel dans le langage Fiacre

Dans cette thèse, nous nous intéressons à la problématique de la vérification formelle des systèmes critiques temps réel, c’est-à-dire des systèmes dont l’exécution dépend de certaines contraintes temporelles. La spécification formelle des exigences pour de tels systèmes, ainsi que leur vérification, reste une tâche très compliquée, surtout pour les non experts. Plusieurs solutions ont été proposées pour faciliter la spécification et la vérification des systèmes temps-réels. Un premier type d’approche est basée sur la définition d’un ensemble de patrons de spécification qui représentent les propriétés les plus utilisées en pratique. Cependant, ce type de solutions n’est pas toujours supporté par un outillage de vérification efficace, dans le sens que les auteurs de ces langages de patrons ne fournissent pas directement une implantation pour leur langage. Un second type d’approches repose sur l’utilisation du formalisme des logiques temporelles pour spécifier les propriétés à vérifier et sur les techniques de model-checking pour leur vérification. S’agissant de systèmes temps-réels, il est dans ce cas nécessaire d’utiliser des extensions temporisées des logiques temporelles. Cependant, ces approches donnent le plus souvent lieu à des problèmes de model-checking qui sont indécidable, ou dont la complexité en pratique est très élevée. Dans ce travail, nous suivons la première approche et proposons un langage de patrons de propriétés temps-réels accompagnés d’un outil de vérification par model- checking. Nous apportons plusieurs contributions à ce domaine. Nous proposons un cadre théorique complet pour la spécification et la vérification de patrons de propriétés temps réel. Notre approche a été implantée dans le contexte du langage de modélisation Fiacre. Enfin, nous définissons deux méthodes complémentaires permettant de vérifier la correction de notre approche de vérificationThe formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of real time systems, that is in the situation where the correctness of the system depends upon timing constraints, such as the “timeliness” of some interactions. Many solutions have been proposed to ease the specification and the verification of such systems. An interesting approach—that we follow in this thesis—is based on the definition of specification patterns, that is sets of general, reusable templates for commonly occurring classes of properties. However, patterns are rarely implemented, in the sense that the designers of specification languages rarely provide an effective verification method for checking a pattern on a system. The most common technique is to rely on a timed extension of a temporal logic to define the semantics of patterns and then to use a model-checker for this logic. However, this approach may be inadequate, in particular if patterns require the use of a logic associated to an undecidable model-checking problem or to an algorithm with a very high practical complexity. We make several contributions. We propose a complete theoretical framework to specify and check real time properties on the formal model of a system. First, our framework provides a set of real time specification patterns. We provide a verification technique based on the use of observers that has been implemented in a tool for the Fiacre modelling language. Finally, we provide two methods to check the correctness of our verification approach; a “semantics”—theoretical— method as well as a “graphical”-practical- metho