Document d'Habilitation à Diriger des Recherches

Université Joseph Fourier - Grenoble I

Modélisation et validation des systèmes réactifs :
un langage synchrone à base d'automates

Florence Maraninchi

Résumé

Ce document décrit la conception du langage Argos. C'est un langage synchrone à syntaxe graphique, qui permet la description de systèmes réactifs sous forme de compositions de machines de Mealy. Le jeu d'opérateurs est en quelque sorte minimal: mise en parallèle, synchronisation par le mécanisme de diffusion synchrone commun à tous les langages synchrones, composition hiérarchique héritée des Statecharts. La composition parallèle de machines à états et la composition hiérarchique rendent réaliste la description de systèmes de taille conséquente par des systèmes d'états et de transitions explicites.

Nous décrivons la démarche de conception du langage : problèmes liés au choix des construc-
tions et à leur sémantique ; implantation efficace ; connexions du compilateur à divers outils de
vérification du domaine ; génération de code. Nous présentons également les extensions du lan-
gage proposées pour la spécification des systèmes temporisés, hybrides ou non-déterministes, et
les expériences de programmation multi-langages menées dans le cadre synchrone avec Esterel et
Lustre.

Nous montrons les relations étroites entre la définition d'Argos et certains aspects de l'ensei-
gnement de l'algorithmique en Deug.

Mots-clé:

Systèmes réactifs, langages synchrones, modélisation, programmation, validation, automates, Ar-
gos, algorithmique

Abstract

This document is about the design of the Argos language. It's a synchronous language, in which reactive systems are described as compositions of Mealy machines. The set of operators is in some sense minimal: the parallel composition; the synchronous broadcast common to all synchronous languages, as the communication mechanism; a hierarchic composition inspired from Statecharts. The parallel and hierarchic compositions allow the description of large systems by means of explicit states and transitions.

We described the design phases of the language: choice of the construct, and definition of their semantics; efficient implementation; connections of the compiler to a wide variety of available verification tools; code generation. We also mention the extensions towards timed, hybrid or non-deterministic systems, and the experience in multi-language programming in the synchronous framework: Argos+Lustre or Argos+Esterel.

We show relationships between the definition of Argos and the teaching of algorithmics.

Keywords:

Reactive Systems, synchronous languages, modelling, programming, validation, automata, Argos, algorithmics