Contribution à la définition et à l'implémentation du langage ``Extended LOTOS''

Mihaela Sighireanu

PhD thesis, Université Joseph Fourier (Grenoble, France), January 1999.

Abstract:

The design of critical, distributed applications is a complex problem for which it is advisable to use both formal description techniques, in order to specify unambiguously the behaviour of the applications under study, and automatic or semi-automatic verification tools, in order to validate the proper functioning of these applications.

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.

Keywords:

E-LOTOS, formal description techniques, labelled transition system, LOTOS, LOTOS NT, process algebra, structural operational semantics, timed Petri net, validation, verification.

Résumé :

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é.

Mots-clés :

E-LOTOS, techniques de description formelle, système de transitions étiquetées, LOTOS, LOTOS NT, algèbre de processus, sémantique opérationnelle structurée, réseau de Petri temporié, validation, vérification.