LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: 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.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article