This thesis deals with the programming and verification of reactive systems. In a first part, we define a multi-paradigm language called ArgoLus. ArgoLus is based on Argos and Lustre, two synchronous languages. In order to describe reactive systems, Argos uses a modular state/transition approach, while Lustre uses data-flow constructs. In the ArgoLus language 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 semantics in terms of timed graphs. The initial semantics of Argos is expressed in terms of labeled transition systems. The drawback of this model is the well-known phenomenon 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 independent of 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.
Committee (September 29th, 1994):
— Jacques Voiron, UJF, President
— Gérard Berry, Ecole des Mines/CMA, Reviewer
— Michel Sintzoff, U. Louvain, -Reviewer
— André Arnold, Pr. U. Bordeaux
— Florence Maraninchi, UJF, supervisor
— Daniel Pilaud, Verilog
Publications
2014
- Implementing and Reasoning About Hash-consed Data Structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Journal of Automated Reasoning - [bibtex]
2013
- Implementing hash-consed data structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Interactive theorem proving (ITP) - [bibtex]
1996
- Vérification de systèmes réactifs en Argos temporisé. Muriel Jourdan, Florence Maraninchi - Congrès AFCET : Modélisation des systèmes réactifs - [bibtex]
1995
- Static Timing Analysis of Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
1994
- A Modular State/Transition Approach for Programming Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
- A Multiparadigm Language for Reactive Systems. Muriel Jourdan, Fabienne Lagnier, Pascal Raymond, Florence Maraninchi - In 5th IEEE International Conference on Computer Languages - [bibtex]
- Studying Synchronous Communication Mechanisms by Abstractions. Muriel Jourdan, Florence Maraninchi - IFIP Working Conference on Programming Concepts, Methods and Calculi - [bibtex]
- Etude d'un environnement de programmation et de vérification des systèmes réactifs, multi-langages et multi-outils. Muriel Jourdan - [bibtex]
1993
- Embedding declarative subprograms into imperative constructs. Muriel Jourdan, Fabienne Lagnier, Florence Maraninchi, Pascal Raymond - Fifth International Symposium on Programming Language Implementation and Logic Programming, \em Tallin, Estonia - [bibtex]
- Verifying quantitative real-time properties of synchronous programs. Muriel Jourdan, Florence Maraninchi, Alfredo Olivero - International Conference on Computer-Aided Verification (CAV) - [bibtex]
