Une algèbre de processus pour la modélisation et la vérification de systèmes temps-réel avec préemption

Other literature type French OPEN
Ermont, Jérôme (2002)
  • Subject: Systèmes embarqués | Temps-réel | Préemption | Algèbre de processus | Modélisation | Vérification | (In)décidabilité | 621.39

La conception et la maîtrise des systèmes embarqués proposent un défi de plus en plus important à relever avec le développement des aéronefs modernes. Cette importance révèle la nécessité de mettre en œuvre des méthodes formelles automatiques permettant d’assister le concepteur. Or, la nature distribuée et le partage des ressources de tels systèmes rendent difficiles leur description à l'aide des méthodes classiques mises en œuvre dans le cadre des systèmes temps-réel (algèbres de processus temporisés, automates temporisés, et, par la suite, de savoir si le système répond bien aux spécifications attendues (vérification). L'objectif de cette thèse est de proposer un élément de réponse à la modélisation, puis à la vérification, de tels systèmes en utilisant les mécanismes de préemption pour réaliser le partage de ressources. L’idée proposée consiste à construire un système embarqué sous la forme d'un ensemble de processus réactifs communicants et préemptibles spécifiés au moyen d’un formalisme algébrique. Deux types de préemption ont été identifiés : l'interruption définitive et la suspension temporaire avec reprise. De ces deux types de préemption découlent la structure de l'étude. En premier lieu, nous proposons de définir une algèbre de processus, nommée TPAPa, permettant l'interruption définitive. Afin de pouvoir vérifier les systèmes décrits dans ce formalisme, une traduction en automates temporisés a été réalisée. De cette manière, il est possible d’utiliser les outils de model-checking classiques (UPPAAL, KRONOS, CMC, ...). En deuxième lieu, nous avons intégré la possibilité de suspendre temporairement l'activité d’un processus puis sa reprise à partir du point d’arrét. Cette fois, la traduction conduit au formalisme des automates à chronomètres. Nous montrons alors que la vérification de propriétés sur une algèbre de processus possédant des mécanismes de suspension, nommée TPAPas, est en général indécidable. Design and mastery of embedded systems are a major challenge whose relevance has increased with the developpement of new generation of aircraft. The need for formal methods to help the designer appared obvious. The distributed and shared resources nature of such systems make their description using classical modelling methods of real-time systems (timed process algebra, timed automata, ...) and, afterwards, their verification from its specifications a difi-icult task. The aim of this dissertation is to provide a solution to both the modelling problem and the verification problem, of such real time systems by using preemption mechanisms to share resources. The underlying idea consists of constructing an embedded system as a set of reactive and preemptive communicating processes specified in an algebraic formalism. Two kinds of preemption mechanisms have been identified : abort and suspension with resumption. On the one hand, a process algebra, called TPAPa, which only allows the abort mechanism is first defined. The verification of system described in TPAPa uses a translation into timed automata formalism. In this way, classical model-checking tools, such as KRONOS, UPPAAL, CMC, ..., can be used. On an another hand, the suspension of the activity of a process and its resumption from the suspension point have been added. The translation of such processes leads to the stopwatch automata formalism. The verification of real-time properties over a timed process algebra supporting suspension and resumption mechanisms, namely TPAPa.s, is in general undecidable, as established in this dissertation.
Share - Bookmark