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 distribués, Sytèmes embarqués, Systèmes temps-réel, Méthodes formelles, Model checking, Automates temporisés, Techniques d'abstraction, 621.39
aLe caractère distribué des nouvelles architectures embarquées fait apparaître de nouveaux problèmes dans le développement des systèmes. En effet, leur comportement asynchrone nécessite la mise en œuvre de techniques permettant, d’une part, la prise en compte de ce phénomène au niveau de la spécification, et, d’autre part, d’aider à la validation de ces systèmes. C’est dans le cadre de la vérification formelle et, plus particulièrement, dans l'application du "model checking" que les travaux présentés dans ce mémoire s’inscrivent. Après une présentation des techniques couramment utilisées dans le domaine des systèmes temps-réel, la première partie de ce mémoire est consacrée à l’étude d’un modèle formel permettant la spécification des systèmes embarqués distribués. Ce modèle est fondé sur la définition d’une architecture fonctionnelle, d’une plateforme d’exécution et d’une fonction d’allocation. Afin de rendre possible la vérification formelle d’un système, deux étapes de transformation sont détaillées afin de mener à l'expression du modèle de spécification dans le formalisme des automates temporisés. En second lieu, nous présentons une méthode de vérification basée sur l'abstraction d’un système. Si l'abstraction d’un système tend à limiter l’espace des états d’un système, cette technique fait naître de nouvelles propriétés devant être vérifiées. Pour ce faire, nous proposons un cadre compositionnel permettant de dégager ces obligations de preuve. La validation d’une exigence conduit alors à valider les obligations de preuve engendrées par l'abstraction du modèle et l'exigence elle-même. The distributed feature of modern embedded architectures generates new problems during system development. Indeed, their asynchronous behaviour requires to develop teclmiques that allow, on the first hand, to take this phenomenon into account during specification and, on another hand, to help to validate these systems. The study developed in this report focuses on formal verification and, more particularly, on the application of model checking. After techniques used in the scope real time systems have been introduced, the first part of this report is dedicated to the study of a formal model that allows to specify distributed embedded systems. This model is based on the definition of a functional architecture, a runtime platfonn and an allocation function. To make formal verification appliable, two transformation steps are detailed in order to allow to express the specification model into timed automata formalism. Secondly, we introduce a verification method based on abstraction techniques. Despite abstraction tends to decrease the state space of a model, this technique generates new properties, named proof obligations, that have to be verified. To succeed in verifying such properties, we define a compositional framework that help firstly to exhibit proof obligations. The validation of a requirement amounts to verify, firstly, proof obligations generated by model abstraction and, secondly, the requirement itself.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article