Etude d'un environnement de programmation et de vérification des systèmes réactifs, multi-langages et multi-outils
Jourdan, Muriel · HAL (Le Centre pour la Communication Scientifique Directe) · 1994
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 systems