Mihaela SIGHIREANU soutiendra le 21 janvier 1999 à 14 h
à l'amphithéâtre de la Maison Jean Kuntzmann
(110, rue de la Chimie, Campus Universitaire de Grenoble)
une thèse de DOCTORAT de l'UNIVERSITE JOSEPH FOURIER de GRENOBLE,
spécialité : informatique, intitulée :
Thèse préparée dans l'Unité de Recherche INRIA Rhône-Alpes
(projet Spectre / laboratoire Verimag, puis action Vasy),
sous la direction de M. Hubert GARAVEL.
La mise au point des applications distribuées critiques est un problème complexe pour lequel il est recommandé d'utiliser des techniques de description formelle afin de spécifier sans ambiguïté le comportement des applications considérées, et des outils de vérification automatique ou semi-automatique afin de valider le bon fonctionnement de ces applications.
Les techniques de description formelle existantes (notamment les trois langages normalisés ESTELLE, LOTOS et SDL) présentent des inconvénients et des limitations qui restreignent leur adoption en milieu industriel. Cette thèse vise à résoudre ce problème en proposant un nouveau formalisme, appelé LOTOS NT, pour la description formelle des applications parallèles et temps-réel. Ce formalisme, qui combine des concepts issus des langages de programmation fonctionnels et impératifs et des algèbres de processus temporisées, est plus simple et plus expressif que les langages existants et autorise une compilation plus efficace. Ce travail constitue une contribution à la révision de la norme LOTOS entreprise à l'ISO.
Cette thèse définit formellement les trois parties du langage LOTOS NT (données, contrôle et modules) en donnant leur syntaxe, leur sémantique statique et leur sémantique dynamique (formulée de manière opérationnelle en termes de systèmes de transitions temporisés). Ensuite, un modèle d'exécution intermédiaire basé sur des réseaux de Petri temporisés est défini. Enfin, deux algorithmes de traduction permettent de passer de LOTOS NT à ce modèle intermédiaire, d'une part, et du modèle intermédiaire à des systèmes de transitions temporisés, d'autre part. L'intérêt de cette approche a été montré sur plusieurs applications concrètes et un compilateur prototype pour le langage LOTOS NT a été développé.
| Président : | M. Jacques VOIRON, professeur à l'UJF |
| Rapporteurs : | M. Claude JARD, directeur de recherche CNRS |
| M. Guy LEDUC, professeur à l'Université de Liège | |
| Examinateurs : | M. Ed BRINKSMA, professeur à l'Université de Twente |
| M. Hubert GARAVEL, chargé de recherche INRIA |
La soutenance sera naturellement suivie d'un pot, au rez-de-chaussée de la Maison Jean Kuntzmann, auquel vous êtes tous cordialement invités.
The existing formal description techniques (in particular, the three standardized languages ESTELLE, LOTOS, and SDL) present drawbacks and limitations, which restrict their industrial acceptance. This thesis addresses this problem by proposing a new formalism, called LOTOS NT, for the formal description of parallel and real time applications. This formalism, which combines concepts from functional and imperative programming languages and timed process algebras, is simpler and more expressive than the existing languages and allows more efficient compiling techniques. This work represents a contribution to the revision of the standard LOTOS undertaken at ISO.
This thesis formally defines the three parts of the LOTOS NT language (data, behaviour, and modules) by giving their syntax, static semantics, and dynamic semantics (defined operationally in terms of timed transition systems). Then, an intermediate execution model based on timed Petri nets is defined. Finally, two algorithms enable the translation from LOTOS NT to the intermediate model, on the one hand, and from the intermediate model to the timed transition system, on the other hand. The interest of this approach has been shown for several applications and a prototype compiler has been developed for the LOTOS NT language.
Back to the VASY Home Page