Réactions synchrones : spécification et analyse
-
Thèse soutenue le 19 novembre 2002 à l'IRISA,
devant le jury :
| Jean-Pierre Banâtre | président |
| Ahmed Bouajjani | examinateur |
| Paul Caspi | rapporteur |
| Robert De Simone | rapporteur |
| Paul Le Guernic | directeur de thèse |
| Sophie Pinchinat | encadrante de thèse |
-
315 pages, compressed
Postscript file (825Ko) Pdf
file (1.92Mo)
-
Bibtex entry:
@PhdThesis{these:mnebut,
author = {Mirabelle Nebut},
title = {Réactions synchrones~: spécification et analyse},
school = {Université de Rennes 1},
year = {2002},
key = {ordre 2741},
month = {novembre},
note = {in french}
}
Résumé :
L'approche synchrone est dédiée à la conception
des systèmes réactifs. Grâce à leur sémantique
forte, des langages synchrones comme Esterel, Lustre et Signal permettent
de spécifier le comportement des systèmes de manière
abstraite et rendent possible leur validation formelle, cruciale dans le
contexte des applications critiques. La validation formelle des systèmes
est un domaine de recherche en pleine expansion, spécialement en
ce qui concerne les espaces d'état infinis et les aspects numériques.
L'application de ces méthodes aux programmes synchrones est fondamentale,
mais plus ou moins simple. Notamment dans le cas de Signal l'absence des
variables est explicitée par une valeur spéciale, ce qui
empêche l'interfaçage direct des outils Signal aux techniques
existantes. Cette thèse traite de la manipulation de l'absence des
variables synchrones, plus particulièrement dans les langages flot
de données. Après un état de l'art du traitement de
l'absence dans les sémantiques et les analyses synchrones, on présente
un langage d'horloges appelé CL, basé sur une extension par
des aspects numériques des horloges booléennes utilisées
dans le contexte de la compilation Signal. On montre que CL permet d'interfacer
naturellement les modèles étendus avec l'absence explicite
à des théories standard, de plusieurs manières.
Mots clés : paradigme synchrone, spécification, horloges,
modélisation et traitement de l'absence des variables, méthodes
formelles.
Abstract:
The synchronous approach is dedicated to the design of reactive systems.
Thanks to their strong semantics, synchronous languages like Esterel, Lustre
and Signal allow the abstract specification of systems behavior, and make
possible their formal validation, what is crucial in the case of safety
critical applications. The formal validation of systems is a research domain
in wide expansion, especially concerning infinite state systems and numerical
aspects. The application of these methods to synchronous programs is fundamental
but more or less easy. In particular in the Signal case absence of variables
is made explicit by a special value, which prevents from directly interfacing
verification tools to existing methods. This document deals with the absence
handling of synchronous variables, more particularly for data-flow languages.
After a state-of-the-art over the treatment of absence in synchronous semantics
and analyses, we present a clock language called CL, based on an extension
by numerical aspects of boolean clocks used in the Signal compilation process.
CL naturally interfaces models extended with explicit absence to standard
theories, by several ways.
Keywords: synchronous paradigm, specification, clocks, modeling
and handling of variable absence, formal methods.
Mirabelle Nebut
Last
modified: Wed Jan 29 18:00:53 /etc/localtime 2003