Spécification et vérification des systèmes temps réel réactifs en B
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
The purpose of this Phd thesis is to develop formal methods allowing the specification and the verification of critical systems. More precisely, we propose timed extensions to the B method. These extensions will allow to specify and check real time systems, as well as the possible interactions with their environment. We distinguish in this case the properties which must be satisfied by the environment and those which must be satisfied by the system. In the latter, we are interested more particularly in the reaction constraints of the controller. We describe timed models allowing the explicit modeling of time, so that it is possible to express real time constraints of a system as quantitative properties on deadlines. For the description of the dynamic behavior of the systems, we chose to extend MITL logic (Metric Interval Temporal Logic) into EMITL (Event/state Metric Interval Temporal Logic) with past operators and event properties. Our extension allows the simultaneous occurrence of several events.
Abstract FR:
L'objectif de cette thèse est de développer des méthodes formelles permettant la spécification et la vérification des systèmes critiques. Plus précisément, nous proposons des extensions temporisées à la méthode B. Ces extensions vont nous permettre de spécifier et de vérifier des systèmes temps réel, ainsi que les interactions possibles avec leur environnement. Nous distinguons dans ce cas les propriétés qui doivent être satisfaites par l'environnement de celles qui doivent être satisfaites par le système. Dans ces dernières, nous nous intéressons plus particulièrement aux contraintes de réaction du contrôleur. Nous décrivons des modèles temporisés permettant la manipulation explicite du temps, afin qu'il soit possible d'exprimer des contraintes temps réel d'un système sous forme de propriétés quantitatives sur des délais. Pour la description du comportement dynamique des systèmes, nous avons choisi d'étendre la logique MITL (Metric Interval Temporal Logic) en EMITL (Event/state Metric Interval Temporal Logic) avec passé. Notre extension permet d'introduire des propriétés d'événements et des opérateurs temporisés sur le passé.