Etude d'un environnement de programmation et de vérification des systèmes réactifs, multi-langages et multi-outils

This thesis deals with the programmation and verification of reactive systemes. In a first part, we define a multiparadigm langage nammed ArgoLus. ArgoLus is based on Argos and Lustre, two synchronous langages. In order to describe reactive systemes Argos uses a modular state/transition approach, while Lustre uses data-flow constructs. In the ArgoLus langage these two styles are mixed. The idea is to allow the description of elementary objects in each of the two styles, and their combination with both constructs. In a second part, we define the Argos semantic in terms of timed graphs. The initial semantic of Argos is expressed in terms of labelled transition systems. The drawback of this model is the well-known phenomenom of state explosion which occurs when large counters of event occurrences are used in the program. This state explosion reduces the formal verification possibilities. The advantage of timed graphs, which are automata extended with time counters, is that their size is independant from the delay values of the counters used in the program. Consequently, this model is less sensitive to the state explosion problem, so the possibilities of formal verification are improved. Moreover, it is possible with this kind of model to express quantitative real-time properties. Finally, we study the possibility of using a large class of formal verification tools not exactly designed for reactive systemsCe travail porte sur la programmation et la verification des systemes reactifs. Il consiste dans une premiere partie en la definition d'un langage mixte imperatif/declaratif, nomme ArgoLus, fonde sur les langages synchrones Argos et Lustre. Argos est un langage imperatif a base d'automates paralleles et hierarchises. Lustre est un langage declaratif fonde sur le modele flots de donnees. Le langage ArgoLus permet de melanger au niveau source ces deux langages. La definition des traductions structurelles d'ArgoLus en Argos ou en Lustre offre deux solutions interessantes pour mettre en oeuvre ce langage, tout en profitant des environnements deja existants. Dans un deuxieme temps la semantique d'Argos en termes de graphes temporises a ete definie. Initialement, celle-ci est definie en termes de systemes de transitions etiquetees. L'inconvenient de ce modele est lie au phenomene d'explosion du nombre d'etats qui limite les possibilites de verification formelle. Une des causes de cette explosion est la presence dans les programmes de compteurs d'occurrences d'evenement. Les graphes temporises sont des automates etendus avec des compteurs de temps, dont la taille est independante des valeurs limites des compteurs du programme. Par consequent, ils sont moins sensibles au phenomene d'explosion du nombre d'etats, d'ou une amelioration des possibilites de verification formelle. De plus, il est possible grace a ce modele d'exprimer des proprietes quantitatives faisant reference au temps. Enfin, un troisieme aspect de ce travail porte sur l'utilisation pour les systemes reactifs d'outils de verification formelle, non concus exactement pour ce type de systemes