# Chapitre 8

## Argos + Lustre via DC

Sources: La traduction d'ARGOS en systèmes d'équations booléennes avec conditions d'activations, publiée dans [MH96a], est déjà présentée dans la première partie (chapitre 5). Il reste à exposer les problèmes d'analyse de déterminisme et réactivité, la ré-initialisation des noeuds DC issus de LUSTRE (qui fait l'objet du mémoire de DEA de Traian Popovici) et le mécanisme de fusion des fichiers DC issus des compilateurs ARGOS et LUSTRE (ce dernier point constitue le sujet de magistère de Yann Rémond).

### 8.1 Structure des programmes et exemple

Dans [MH96a] nous avons réduit DC à sa plus simple expression. En réalité il s'agit d'un format assez riche, qui offre par exemple une notion de noeud analogue à celle de LUSTRE pour la structuration des programmes. Nous considérons également une syntaxe structurée d'ARGOS, qui offre la notion de *processus*. La traduction choisie est telle que l'on crée un noeud DC pour chaque *processus* ARGOS. La liaison entre les deux langages repose sur le mécanisme d'appel de noeud. Tout *processus* ARGOS peut être construit en utilisant un noeud défini dans le fichier LUSTRE. Inversement, tout noeud LUSTRE peut faire appel à un *processus* ARGOS. Chacun des fichiers est analysé par le compilateur adéquat, et l'on produit un ensemble de noeuds DC correspondant aux *processus* ARGOS, et un ensemble de noeuds DC correspondant aux noeuds LUSTRE. Le programme global doit bien sûr contenir tous ces noeuds.

La figure 8.1 donne un exemple très simple de programme mixte, dans lequel la structure principale est décrite en ARGOS. L'un des composants est un noeud LUSTRE, défini ci-dessous :

```
node L (x: bool) returns (y,z: bool)
var M: bool;
let
    M = x ->not pre(M) and x;
    y,z = A2 (M, x);
tel.
```

Lequel, lui-même, fait appel à un *processus* ARGOS A2 également donné figure 8.1.

La figure 8.2 donne l'arbre abstrait de ce programme, en montrant les sous-arbres LUSTRE et les sous-arbres ARGOS.
<figure><img src="image_37.png" /><figcaption>processus A2 (u, v)(w, t)</figcaption></figure>

<figure><img src="image_38.png" /><figcaption>FIG. 8.1 – *Un programme mixte LUSTRE+ARGOS (partie ARGOS)*</figcaption></figure>

<figure><img src="image_39.png" /><figcaption>FIG. 8.2 – *Arbre abstrait d’un programme mixte*</figcaption></figure>
<figure><img src="image_40.png" /><figcaption>FIG. 8.3 – *Programmation mixte* ARGOS+LUSTRE *via* DC</figcaption></figure>

## 8.2 Schéma de principe

La figure 8.3 donne le schéma de principe d'un environnement de programmation mixte ARGOS+LUSTRE, avec fusion au niveau DC. Le compilateur ARGOS produit naturellement des noeuds DC réinitialisables (cf. chapitre 5, il suffit de conserver les attributs hérités kill et alive comme paramètres de chaque noeud DC produit pour un processus ARGOS). Cette propriété permet d'intégrer le noeud dans un contexte comme le raffinement ARGOS, où il peut être lancé, interrompu, relancé dans son état initial. Le compilateur LUSTRE, en revanche, produit des noeuds DC non réinitialisables.

D'autre part, si le compilateur LUSTRE garantit que les ensembles d'équations des noeuds DC produits sont sans boucle, ce n'est pas le cas pour le compilateur ARGOS.

On introduit donc deux outils de modification des fichiers au format DC: un “débouleur”, et un outil de réinitialisation. Ces outils sont utilisés avant fusion, pour ne fusionner que des ensembles de noeuds à la fois non bouclés et réinitialisables. La fusion risque toutefois de réintro-duire des boucles (cf. ci-dessous). On doit donc appliquer le mécanisme de débouclage une fois encore.
## 8.3 Outil de débouclage des noeuds DC issus d'ARGOS

A l'échelle d'un noeud DC produit par compilation d'un processus ARGOS, on peut rassembler toutes les déclarations de signaux locaux (la syntaxe proposée au chapitre 6 ressemble d'ailleurs à celle de LUSTRE, où la déclaration des signaux locaux est toujours attachée à la définition d'un noeud). On peut donc considérer que le processus ARGOS n'a qu'une opération d'encapsulation, située à la racine.

On adapte la technique de l'outil BAC décrite au chapitre 5, paragraphe 5.2, qui produit : un ensemble d'équations non bouclées, et une condition nécessaire et suffisante portant sur les variables d'état et les signaux d'entrée, qui détermine dans quelles configurations le programme est à la fois déterministe et réactif. Cette condition est ajoutée à la partie *assertion* du noeud DC. Le débouclage étant nécessaire à chaque encapsulation, on l'applique à tout noeud DC issu d'ARGOS.

## 8.4 Réinitialisation des noeuds DC issus de LUSTRE

Pour être utilisé dans un raffinement ARGOS, un programme LUSTRE doit être rendu *réinitialisable*.

La transformation consiste à ajouter deux paramètres d'entrée *kill* et *alive*, avec la même signification qu'au chapitre 5 : *kill* signifie que le processus considéré est tué durant la réaction courante ; *alive* signifie qu'il participe à la réaction courante. On effectue ensuite les trois modifications suivantes :

- Ajouter le paramètre *alive* à toutes les conditions d'activation. Ainsi le noeud considéré ne calcule rien aux instants où *alive* est faux, s'il est placé dans un contexte qui peut l'activer et le désactiver.

- Ajouter une nouvelle variable locale *reset* définie par une mémorisation : $MEM(reset, kill, TRUE, FALSE)$. *reset* est vrai lorsque *kill* était vrai à l'instant précédent. *reset* détermine des instants où tous les objets doivent prendre leurs valeurs initiales.

- Modifier toutes les parties droites des définitions d'origine en tenant compte de *kill* et *reset*.

D'où :

**Equations:** En DC, la valeur $x_0$ des équations est utilisée au début, avant que le premier instant où C est vrai permette de définir $x$ en calculant $E$. $x$ vaut donc $x_0$ jusqu'au premier instant où C est vrai *exclu*. Dans un noeud DC réinitialisable, la valeur $x_0$ est utilisée dans les intervalles définis par une occurrence de *reset* et une occurrence de C. Lorsque C et *reset* sont simultanés, l'intervalle est vide et on n'a pas besoin de $x_0$, $x$ est tout de suite calculé d'après $E$. L'essentiel est de remplacer le recours à la valeur précédente de $x$ par $x_0$, lorsque le noeud est réinitialisé. Une équation $EQU(x, E, C, x_0)$ est donc remplacée par $EQU(x, \text{if } C \text{ then } E \text{ else } x_0, C \land alive \lor reset, x_0)$.

**Mémorisations:** En DC, la valeur $x_0$ des mémorisations est utilisée comme valeur intiale, avant toute affectation à $x$. $x$ vaut donc $x_0$ jusqu'au premier instant où C est vrai *inclus*. Dans un noeud DC réinitialisable, la valeur $x_0$ est utilisée dans les intervalles définis par une occurrence de *reset* et l'instant suivant une occurrence de C. Une mémorisation $MEM(x, E, C, x_0)$
est donc remplacée par
MEM($x$, if kill then $x_0$ else E, kill $\lor$ C $\land$ alive, $x_0$)

## 8.5 Un mécanisme d'édition de liens au niveau DC

L'édition de liens des ensembles de noeuds DC ayant subi les modifications ci-dessus consiste simplement à rassembler tous les noeuds. Pour que l'ensemble constitue un programme exécutable, il ne doit plus y avoir de noeud indéfini. D'autre part la structure des appels de noeuds ne doit pas présenter de cycle.

Enfin, et c'est le plus ardu, il peut apparaître de nouveaux cycles de définition de signaux, lors de la fusion des deux ensembles de noeuds. Il faut donc réaliser globalement une phase de débouclage.

## 8.6 Travaux de même nature

L'équipe d'Axel Poigné à la GMD (Sankt Augustin) travaille sur le projet Synchronie, dont l'un des objectifs est de définir et implanter un environnement de programmation synchrone basé sur LUSTRE, ESTEREL et ARGOS. Les membres de l'équipe ont pour cela réécrit la sémantique des trois langages en termes d'automates booléens, un format équationnel de définition d'automates, assez similaire à DC. La fusion des langages est réalisée au niveau des automates booléens. Cette réécriture des sémantiques s'accompagne de quelques modifications de fond, comme la suppression des variables en ESTEREL.

Ayant commencé avec des ambitions assez vastes — comme par exemple de réaliser une imbrication plus fine d'ARGOS et LUSTRE, dans laquelle les transitions ARGOS auraient porté des portions de programmes LUSTRE — ils semblent maintenant s'être ramenés à des choix semblables aux nôtres. Il semble pourtant difficile de profiter de leur travail, même en partie, puisque les formats, les langages et les compilateurs utilisés sont entièrement redéfinis.

## 8.7 Pour aller plus loin...

La technique de mélange de langages par un mécanisme d'édition de liens au niveau DC peut être poussée plus loin. On peut ainsi envisager de mêler ARGOS, LUSTRE et ESTEREL dans un schéma similaire à celui décrit plus haut. Un noeud DC issu des compilateurs LUSTRE ou ARGOS doit être équipé d'entrées et de sorties spécialisées, pour intégration dans un contexte ESTEREL quelconque. Même si l'on restreint ces contextes ESTEREL à des contextes d'appel de modules (c'est-à-dire sans récupération des exceptions), il faut prévoir 4 entrées go, resume, suspend et kill et deux sorties halt et term. Par exemple, le processus se réincarne lorsque go et res sont tous deux présents. Le contexte permet de déterminer le degré de réincarnation (c'est-à-dire le nombre d'instances simultanément vivantes) du processus que l'on placera dans ce contexte. Un noeud DC candidat à occuper ce contexte doit être modifié pour présenter autant d'exemplaires que nécessaire de ses signaux d'entrée.

Une version simplifiée pourrait consister à n'autoriser l'intégration dans un contexte ESTEREL de noeuds DC issus des autres compilateurs, qu'à la condition que le contexte soit sans réincarnation, ce qui peut être déterminé statiquement.
# Chapitre 9

## Argos + Esterel

Sources: *Les propositions pour un langage mixte ARGOS+ESTEREL présentées ici sont issues de discussions avec Gérard Berry et Nicolas Halbwachs, après que G. Berry eut fait état de préoccupations relatives à la syntaxe chez les utilisateurs d'ESTEREL (paragraphe "Motivations"). La version correcte des schémas de traduction structurelle est due en grande partie à N. Halbwachs. Ce travail n'est pas publié dans son intégralité. Il n'existe pour l'instant que sous forme de rapport de recherche embryonnaire, l'existence de travaux tout à fait similaires et plus accomplis (dernier paragraphe) nous ayant dissuadés de poursuivre la réflexion jusqu'à l'implantation.*

Le dernier paragraphe est tiré de réflexions tout à fait personnelles autour de la notion de causalité. L'interprétation de cette notion, et les conclusions qui en découlent, sont parfaitement indépendantes des motivations et de la traduction proposée.

### 9.1 Motivations

Le mélange ARGOS+ESTEREL répond bien sûr aux motivations générales exposées au chapitre 7, complétées par ce qui suit:

**Du point de vue d'ESTEREL:** Dans un programme ESTEREL, les structures de contrôle temporelles comme le chien de garde (watching) et la détection d'exception (trap) définissent des contextes de préemption imbriqués. La syntaxe textuelle d'ESTEREL ne montre pas toujours assez explicitement les interactions entre une suite d'instructions et son contexte de préemption. Dans les langages séquentiels, il est possible de comprendre le corps d'une itération en s'abstrayant de la condition de continuation. En revanche, un chien de garde ESTEREL interagit avec son corps à *tout instant* de l'exécution de celui-ci. La compréhension d'une portion de programme exige donc la lecture de toutes les structures de contrôle englobantes, qui peuvent être assez éloignées dans le texte, et dont l'imbrication n'est manifeste que dans l'indentation. Une syntaxe graphique pourrait peut-être rendre la structure des programmes plus lisible.

D'autre part, dans un contexte de description impérative des systèmes réactifs, on rencontre souvent des systèmes dont la description la plus naturelle est donnée sous forme d'automate. Il n'y a pas de moyen simple pour décrire une telle machine, de manière lisible, avec les structures d'ESTEREL. La traduction systématique d'un automate en programme ESTEREL, proposée plus loin, permet de s'en convaincre.
**Du point de vue d'ARGOS :** Les syntaxes graphiques doivent se contenter d'un nombre assez restreint de caractères (formes, couleurs, positions) significatifs. Une syntaxe graphique devient rapidement illisible par accumulation de caractères. Dans le cas d'ARGOS, il ne serait guère raisonnable par exemple de distinguer des états carrés ou rectangulaires, à coins carrés ou arrondis, à trait épais ou fin, etc. Le nombre de constructions syntaxiquement distinguables est donc réduit. D'autre part la taille d'un écran ou d'une feuille de papier impose des limitations de taille aux portions de programmes qui doivent être lues d'un seul bloc, et il s'avère en général que, pour la même limitation de taille, une syntaxe graphique offre moins d'information qu'une syntaxe textuelle.

Toutes ces raisons font qu'un programme ARGOS de moyenne complexité est assez encombrant (jeu de construction réduit et syntaxe peu concise). D'autre part l'utilisation des deux dimensions que permet une syntaxe graphique est intéressante quand il s'agit de visualiser les structures de contrôle emboîtées qui constituent l'architecture globale d'un programme, mais dans la description des détails, lorsqu'il s'agit finalement de décrire des enchaînements d'actions simples, on aimerait se ramener à une syntaxe textuelle plus économique. Enfin les constructions d'ARGOS représentent un sous-ensemble des primitives d'ESTEREL, et même si les primitives manquantes peuvent être reconstruites, cela rend les programmes peu concis et moins lisibles. Mêler des portions de code ESTEREL aux programmes ARGOS pourrait apporter une solution à ces problèmes.

## 9.2 Proposition : ARGOS+ESTEREL

Du point de vue langage, notre proposition peut être vue de deux manières : 1) comme une extension d'ARGOS par quelques structures d'ESTEREL permettant de réduire la taille des programmes, dans des cas bien connus ; 2) comme l'ajout à ESTEREL d'une structure de contrôle temporelle supplémentaire basée sur l'idée du raffinement ARGOS. D'un point de vue pratique, nous proposons de traduire le langage mixte en ESTEREL, pour bénéficier en aval de tout l'environnement de programmation ESTEREL (génération de code, simulation, débogage symbolique, systèmes de validation, ...).

Les propositions portent sur des extensions indépendantes les unes des autres, parmi lesquelles il devrait être possible de choisir librement. Nous étudions toutefois les interactions entre extensions, là où elles risquent de rendre le langage incompréhensible ou ambigu.

### 9.2.1 Préemption forte ou faible

En ARGOS, la structure de préemption définie par le raffinement correspond à la préemption faible d'ESTEREL : prendre une transition issue d'un état *X* raffiné par *P* détruit *P*, mais il peut encore exécuter une de ses propres réactions dans la réaction globale qui le détruit (ses "dernières volontés" sont prises en compte). Cette caractéristique est nécessaire à l'expression des "suicides", dans lesquels le processus raffinant *P* demande à être détruit, en exécutant une transition qui émet un signal dédié, lequel déclenche une transition issue de l'état raffiné *X*.

Toutefois, de nombreux cas requièrent l'utilisation d'une structure de préemption **forte**, dans laquelle le processus ne réagit pas pendant la réaction qui le détruit. Pour un exposé des différentes notions de préemption dans les systèmes réactifs, voir [Ber93].
En ESTEREL, la préemption forte d'un processus P par un signal S est liée à la structure `do ... watching ...`. La préemption faible est construire à l'aide de la structure `trap T ... in ... exit T ... end`<fnref n="1" />.

On écrit donc :

<table><tr><td>do</td><td>[ P; exit T ]</td></tr><tr><td>P</td><td>||</td></tr><tr><td>watching S</td><td>[ await S; exit T ]</td></tr><tr><td></td><td>end T</td></tr></table>

Nous avons montré au chapitre 2, section 2.4.1, que la préemption forte peut être construite à partir de la préemption faible, en utilisant l'opération de définition d'horloge. Au chapitre 6, nous proposions même de définir pour cela une macro-notation.

Dans le langage mixte `ARGOS+ESTEREL`, nous proposons une syntaxe particulière pour la préemption forte, qui sera traduite directement en structure de préemption forte d'ESTEREL, sans passer par la construction à base d'horloge.

<figure><img src="image_41.png" /><figcaption>FIG. 9.1 – *Notations des préemptions faible et forte. Le triangle plein (resp. creux) dénote une préemption forte (resp. faible)*</figcaption></figure>

### 9.2.2 Terminaison implicite

En `ARGOS`, il n'y a pas de notion implicite de terminaison d'un sous-programme. En particulier les machines de Mealy qui constituent les composants de base des programmes, si elles ont nécessairement un état *initial* distingué, n'ont pas d'état(s) final(s). D'autre part toute machine est réactive, et on ne peut utiliser la notion de *puits* pour déterminer des états de terminaison. En `ESTEREL` au contraire, la notion de terminaison est implicite : toute portion de programme se termine, sauf *halt* et les boucles. Les instructions élémentaires ont un début et une fin bien identifiés, et toute construction définit la terminaison du programme construit en termes des terminaisons des composants. Par exemple, la composition parallèle de *n* programmes se termine lorsque chacun des composants a terminé — les composants "s'attendent" les uns les autres et la terminaison de l'ensemble est simultanée à la terminaison du (ou des) dernier(s) d'entre eux. Cette synchronisation implicite des composants d'une mise en parallèle doit être explicitement construite en `ARGOS`, et si l'on matérialise l'attente de chacun des composants par un état, la taille de la construction obtenue est une fonction exponentielle du nombre de composants parallèles. En utilisant l'équivalent du *sustain* `ESTEREL`, c'est-à-dire l'émission continue d'un signal, on évite cette explosion du nombre d'états.

**Exemple 9.1 : Construction de la terminaison des compositions parallèles**

<footnote n="1">1. En `ESTEREL v5`, ces deux structures sont notées `abort ... when` et `weakabort ... when`.</footnote>
On considère un système à *n* signaux d'entrée *a*₀, *a*₁, ..., *a*ₙ₋₁, qui émet un signal de sortie *o* dès qu'au moins une occurrence de chacun de ces signaux d'entrée est apparue. Pour *n* = 3 on écrit en ESTEREL :

Module M:
inputs a0, a1, a2;
outputs o;
    [ await a0 || await a1 || await a2 ] ;
emit o
end.

En ARGOS il y a essentiellement deux solutions.

Dans la première, on écrit trois processus à une transition de la forme *a*ᵢ/*end*ᵢ, et on les compose en parallèle avec un synchroniseur ternaire, qui attend les trois signaux “end” et émet *o*. La figure 9.2 donne une version simplifiée de ce synchroniseur, dans le cas où les terminaisons des différents processus ne sont jamais simultanées (pour prendre en compte d'éventuelles terminaisons simultanées, il faut ajouter tous les “raccourcis” de deux ou trois transitions).

<figure><img src="image_42.png" /><figcaption>FIG. 9.2 – Synchroniseur ternaire</figcaption></figure>

La deuxième solution évite l'explosion des états. Les processus à composer sont donnés par :

<figure><img src="image_43.png" /><figcaption>FIG. 9.3 – Construction de la terminaison par émission continue d'un signal</figcaption></figure>

Et le synchroniseur ternaire observe simplement l'occurrence simultanée des signaux “end₁”, “end₂” et “end₃”. Il a donc une unique transition end₁∧ end₂∧ end₃/o. ☐
<figure><img src="image_44.png" /><figcaption>FIG. 9.4 – Syntaxe pour la terminaison : les transitions de terminaison du processus raffinant ne conduisent pas à un véritable état : on les dessine terminées par un petit cercle ; la récupération de la terminaison par le processus raffiné est dénotée par une transition dont l'origine porte le même petit cercle.</figcaption></figure>

La deuxième construction illustrée par l'exemple ci-dessus est peu coûteuse, mais elle n'est pas modulaire : si l'on ajoute un composant numéro 4 qui se comporte comme les trois premiers, le synchroniseur doit être modifié pour réagir à $end_1 \land end_2 \land end_3 \land end_4$. Il est donc intéressant d'introduire la terminaison comme notion implicite.

Pour introduire la terminaison implicite dans ARGOS, on doit permettre de dénoter la terminaison des processus élémentaires. On doit également prévoir de dénoter des transitions particulières dans les automates contrôleurs de raffinements, déclenchables sur terminaison du processus raffinant. Ces transitions ne peuvent être que des préemptions faibles (le processus raffinant doit réagir, précisément pour signaler sa terminaison) et elles ont une condition d'entrée réduite à true (On peut aussi autoriser plusieurs transitions de récupération de la terminaison, à condition que leurs conditions soient deux à deux exclusives et que la disjonction de leurs conditions donne true). La figure 9.4 donne un programme qui émet X chaque fois qu'il a reçu une entrée a et deux entrées b.

Charles André propose pour les SyncCharts (voir paragraphe 9.5 ci-dessous pour plus de détails) une notion d'état "accepteur" plutôt que terminal. C'est une extension très intéressante qui permet de décrire des cas où la terminaison est définie de manière distribuée. Dans l'extension proposée ci-dessus, comme en ESTEREL, chaque processus élémentaire séquentiel a un état terminal parfaitement défini, et la terminaison d'une composition parallèle ne peut être définie que comme la terminaison de tous les processus. Ch. André donne l'exemple d'un compteur modulo 8 où la valeur 5 constitue l'état terminal. Si ce compteur est décrit par un unique automate (ou, en ESTEREL, un unique processus séquentiel), il est fort simple de définir la terminaison comme désiré. Si l'on code le compteur par la composition parallèle de trois compteurs 1 bit (c'est l'exemple 2.1 donné au chapitre 2), la situation terminale est décrite par l'état global One/Zero/One. Pourtant aucun des trois états de base ne peut être déclaré terminal dans sa composante.

En ESTEREL ou en ARGOS étendu comme ci-dessus, la terminaison implicite ne permet pas d'exprimer cette terminaison distribuée. On la code toutefois facilement par le mécanisme proposé dans l'exemple ci-dessus, où chaque état accepteur émet continuellement le signal de terminaison de sa composante.
### 9.2.3 Priorités de transitions

Les machines de Mealy qui constituent les composants de base des programmes ARGOS doivent être déterministes, et cela exige que les conditions booléennes des transitions issues d'un même état soient deux à deux exclusives. Nous avons vu au chapitre 6 comment relâcher quelque peu cette contrainte en proposant des conventions raisonnables d'écriture abrégée des conditions booléennes. Toutefois, dans le cas général, cette exigence de déterminisme peut conduire à écrire des conditions complexes.

**Exemple 9.2**

Considérons un système qui, dans son état $A$, doit prendre une transition $t_1$ lorsque le signal $a_1$ survient, sinon une transition $t_2$ lorsque $a_2$ survient, sinon... etc. La transition $t_1$ a pour condition $a_1$, la transition $t_2$ a pour condition $\neg a_1 \land a_2$, puis $\neg a_1 \land \neg a_2 \land a_3$, etc. □

Dans de tels cas, il pourrait être plus simple de permettre une notation syntaxique de l'ordre de priorité entre transitions, au lieu de s'en remettre à l'expression des conditions. La condition d'une transition serait alors implicitement renforcée par la négation des conditions de toutes les transitions plus prioritaires.

Dans un langage séquentiel, la priorité serait exprimée par l'ordre des conditions (la plupart des constructions de type `CASE` ont une interprétation séquentielle: la structure `switch` de C, la fonction `cond` de LISP et de ses dérivés, ...). Dans un langage graphique dont la syntaxe est à deux dimensions, définir un ordre sur les transitions par des critères de position (par exemple décider que les transitions issues d'un état sont ordonnées en fonction de la position de leur point de départ sur l'état, dans le sens trigonométrique) peut imposer des contraintes de placement assez pénibles. Nous proposons donc de numéroter les transitions.

### 9.2.4 Activation sur initialisation

En ARGOS, tout programme ou sous-programme a un état initial, non une transition initiale, comme en ESTEREL. D'un point de vue global, cette contrainte empêche de décrire un système qui, avant d'accepter des entrées, réalise quelques actions et émet quelques signaux destinés à installer une configuration initiale de l'environnement. Cet inconvénient est toutefois contournable en décrivant des systèmes munis d'un état initial fictif, et dont la première transition est en quelque sorte spontanée (sa condition est `TRUE`, et la transition est donc activable à chaque passage dans la boucle d'exécution décrite en introduction). L'activation de cette première transition réalise les actions désirées.

D'un point de vue local, c'est-à-dire concernant les sous-programmes, cela explique pourquoi les processus raffinants ne réagissent pas dans la réaction qui les lance, alors qu'ils réagissent éventuellement dans la réaction qui les détruit. Cette dissymétrie de comportements a quelques inconvénients illustrés par l'exemple suivant.

**Exemple 9.3 : Réaction initiale et choix de l'état initial**

Considérons un système à deux modes `Running` et `Stopped`. Lorsqu'il reçoit une question $q$, il répond par $y$ dans l'état `Running` et par $n$ dans l'état `Stopped`. Le mode peut changer sur occurrence d'un signal `change`. Dans un système plus complexe, on peut avoir besoin de plusieurs instances de ce système simple, certaines dont l'état initial est `Running`, d'autres dont l'état initial est `Stopped`. Il est bien sûr possible de décrire deux systèmes de ce type, en changeant l'état initial. Mais on pourrait se contenter d'une version *paramétrée*, en quelque sorte dynamiquement, par
une réaction initiale capable de choisir l'état initial. La figure 9.5 donne un tel système (en cas d'occurrence simultanée de la question *q* et du signal de changement de mode *change*, le système émet *y* et *n*. On pourrait bien sûr éviter ce comportement par l'expression de priorité entre transitions).

<figure><img src="image_45.png" /><figcaption>FIG. 9.5 – Réaction initiale et choix de l'état initial</figcaption></figure>

☐

La réaction initiale des sous-programmes permet donc, en particulier, le choix de l'état initial, et accroît la réutilisabilité des composants. Cette extension offre la puissance des transitions inter-niveaux entrantes des Statecharts, tout en préservant une structure propre des programmes.

On trouvera dans [JM94a, MV92a] la description de l'interface boutons d'une montre plus complexe qu'à l'ordinaire — les boutons peuvent avoir des significations différentes selon la durée d'appui, et l'on y trouve une notion analogue au double click souris — utilisant une structure de raffinement avec initialisation. Cette opération est d'ailleurs implantée dans le compilateur ARGOS actuel, mais souffre d'une étude imparfaite des problèmes de réincarnation posés par son utilisation générale. Lorsqu'on exécute une transition qui est une boucle sur un état raf-finé, le processus interne existe simultanément en deux exemplaires: une instance en train de mourir, qui a droit à une ultime réaction, et une instance en cours de création, qui a droit à une réaction initiale. Ces deux instances sont décrites par la même portion de programme, mais la sémantique doit décrire comment cette portion de programme est dupliquée en deux objets aux évolutions potentiellement distinctes. La difficulté majeure provient des signaux locaux à ce processus "réincarné".

Nous proposons ici d'introduire les réactions initiales sous forme de transitions initiales dans les automates. Syntaxiquement, un automate peut avoir plusieurs transitions étiquetées et maté-rialisées par des flèches sans origine, portant des conditions deux à deux exclusives (ou ordonnées selon un ordre de priorité), et couvrant le domaine des entrées ; autrement dit la disjonction des conditions de ces transitions doit donner **true**. La traduction structurelle en ESTEREL permet de ne pas se préoccuper des problèmes de réincarnation, puisqu'ils sont résolus dans les compi-lateurs récents [Ber91] (en ESTEREL la réincarnation provient des déclarations de signaux dans une structure **loop**).
## 9.2.5 Etats transitoires

### 9.2.5.1 Séquence et états transitoires

La dernière construction d'ESTEREL qui nous intéresse, parce qu'elle est difficile à construire en ARGOS, est la séquence dans l'instant. L'introduction d'un mécanisme de détection de la terminaison permet d'enchaîner plusieurs processus séquentiellement, mais la séquence dans l'instant n'existe en ARGOS que sous une forme très particulière.

Pour un programme ARGOS réduit à un automate, toute réaction est constituée d'exactement une transition. Il y a donc identification parfaite entre les états syntaxiques (ceux de l'automate) et les états sémantiques, c'est-à-dire les états stables du système, à l'exécution. Il semble que ce soit une propriété importante lorsque l'on est habitué à concevoir des systèmes sous forme d'automates.

Les terminaisons intempestives sont codées par un mécanisme de suicide. Le processus raffinant exécute une transition $t'$ et émet un signal $\alpha$ qui déclenche une transition $t$ issue de l'état raffiné. Cette transition le tue, donc. On fait ainsi apparaître des états transitoires. En effet, l'état but de la transition $t'$ ne correspond à aucun état stable de l'exécution. Dans la version compilée, il n'apparaît plus, d'ailleurs. (Si l'on généralise le raffinement pour autoriser une réaction initiale du processus lorsqu'il est lancé, son état initial devient également transitoire).

Le dialogue instantané (voir l'exemple 3.1 au chapitre 3) demande une séquence dans l'instant, et s'écrit en ESTEREL :

```
[ present C then emit Q; present Y then ... ]
|
[ ... present Q then emit Y ... ]
```

En ARGOS on doit exprimer cette séquence par un raffinement. L'état transitoire du processus raffinant correspond à l'état du programme ESTEREL au niveau du point-virgule.

Toutefois un codage systématique des séquences d'ESTEREL par des raffinements ARGOS produit rapidement des niveaux d'imbrication prohibitifs. D'où l'idée de généraliser la notion d'état transitoire. Le dialogue instantané s'écrirait en ARGOS comme illustré figure 9.6. L'état en pointillé est transitoire : une transition qui y mène peut (ou doit?) être exécutée simultanément avec une transition qui en sort. La transition d'étiquette $C/Q$ s'enchaîne donc naturellement avec la transition $Y$. Les états transitoires ne doivent pas non plus constituer des puits, et il faut donc prévoir explicitement la transition par $\neg Y$ ; de plus cette transition n'est pas une boucle, au contraire de la transition $\neg C$, qui peut être omise.

Il est possible de transformer une machine à états transitoires en machine ordinaire, sans état transitoire, au risque de provoquer une explosion du nombre des transitions. En effet, il suffit de supprimer les états transtotoires, et d'écrire explicitement tous les enchaînements possibles de transitions, entre deux états non transitoires. Il faut pour cela que la machine soit dépourvue de cycles d'états transitoires. On retrouve la condition de correction des structures de boucles d'ESTEREL : les boucles en temps nul sont rejetées.

Les états transitoires peuvent ainsi être utilisés pour coder les transitions "branchues" des Statecharts. Ces transitions représentent des arbres de décision sur les signaux. La figure 9.7 en donne un exemple. l'utilisation de branches (a) permet une notation concise des conditions de (b), dans le style des BDD.

La traduction en ESTEREL utilise le mécanisme de traitement immédiat des signaux.
<figure><img src="image_46.png" /><figcaption>FIG. 9.6 – *Expression du dialogue instantané grâce à un état transitoire*</figcaption></figure>

<figure><img src="image_47.png" /><figcaption>FIG. 9.7 – *Utilisation des états transitoires pour le codage des transitions branchues*</figcaption></figure>
### 9.2.5.2 Raffinement des états transitoires

Les difficultés surviennent lorsque l'on tente d'utiliser de telles machines à états transitoires comme composants de programmes ARGOS. Peut-on raffiner un état transitoire ? Si oui, doit-on obligatoirement le raffiner par un processus qui se termine toujours dans l'instant ?

Nous n'avons pas poursuivi la réflexion plus loin. Il nous a semblé que le raffinement des états transitoires était un cas typique de construction intuitivement non justifiable. Restreindre l'utilisation des états transitoires aux composants de base non raffinés est une contrainte suffisante. Il est peut-être possible de la relâcher quelque peu, mais il faudrait pour cela étudier de nombreux exemples.

## 9.3 Schémas de traduction structurelle en ESTEREL

La compréhension détaillée des schémas de traduction présentés ici suppose une connaissance assez poussée du langage ESTEREL. Une introduction assez détaillée pour permettre au lecteur complètement novice de comprendre ces schémas ne peut, à l'évidence, être incluse dans ce document.

Toutefois nous tentons d'illustrer l'idée générale de ces schémas de traduction, qui est de fournir un cadre assez souple de traduction des machines de Mealy, tel que la prise en compte de l'une ou l'autre des extensions proposées ci-dessus soit réalisable par des modifications ponctuelles. Nous essaierons, autant que possible, de donner l'intuition des modifications introduites.

Pour un processus ARGOS P, notons [[P]] sa traduction en ESTEREL. La traduction est telle que, pour tout opérateur n-aire op d'ARGOS, [[op(P₁, ..., Pₙ)]] = [[op]]([([P₁])], ..., [[Pₙ]]).

Cette propriété est essentielle. C'est sur elle que repose la justification d'un mélange ARGOS+ESTEREL au niveau source: on pourra par exemple écrire un programme ESTEREL et l'utiliser pour raffiner un état d'automate ARGOS.

Nous esquissons ci-dessous le schéma de traduction qui permet de traduire simplement toutes les constructions d'ARGOS en ESTEREL, de manière structurelle, et se prête bien à l'introduction des extensions proposées ci-dessus.

### 9.3.1 Composants de base

Considérons une machine de Mealy $M = (S, \sigma_0, I, O, T)$. La traduction utilise un ensemble de signaux auxiliaires $\{go_\sigma | \sigma \in S\}$, un pour chaque état $\sigma$ de la machine. Le signal $go_\sigma$ sera émis chaque fois qu'une transition qui active l'état $\sigma$ est exécutée.

[[M]] est un module ESTEREL de la forme :

```module M:
input { s | s \in I - 0 };
output { s | s \in O - I };
inputoutput { s | s \in I \cap O };
signal { go_\sigma | \sigma \in S } in
    emit go_{\sigma_0} ; || P_\sigma
end.
```

Le corps du module commence par l'émission du signal qui active l'état initial $\sigma_0$ de S. On trouve ensuite la composition parallèle des processus $P_\sigma$ pour $\sigma \in S$, qui décrivent les états de la
machine. Chaque P<sub>σ</sub> est de la forme :

loop
    await immediate go<sub>σ</sub>;
    trap OUT<sub>σ</sub> in
        halt

$$ \parallel_{t=(\sigma,-,-,-) \in T} \parallel Q_t $$
end

end

L'instruction `halt` est ici inutile, mais elle sera remplacée par un programme, lorsque l'automate sera raffiné.

Finalement le codage $Q_t$ d'une transition $t = (\sigma, \varphi, e, \sigma') \in T$ est de la forme :
await $\varphi$; emit $e$; emit $go_{\sigma'}$; exit $OUT_{\sigma}$.

Le programme attend l'événement décrit par $\varphi$, puis émet les signaux de l'ensemble de sortie $e$, et le signal $go_{\sigma'}$ qui active l'état but de la transition, puis sort de la structure `trap OUT<sub>σ</sub>...`", ce qui désactive l'état source $\sigma$. Notons que, si la transition est une boucle (c'est-à-dire $\sigma = \sigma'$), la portion de programme qui décrit l'état $\sigma$ est simultanément réactivée, conformément à la sémantique d'ARGOS.

La notation `await \varphi` doit être comprise comme une abréviation de :

- `halt` si $\varphi = FALSE$

- `await tick` si $\varphi = TRUE$

- `await [[\varphi]]` sinon, avec : $[[x]] = x$, $[[\neg \varphi]] = \text{not} [[\varphi]]$, $[[\varphi_1 + \varphi_2]] = [[\varphi_1]] \text{ or } [[\varphi_2]]$ and $[[\varphi_1 \cdot \varphi_2]] = [[\varphi_1]]$ and $[[\varphi_2]]$.

Ce choix de codage des transitions issues d'un même état appelle deux remarques.

Tout d'abord, on notera que les portions de programme codant les différentes transitions sont composées en *parallèle*, ce qui permet de ne pas imposer de priorité statique entre elles (ce qui serait le cas si on les traduisait par des structures de chien de garde nécessairement emboîtées). Cet aspect de la traduction est essentiel pour respecter la sémantique d'ARGOS. En effet, il y a un côté *declaratif* plutôt qu'impératif dans l'interprétation de l'ensemble de transitions issues d'un même état : aucun ordre n'est imposé entre elles. Cette réflexion motivait d'ailleurs le titre "An experience in compiling a mixed declarative/imperative language for reactive systems" de l'article [MV92b] dans lequel nous décrivions l'utilisation des BDD dans le compilateur ARGOS.

Le deuxième point important concerne le codage des transitions, individuellement. On traduit la structure $\varphi/e$ par une structure séquentielle d'ESTEREL : `await \varphi; emit e`, qui introduit une dépendance entre l'émission de $e$ et la présence ou l'absence des signaux qui déterminent l'événement $\varphi$. En ESTEREL ces dépendances entre signaux (déduites des structures séquentielles, conditionnelles, ou des structures de contrôle temporelles) forment la base de la définition de la notion de *causalité* des programmes. Ces dépendances conduisent parfois à rejeter, selon des critères de causalité, un programme ESTEREL obtenu par traduction d'un programme ARGOS, alors même que ces critères n'ont pas de sens en termes du programme ARGOS d'origine. Le paragraphe 9.6 ci-dessous précise ces idées.
## 9.3.2 Traduction des constructions d'ARGOS

La traduction des constructions d'ARGOS est directe: la mise en parallèle est traduite en mise en parallèle ESTEREL; l'encapsulation en structure de déclaration *signal ... in ... end*; la définition d'horloge en structure *suspend ... when ...*. Le raffinement d'une machine *M* par un ensemble de processus $P_\sigma$ est obtenu en remplaçant, dans la traduction ci-dessus de la machine *M*, l'instruction *halt* de $P_\sigma$ par *run R_\sigma*, où $R_\sigma$ est un module ESTEREL quelconque, écrit directement en ESTEREL ou issu de la traduction d'un autre programme ARGOS.

## 9.3.3 Traduction des extensions proposées

### 9.3.3.1 Préemptions faible et forte

La traduction en ESTEREL vise à préserver une certaine symétrie parmi les différents types de transitions: aucune priorité n'est imposée a priori entre les transitions qui représentent des préemptions faibles et celles qui représentent des préemptions fortes. Nous montrons au paragraphe 9.3.3.3 que cela permet d'éviter l'introduction de "faux" problèmes de causalité.

On ne change que le codage $P_\sigma$ d'un état $\sigma$. Dans la suite, nous noterons $R_\sigma$ le codage du processus raffinant l'état $\sigma$, s'il y en a un, et l'instruction *halt* sinon.

loop
    await immediate go_σ;
    signal weak, strong in
        trap OUT_σ in
            do
                run R_σ
            ||
                await weak; exit OUT_σ
            watching strong timeout exit OUT_σ end
        ||
            ||
            t=(σ,−,−,−)∈T Q_t
    end trap
end signal
end loop

et les codages de transitions $Q_t$, $t = (\sigma, \varphi, e, \sigma') \in T$, sont de la forme :

await $\varphi$; emit e; emit go$_{\sigma'}$;
emit { weak si la transition est faible
      strong si la transition est forte

### 9.3.3.2 Terminaison

Ici on ne change que la structure générale du module qui code une machine raffinée. Le corps du module précédemment défini est englobé dans une construction *trap*:

module M:
input ...
output ...
inputoutput ...
signal... in
trap TERM in
    emit go<sub>σ₀</sub> ; ||| P<sub>σ</sub>
end trap
end.

Une transition de terminaison de l'un des processus raffinants doit simplement être traduite en ESTEREL par une séquence d'instructions qui se termine par exit TERM, au lieu de l'émission du signal go de son état but.

La récupération de la terminaison par l'automate contrôleur d'un raffinement est réalisée en deux points: on introduit un signal term_σ local au programme d'un état σ, et on fait suivre l'instruction run R_σ de lancement du processus qui raffine σ de l'instruction emit term_σ. Dans le programme de traitement des transitions, les transitions spéciales de récupération de la terminaison doivent être conditionnées par la présence de term_σ, ce qui donne donc: await ϕ and term_σ; emit e; emit go_σ'; exit OUT_σ. comme codage d'une transition de terminaison t = (σ, ϕ, e, σ') ∈ T.

### 9.3.3.3 Priorités de transitions

La traduction en ESTEREL des niveaux de priorité est directe, puisqu'il existe dans ce langage une structure de type CASE à interprétation séquentielle. Il suffit de considérer que les portions de programme qui codent les transitions issues d'un même état ne sont plus en parallèle mais structurées par un case:

await
    case ϕ₁ do emit e₁; emit ...
    ...
    case ϕₙ do emit eₙ; emit ...
end

Cette traduction est compatible avec l'utilisation de transitions de terminaison, et avec l'expression de préemptions fortes ou faibles. Il faut toutefois noter que donner une plus grande priorité à une transition de préemption faible, qu'à une transition de préemption forte, a de fortes chances de conduire à des problèmes de causalité assez subtils.

### 9.3.3.4 Réaction initiale

Dans le schéma de traduction d'une machine de Mealy, il suffit de remplacer l'instruction emit go<sub>σ₀</sub> qui permettait de définir l'état initial, par un traitement de transition initiale. Si les conditions des transitions initiales sont exclusives, on obtient par exemple:

[
    present ϕ₁ then
    emit e₁;
    emit go<sub>σ'₁</sub>
end
|| ... 
|| present $\varphi_n$ then
        emit $e_n$;
        emit $g\sigma'_n$
end
]

## 9.4 Preuve de conformité

La traduction d'ARGOS étendu en ESTEREL en donne une sémantique formelle, puisqu'ESTEREL dispose d'une sémantique formelle.

Pour le langage ARGOS de base, il serait bon de comparer la sémantique usuelle par compilation en machines de Mealy, à la sémantique définie par traduction en ESTEREL. C'est très certainement une preuve par induction structurelle assez lourde, mais sans véritable difficulté autre que la notion de correction des programmes. Le paragraphe 9.6 ci-dessous expose les problèmes.

## 9.5 Travaux de même nature

### 9.5.1 Les SyncCharts

Charles André et son équipe (Université de Nice) travaillent à la définition du langage SyncCharts [And96, AG95]. C'est un langage graphique à base d'automates hiérarchiques comme en ARGOS, qui hérite de certaines constructions ESTEREL — modes de terminaison, réaction initiale des processus raffinants, traitement immédiat des signaux — et de constructions du Grafcet — association de l'émission d'un signal à un état, inhibition de processus par un signal, etc. L'ensemble est traduit en ESTEREL.

### 9.5.2 Synopsys

Joe Buck chez Synopsys travaille sur une extension d'ARGOS dans laquelle on retrouve essentiellement les différents types de transitions associés aux modes de terminaison ESTEREL (terminaison normale, préemptions faible et forte) et la réaction du processus raffinant lors de son activation. L'ensemble est traduit en ESTEREL.

## 9.6 Comparaison des notions de causalité en ARGOS et ESTEREL

### 9.6.1 Un point de vue sur la causalité

Nous avons vu au chapitre 2 comment interpréter l'encapsulation ARGOS en termes de systèmes d'équations booléennes à résoudre pour déterminer le statut des signaux locaux. Au chapitre 5 nous montrons comment traduire l'ensemble des constructions d'ARGOS en équations booléennes. Il existe pour ESTEREL "pur" (c'est-à-dire réduit aux booléens) une traduction complète en systèmes d'équations booléennes [Ber91].

L'exigence de déterminisme et de réactivité des programmes décrits s'exprime, comme pour ARGOS, par le fait que ces systèmes d'équations doivent avoir une solution unique. Le statut des
signaux locaux — sur lesquels repose la synchronisation entre composants par diffusion synchrone — doit être parfaitement déterminé, pour tout état, pour toute configuration des signaux d'entrée.

L'exigence de *causalité* des programmes — le terme a été introduit pour ESTEREL — va plus loin. Une manière de voir les choses est de dire qu'un programme est non causal si le système d'équations sous-jacent, qui définit le statut des signaux locaux, admet des solutions inexplicables en termes des structures syntaxiques du langage. On voit là que la notion de causalité ne peut qu'être dépendante du langage.

## 9.6.2 Comment définir une notion de causalité pour ARGOS ?
une conjecture...

Dans l'état actuel de la sémantique proposée pour ARGOS, il n'y a pas de notion de *causalité*. La sémantique se contente de définir une notion de programme incorrect vis-à-vis du déterminisme ou de la réactivité. L'implantation qui utilise l'outil BAC (cf. chapitre 5) permet d'affaiblir quelque peu les critères sans remettre en cause l'exigence de déterminisme et réactivité. On accepte toujours tout programme qui définit complètement l'état but et les signaux émis, dans tout état accessible, pour tout événement d'entrée.

Le besoin éventuel d'une notion de causalité (c'est-à-dire de critères plus forts que la simple exigence de déterminisme et réactivité) apparaît lorsque l'on considère des programmes comme le dialogue instantané décrit au chapitre 3, page 47. Dans la version (b), il est impossible d'expliquer la transition globale par un enchaînement de transitions élémentaires, ce qui peut paraître curieux. Cette remarque pourrait conduire à adopter la sémantique décrite pour les "réactions en chaîne" (toujours au chapitre 3) dans laquelle, outre l'existence d'une solution unique au système d'équations qui définit le statut des signaux locaux, on exige l'existence d'un ordre entre les transitions des composants de base. Le dialogue instantané ne peut alors s'écrire qu'avec un raffinement. ce choix aurait pour avantage de fournir une explication très simple de la non causalité d'un programme en termes de structures syntaxiques d'ARGOS.

D'autre part, si l'on traduit ARGOS en ESTEREL, on hérite nécessairement de la notion de causalité d'ESTEREL. Lorsqu'une traduction est rejetée par le compilateur ESTEREL, il faudrait savoir le justifier en termes des structures syntaxiques d'ARGOS. Cela risque d'être compliqué, ou artificiel.

La causalité d'ESTEREL repose sur une interprétation en logique constructive des systèmes d'équations booléennes qui définissent le statut des signaux locaux. Si l'on pouvait montrer que cette notion coïncide avec la sémantique par enchaînement de transitions élémentaires mentionnée ci-dessus, cela donnerait une notion solide de causalité pour ARGOS, et autoriserait la compilation par traduction en ESTEREL. Rappelons que la traduction d'ARGOS en IC (format intermédiaire du compilateur ESTEREL antérieur à l'analyse de causalité) avait été abandonnée en 1990, essentiellement parce que le compilateur V3 exhibit des erreurs de causalité incompréhensibles au niveau du source ARGOS.

Observons un exemple, figure 9.8.
<figure><img src="image_48.png" /><figcaption>FIG. 9.8 – *Dépendances entre signaux résolues par calcul booléen classique*</figcaption></figure>

Pour l'unique état global, les équations des signaux locaux sont :

$$a = e \land c \lor b$$

$$b = e \land \neg c$$

$$c = a \land d$$

qu'une simplification booléenne élémentaire réduit à :

$$a = e$$

$$c = e \land d$$

$$b = e \land \neg d$$

où les dépendances ont disparu. Le programme ARGOS est donc correct.

Or, quelle que soit la valuation des entrées *e* et *d*, la transition globale déduite du statut des signaux locaux défini par $a = e, c = e \land d, b = e \land \neg d$ n'est pas explicable par un enchaînement de transitions élémentaires.

D'autre part la simplification effectuée n'est pas autorisée en logique constructive, puisqu'elle nécessite l'utilisation de l'axiome $a \lor \neg a = \text{TRUE}$.

S'agit-il donc de la même notion ? Cette question est ouverte. Il semble assez évident que, s'il existe pour toute configuration des entrées un enchaînement de transitions élémentaires qui détermine le statut des signaux locaux, alors le système d'équations booléennes a une solution en logique constructive, qui n'est pas réduite au n-uplet indéfini.

Mais peut-être existe-t-il des situations complexes dans lequel le système d'équations a une solution constructive, bien que l'on échoue toujours à l'expliquer par un enchaînement de transitions élémentaires.

### 9.6.3 Pourquoi *a/b* n'est pas toujours une commande gardée

Quelle que soit la réponse à la question ci-dessus, on peut aussi s'interroger sur une notion de causalité ARGOS qui impose que les réactions globales soient toujours explicables comme enchaînement de transitions élémentaires, ce qui correspond à une interprétation très impérative de la notation *a/b*.

Ce paragraphe illustre simplement une classe d'exemples pour lesquelles la notation *a/b* n'est pas interprétée comme une commande gardée. Dans ce cas l'exigence d'enchaînement de transitions peut conduire à rejeter des programmes qu'on aimerait conserver. De même la traduction
en ESTEREL present a then emit b, qui fait dépendre l'émission de b de la présence de a,
conduira à des erreurs de causalité non interprétables en ARGOS.

L'interprétation de *a/b* comme une commande gardée signifie que cette notation se lit : *lorsque je suis sûr(*e**) de la présence de *a*, j'émet *b*. C'est un point de vue très impératif.

Une autre interprétation possible est : *la présence de a est une condition suffisante à l'émission de b*. Peut-être faudrait-il d'ailleurs adopter une notation du genre *b ← a*, pour mieux refléter l'aspect déclaratif de cette affirmation. Rien ne dit que la présence de *a* soit nécessaire à la présence de *b*.

**Exemple 9.4 : Conception dirigée par les entrées ou par les sorties**

Considérons un système qui, dans un état *A*, doit émettre *e* lorsque *a* et *b* sont présents simul-
tanément, et {*e*, *f*} lorsque *a* est présent et *b* absent. Avec la notation suggérée ci-dessus :

$$
\begin{align*}
e &\leftarrow a \wedge b \\
e, f &\leftarrow a \wedge \neg b
\end{align*}
$$

On détermine les ensembles de signaux à émettre et, pour chaque ensemble, on indique une
condition suffisante. Un tel ensemble de définitions peut être augmenté de nouvelles conditions
suffisantes à l'émission de l'ensemble {*e*, *f*} par exemple.

Une vision impérative de cette situation donnera toujours une structure de tests sur la pré-
sence de *a* et *b*, provoquant l'émission de *e*, *f* ou {*e*, *f*}. Une longue habitude de factorisation
des tests, héritée de la programmation séquentielle, conduira à minimiser la duplication de code
en écrivant un arbre de décision. En ESTEREL on obtient quelque chose du genre :

present a then
    emit e ;
    present b else emit f end
end

où il apparaît très clairement que l'émission de *e* ne dépend pas du statut de *b*.

Pour décrire une telle situation avec un automate (où l'on ne dispose pas a priori des transi-
tions branchues proposées plus haut), on dessinera plutôt deux transitions issues du même état
A, d'étiquettes a ∧ b/e et a ∧ ¬b/e, f. L'information selon laquelle l'émission de e ne dépend pas
du statut de b est en quelque sorte syntaxiquement distribuée, mais elle est toujours là. Cette
petite différence de syntaxe doit-elle conduire à une différence majeure de sémantique? □

Dans l'exemple précédent, on pourrait imaginer des méthodes de codage, ou des extensions
de la syntaxe des automates (comme les transitions branchues) qui éviteraient d'écrire de fausses
dépendances entre signaux. Cela peut être fait localement, si les transitions a ∧ b/e et a ∧ ¬b/e, f
appartiennent au même automate. Toutefois, si le même genre de situation se présente dans une
composition parallèle, ce n'est plus possible. On retombe sur l'exemple de la figure 9.8 ci-dessus.
Troisième partie

Extensions temporelle et hybride
<figure><img src="image_49.png" /></figure>
# Chapitre 10

## Argos temporisé

Sources: L'extension temporisée d'ARGOS est présentée dans [JMO93]. La méthode est exposée sur un exemple dans [JM95]. D'autre part le compilateur ARGOS étendu aux automates temporisés, couplé à l'outil KRONOS, a servi de support à l'activité de Muriel Jourdan en stage post-doctoral. Il s'agissait d'appliquer la méthode proposée dans un environnement de programmation de robots mobiles. Ce travail est rapporté dans [Jou96, SKEJ95].

### 10.1 Motivations

Les motivations de ce travail sont de deux ordres, selon que l'on adopte le point de vue des concepteurs de langages synchrones ou celui des utilisateurs d'automates temporisés.

#### 10.1.1 Prise en compte du temps dans les langages synchrones

La notion de temps dont on dispose dans les langages synchrones est un temps discret et multiforme. Le temps est assimilé aux instants de présence d'un signal extérieur. Rien n'empêche, donc, de considérer différentes échelles de temps non corrélées. L'exemple standard proposé par Gérard Berry fait intervenir des échelles de temps "mètres" et "secondes" pour expliquer qu'il est plus naturel d'exiger d'une automobile qu'elle s'arrête dans un délai de 5 mètres, que dans un délai de 10 secondes.

Lorsqu'on compile un programme qui fait intervenir des délais, ou compteurs de temps, pour obtenir un automate interprété (voir définition dans le paragraphe d'introduction sur les modèles, 1.2), il y a essentiellement deux solutions.

La première solution consiste à expanser les valeurs possibles des compteurs en états. On risque l'explosion du nombre d'états du programme global, au moins par composition parallèle des compteurs. D'autre part, on peut avoir à considérer en parallèle des composants qui comp- tent le même temps avec des ordres de grandeur différents. En effet, si un composant compte des secondes, et l'autre des heures, il faut se ramener à la même unité si l'on veut pouvoir compa- rer les compteurs. Le compteur d'heures atteint alors, en nombre de secondes, de très grandes valeurs. Toutefois cette solution permet de prendre en compte les valeurs des compteurs dans la vérification formelle des programmes, puisque l'information correspondante existe bien dans la partie contrôle de l'automate interprété. L'expression des propriétés est quelquefois compliquée par le fait que les valeurs des compteurs sont en quelque sorte codées en base 1 : exprimer $x > y$
lorsque les valeurs des compteurs *x* et *y* sont explicitement représentées par des états n'est pas de tout repos. C'est en ce sens que nous écrivions, dans l'introduction de [JMO93], qu'il est impossible d'exprimer des propriétés *quantitatives*.

La deuxième solution consiste à coder les compteurs par des *variables* de l'automate interprété. On supprime le problème d'explosion d'états, d'une part parce que la mise en parallèle n'a pas d'effet néfaste sur les conditions et affectations qui portent sur les variables ; d'autre part parce que les compteurs d'ordres de grandeur différents se traduisent par des valeurs d'ordres de grandeur différents à l'exécution, aisément comparables. L'inconvénient majeur de cette approche est l'impossibilité de prendre en compte les aspects de délai dans l'expression de propriétés effectivement vérifiables.

La troisième solution (!) est décrite dans [Hal93]. Pour joindre les avantages de la deuxième solution ci-dessus à la possibilité d'exprimer des propriétés temporelles — avantage dont ne jouissait jusque là que la première des deux solutions — il “suffit” d'appliquer aux automates interprétés issus par exemple du compilateur *ESTEREL* des techniques d'évaluation approchée, après avoir réalisé une analyse du format *OC* pour repérer parmi les variables au nom évocateur comme _v_0.1, celles qui proviennent de l'expansion des structures de contrôle temporelles. Nous retrouvons cette approche au chapitre 11, qui décrit le prototype *HARGOS* basé sur la connexion d'un compilateur *ARGOS* qui accepte des “pragmas” à l'outil *POLKA* de N. Halbwachs. Le seul inconvénient de la méthode réside dans la nature approchée des résultats obtenus, mais l'expérience a prouvé depuis que, dans la plupart des cas traités, l'analyse produit des résultats suffisants. Par ailleurs la même méthode (et le même outil d'analyse) peut être utilisée pour découvrir la valeur d'un délai permettant d'assurer une propriété donnée, en considérant certaines des valeurs de délai, non plus comme des constantes, mais comme des variables.

Le travail présenté dans [JMO93] explore une voie légèrement différente. En acceptant de perdre la richesse d'expression du temps multiforme, propre aux langages synchrones, on étend *ARGOS* avec une construction de délai, et on compile les programmes en automates temporisés (*Timed graphs* [AD90]), modèle sur lequel des propriétés quantitatives exprimées en logique temporelle temps-réel sont vérifiables. Pratiquement, on connecte le compilateur *ARGOS* à l'outil *KRONOS* développé à Vérimag, via son format d'entrée.

### 10.1.2 *ARGOS* temporisé comme langage de description des automates temporisés

Du point de vue des utilisateurs d'automates temporisés, la définition d'*ARGOS* temporisé fournit un *langage*. En effet les automates temporisés, comme tout modèle à base de systèmes de transitions, ne peuvent être utilisés directement pour la description de systèmes un tant soit peu complexes. Toutefois *ARGOS* temporisé n'a pas la puissance d'expression maximale. La construction de délai ne produit que des automates très particuliers. La question se pose alors de déterminer la classe des automates temporisés accessibles. Il est assez facile de caractériser cette classe de manière syntaxique, mais pour que cela offre de l'intérêt il faudrait savoir comparer la caractérisation syntaxique et les équivalences comportementales d'automates temporisés.

Muriel Jourdan a prouvé dans sa thèse [Jou94] que les automates temporisés obtenus par compilation d'ARGOS temporisé ont une bonne propriété: ils sont “non zénon” (les évolutions temporelles d'un automate temporisé qui n'a pas cette propriété supposent que le temps est borné: il croît indéfiniment, mais tend vers une borne supérieure. On se débrouille en général pour éliminer ces automates-là, pour lesquels la validité de certaines propriétés pose des problèmes d'interprétation). Ne pas avoir la puissance d'expression maximale paraît, dans ce cas, plutôt un
avantage qu’un inconvénient.

Toutefois Sergio Yovine a proposé des exemples qui montrent que l'on aimerait utiliser certains automates temporisés inaccessibles par compilation d'ARGOS temporisé. Il s'agit en général d'automates temporisés qui présentent un cas de non-déterminisme temporel.

La généralisation du travail de définition de sémantique de [JMO93], à des compositions d'automates qui portent des pragmas quelconques (voir chapitre 11), devrait fournir une solution à ce problème, au prix d'une utilisation plus difficile du langage. Toutefois, si pour des automates temporisés obtenus par compilation de la construction de délai proposée ici, l'interprétation de la synchronisation par diffusion synchrone ne posait pas de problème, cela demande à être étudié de plus près dans le cas des automates temporisés généraux, en suivant par exemple les idées de [SY96].

## 10.2 ARGOS temporisé et sa traduction en automates temporisés

### 10.2.1 Une construction temporelle

La construction temporelle que nous introduisons dans ARGOS provient d'un des tous premiers rapports sur les Statecharts, datant de 1984, qui proposait une série d'extensions à un formalisme encore tout jeune. On y trouvait donc, en particulier, la suggestion de temporiser les états. Cela consiste à associer à un état *A* un couple de valeurs réelles *a* et *b*, avec en général *a* ≤ *b*. La sémantique de cette construction exprime que, une fois entré dans l'état *A*, le système ne peut en sortir avant qu'un délai *a* ne se soit écoulé, et doit en être sorti lorsque le délai *b* expire. Pour que le système ne se bloque pas, on prévoit une transition dite de "time out", qui force à quitter l'état *A* lorsque le délai *b* expire, si on ne l'avait pas quitté auparavant en suivant le fonctionnement normal.

Puisque les états sont en fait des macro-états, l'utilisation de cette construction sur des états raffinés permet l'expression de chiens de garde.

Les constructions temporelles proposées pour les Statecharts dans des articles plus récents sont, à mon avis, moins propres que celle-là, dont on peut déplorer la disparition.

En ARGOS, on introduit la même construction, en ne gardant que la borne supérieure. La construction à deux bornes peut être fabriquée à partir de la construction à une seule borne. On peut considérer cette nouvelle construction comme une macro-notation, et décrire formellement son expansion en ARGOS usuel. Chaque temporisation d'état a pour effet d'ajouter un composant compteur, en parallèle. On synchronise le composant temporisé avec le compteur. On y gagne en lisibilité des programmes, mais c'est une façon d'appliquer la première solution mentionnée en introduction : la taille des modèles explose.

La bonne idée consiste donc à considérer cette nouvelle construction comme faisant partie du langage, et à redéfinir la sémantique d'ARGOS en automates temporisés.

### 10.2.2 ARGOS temporisé

Les programmes ARGOS temporisés adoptent la même syntaxe que les programmes ARGOS simples. Les machines qui constituent les composants de base sont équipées de temporisations d'états :

(S, s₀, I, O, T, T), où $T \in S \times \mathcal{N}(A) \times 2^A \times S$ est l'ensemble des transitions. La condition d'une transition est un élément de $\mathcal{N}(A) = \mathcal{B}(A) \cup \{to\}$, où to désigne une condition d'expiration de
<figure><img src="image_50.png" /><figcaption>FIG. 10.1 – Détection des doubles clicks en ARGOS temporisé</figcaption></figure>

délai (timeout). $\mathcal{T} : S \to \mathbb{N}^* \cup \{+\infty\}$ est la fonction de temporisation des états. $\mathcal{T}(s) = +\infty$ lorsque l'état n'est pas temporisé. $P_t$ désigne l'ensemble des programmes ARGOS temporisés.

La figure 10.1 donne un exemple d'utilisation des états temporisés dans un programme qui détecte les doubles clicks d'une souris. Le système reçoit en entrée un signal Click et le signal temporel. Il émet les signaux Simple ou Double, selon que le click est double — c'est-à-dire suivi d'un autre click dans un intervalle de temps inférieur à 3 unités de temps — ou simple. Ce petit programme peut servir d'interface dans un programme plus complexe qui associe des comportements différents aux clicks simple et double.

Nous avons vu au chapitre 6 comment ré-écrire un tel programme en ARGOS non temporisé, en considérant les états temporisés comme une macro-notation. Nous montrons ci-dessous comment traduire cette construction directement en automate temporisé.

### 10.2.3 Aperçu des automates temporisés

Un automate temporisé décrit l'évolution d'un système dans le temps grâce à un ensemble de variables réelles appelées *horloges*, qu'on peut tester et remettre à zéro. Leur valeur évolue de manière continue.

Nous utilisons les automates temporisés munis d'invariants sur les états, comme ceux définis dans [HNSY92]. Ajouter ces invariants est un moyen d'exprimer l'urgence des transitions, ce que ne permettait pas la définition initiale donnée dans [AD90] (un autre moyen d'exprimer l'urgence est décrit dans [SY96]).

La figure 10.2 est adaptée d'un exemple de [ACH$^{+}$92].

La transition $t$ de $s0$ à $s1$ initialise l'horloge $x$. La transition de $s1$ à $s2$ initialise l'horloge $y$, et peut être tirée après un temps quelconque passé dans l'état $s1$, pendant lequel $x$ croît. La transition de $s2$ à $s3$ ne sera possible que si le temps écoulé depuis que $t$ a été tirée appartient à l'intervalle $]1, 6[$. Toutefois la transition de $s1$ à $s2$, nécessairement tirée entre temps, a initialisé l'horloge $y$, et on ne peut être dans l'état $s3$ qu'à condition que $y \le 5$. Les invariants d'états réduisent ainsi les comportements possibles. L'étiquette de la transition de $s3$ à $s4$ indique qu'elle est tirable n'importe quand dès que $y \ge 4$. L'invariant $y \le 5$ de son état de départ la rend obligatoire quand $y$ atteint 5.

La forme des conditions — des comparaisons à des constantes entières — et des actions d'affectation — uniquement des remises à zéro — garantit la décidabilité de la logique TCTL sur le modèle des automates temporisés. En particulier l'accessibilité d'un certain état du graphe, avec une certaine valuation des horloges, est décidable. TCTL est une version temporisée de CTL, dans laquelle on associe des bornes temporelles aux modalités comme INEV. On peut ainsi
<figure><img src="image_51.png" /><figcaption>FIG. 10.2 – Exemple d'automate temporisé</figcaption></figure>

exprimer qu'une certaine propriété sera vraie inévitablement à partir d'un état, et cela dans un délai de 5 unités de temps. L'outil KRONOS développé à Vérimag est basé sur les résultats décrits dans [HNSY92].

### 10.2.4 Traduction

Nous donnons la sémantique d'ARGOS temporisé en termes d'automates temporisés avec actions, ce qui permet de conserver les étiquettes ARGOS comme étiquettes des automates temporisés. Les automates temporisés avec actions et invariants d'états sont de la forme : ($S, s_0, I, O, T, \mathcal{F}, X$) où $X$ est l'ensemble des horloges, $T \subseteq S \times C(X) \times B(I) \cup \{\text{EMPTY}\} \times 2^O \times \mathcal{RA}(X) \times S$ est l'ensemble des transitions et $\mathcal{F}: S \to C(X)$ décrit les invariants associés aux états.

$C(X)$ est l'ensemble des expressions booléennes construites à partir des variables de $X$ selon la grammaire : $c ::= x < k \mid x = k$ où $k$ est une constante entière positive ou nulle et $x \in X$ (la définition usuelle des automates temporisés autorise des conditions plus générales). $\mathcal{RA}(X) = 2^X$ est l'ensemble des actions de remise à zéro. Une remise à zéro détermine quelles variables doivent être remises à zéro lorsque la transition est exécutée. La partie action de l'étiquette en provenance d'ARGOS a la forme usuelle : c'est un élément de $B(I) \times 2^O$. On ajoute l'action EMPTY pour reconnaître les transitions construites pour exprimer l'expiration des délais, qui sont en quelque sorte spontanées : elles peuvent être exécutées sans influence extérieure. Les transitions qui portent cette action sont dites temporelles. Noter qu'une transition temporelle peut émettre des sorties. Une transition $t = (s_i, C, m, o, r, s_f)$ sera notée $s_i \xrightarrow{C, m/o, r} s_f$.

Le principe de la traduction est simple. On associe une horloge Var ($A$) à chaque état $A$ du programme ARGOS (lorsque l'état n'est pas temporisé, on verra apparaître des conditions de la forme $x < +\infty$ ou $x = +\infty$ que l'on remplace par true et false). Pour chaque état de chaque automate, on obtient un état d'automate temporisé avec actions, comme illustré figure 10.3.

On étend ensuite la sémantique des opérations d'ARGOS à des objets de cette forme. Nous ne donnons ici que la composition parallèle.

Soit $S'(P_i) = (S_i, s_{0i}, T_i, \mathcal{F}_i, X_i)$ la traduction du programme $P_i$, $i \in \{1, 2\}$.

La traduction $S'(P_1 \| P_2)$ est alors de la forme :

$$ (S_1 \| S_2, s_{01} \| s_{02}, T', \lambda s_1 \| s_2 \bullet \mathcal{F}_1(s_1) \wedge \mathcal{F}_2(s_2), X_1 \cup X_2) $$
<figure><img src="image_52.png" /><figcaption>FIG. 10.3 – *Principe de la traduction*</figcaption></figure>

L'ensemble des états et l'état initial sont définis comme auparavant :

$$S_1 \| S_2 = \{s_1 \| s_2, s_1 \in Q_1, s_2 \in Q_2\} \qquad s_{01} \| s_{02}$$

on fait l'union des ensembles d'horloges et l'invariant d'un état $s_1 \| s_2$ est la conjonction des invariants de $s_1$ et de $s_2$. Finalement $T'$ est défini d'après $T_1, T_2$ par :

$$ \frac{s_1 \mathrel{\substack{\overline{\underline{\hspace{2.5cm}}} \\ \hspace{2.5cm}} \hspace{-0.5cm} C_1 \cdot m_1/o_1 \cdot A_1 \Rightarrow} s'_1, \quad s_2 \mathrel{\substack{\overline{\underline{\hspace{2.5cm}}} \\ \hspace{2.5cm}} \hspace{-0.5cm} C_2 \cdot m_2/o_2 \cdot A_2 \Rightarrow} s'_2, \\ (m_1 = m_2 = \text{EMPTY}) \lor (m_1 \neq \text{EMPTY} \land m_2 \neq \text{EMPTY} \land (m_1 \land m_2 \neq \text{false}))} \qquad \text{[Pt]} $$

$X_1$ and $X_2$ sont disjoints. $C_1 \land C_2$ ne peut être réduit à **false**, puisque les deux fonctions portent sur des ensembles de variables disjoints. Les transitions temporelles (resp. non temporelles) peuvent être exécutées simultanément. Les deux types de transitions ne peuvent être fusionnés.

### 10.2.5 Propriété de cohérence des sémantiques

Pour juger de la nouvelle sémantique introduite pour ARGOS temporisé, il faut trouver un moyen de la comparer à la sémantique d'ARGOS simple.

On montre que : $S(\mathcal{E}xp(P_t)) \equiv \mathcal{D}(S'(P_t))$ où:

- $\mathcal{E}xp$ représente l'expansion de la macro-notation de temporisation des états (cf. chapitre 6). $\mathcal{E}xp(P_t)$ est un programme ARGOS simple, qui utilise un signal "temporel" noté $\chi$;

- Pour comparer $S(\mathcal{E}xp(P_t))$ — un système de transitions avec des signaux $\chi$, à $S'(P_t)$ — un automate temporisé, où le temps est implicite — nous utilisons une sémantique en temps discret $\mathcal{D}$ des automates temporisés obtenus par traduction des programmes ARGOS. $\mathcal{D}(atg)$ est un système de transitions étiquetées où apparaît également $\chi$.

- $\equiv$ est la bisimulation.

## 10.3 Implantation et exemples d'utilisation

### 10.3.1 Implantation

L'implantation est réalisée par modification du compilateur ARGOS existant. On produit des automates temporisés au format d'entrée de KRONOS, où le mécanisme d'étiquetage des transitions permet de conserver l'information en provenance des étiquettes de transitions ARGOS. Il est
<figure><img src="image_53.png" /><figcaption>FIG. 10.4 – Un schéma de synchronisation de tâches-modules</figcaption></figure>

<figure><img src="image_54.png" /><figcaption>FIG. 10.5 – Comportement temporel d'un schéma de synchronisation de tâches-modules</figcaption></figure>

ainsi assez simple de remonter au source, lorsque KRONOS fournit des résultats en termes d'états de l'automate temporisé.

### 10.3.2 Vérification d'un schéma de synchronisation de tâches-robot

L'exemple est fourni par l'environnement ORCCAD (Open Robot Controller Computer Aided Design), qui propose une approche intégrée, depuis une spécification de haut niveau jusqu'à l'implémentation. La notion de tâche-robot est centrale dans ORCCAD. Une tâche-robot est un ensemble de tâches temps-réel communicantes appelées tâches-modules. Pour spécifier complètement une tâche-robot, on associe à chacune de ses tâches-modules une durée de calcul (supposée connue) et une période d'activation, et on décide des protocoles de synchronisation utilisés entre les tâches (on considère en général des connexions binaires entre un producteur et un consommateur, et la lecture et/ou l'écriture peuvent être blocantes ou non).

La figure 10.4 donne une tâche-robot constituée de trois tâches-modules A, B et C. Le temps de calcul de A est de 5ms, et cette tâche est activée toutes les 10ms. Elle est synchronisée avec la tâche B par un protocole dit "asynchrone/synchrone" (dans la terminologie ORCCAD), c'est-à-dire que A évolue librement, alors que B est bloqué en attente d'une donnée produite par A. Le même type de synchronisation est utilisé entre B et C. La figure 10.5 donne le comportement temporel de la tâche-robot.

La figure 10.6 donne le programme ARGOS utilisé pour modéliser ce schéma de synchronisation.

La modélisation des tâches-robots en ARGOS temporisé, et l'utilisation de KRONOS, sont proposées comme une méthode de validation des schémas de synchronisation. En particulier, nous
<figure><img src="image_55.png" /><figcaption>FIG. 10.6 – Modèle ARGOS du schéma de synchronisation</figcaption></figure>

pouvons montrer automatiquement qu'un tel schéma est exempt de blocage temporel, autrement dit que les tâches-modules ont toujours fini leur exécution lorsque leur réactivation survient. Nous pouvons également exhiber les situations de blocage temporel, lorsqu'elles existent. Dans l'exemple proposé ci-dessus, un blocage apparaît, 16 ms après l'initialisation globale : la tâche *B* doit être réactivée, mais elle n'a pas même commencé son calcul, étant en attente d'activation par *A*.

## 10.4 Généralisation

Comme je l'exposais en introduction, nous avons, pour cette première extension d'ARGOS, redéfini la sémantique des constructions, qui expriment maintenant des compositions de "machines de Mealy temporisées". Cette nouvelle sémantique et sa propriété de compositionnalité s'inspirent bien sûr des travaux antérieurs, mais il apparaît finalement peu satisfaisant d'avoir à ré-écrire ainsi l'essentiel de la sémantique des opérations, tout en s'attachant à résoudre les nouveaux problèmes que pose l'extension temporelle.

Il est facile de se convaincre, en lisant la sémantique d'ARGOS temporisé, que les gardes temporelles et les affectations aux variables temporelles sont traitées indépendamment des gardes booléennes utilisées pour l'expression de la synchronisation usuelle.

Cette remarque suggère d'écrire la sémantique d'un ARGOS dans lequel on pourrait attacher
des informations quelconques aux états et transitions. Cette technique est utilisée pour décrire
en ARGOS des systèmes dits *hybrides* et fait l'objet du chapitre 11.

Le cas temporisé n'est plus ainsi qu'un cas particulier du cas hybride. Nous abandonnons
l'idée de prévoir dans le compilateur ARGOS un algorithme de compilation directe en automates
temporisés. Ceux-ci peuvent être obtenus, depuis un programme qui utilise la macro-notation
de temporisation ou des pragmas, grâce au prototype HARGOS décrit au chapitre suivant. La
connexion à POLKA, qui peut réaliser des analyses approchées, est souvent nécessaire pour traiter
des problèmes hors de portée de l'analyse exacte réalisée par KRONOS.
# Chapitre 11

## Argos hybride, un point d'entrée de l'outil Polka

Sources: L'article [HMP95] expose un exemple d'utilisation de l'outil HARGOS obtenu en connectant une extension du compilateur ARGOS à l'outil POLKA de N. Halbwachs []. Nous reprenons cet exemple ici, en ajoutant une description du langage ARGOS hybride utilisé en entrée — non publiée pour l'instant — et quelques réflexions sur l'implémentation de la connexion.

### 11.1 Motivations

Les motivations de ce travail sont doubles. Il s'agit, d'une part de généraliser le travail réalisé pour ARGOS temporisé; d'autre part de permettre l'utilisation d'un langage structuré pour la description des systèmes hybrides sous forme de systèmes de transitions équipés de contraintes linéaires.

Le travail de réécriture de la sémantique d'ARGOS, pour tenir compte des contraintes temporelles associées aux états, fait apparaître une idée simple: ARGOS peut être considéré comme un jeu d'opérateurs pour combiner des automates, quelle que soit la nature des informations attachées aux états et transitions. En d'autres termes, il est possible de séparer complètement les aspects de calcul de la synchronisation par diffusion synchrone, des autres informations qu'on peut vouloir attacher aux états et transitions. Ces informations additionnelles sont introduites sous formes de pragmas (cf. chapitre 6), dont la sémantique est ignorée par le compilateur ARGOS.

En ce qui concerne les systèmes hybrides, la technique des pragmas d'ARGOS permet une description structurée plus facile à concevoir et manipuler qu'un automate plat. L'apport le plus intéressant concerne la vérification des programmes. En effet, la nature synchrone d'ARGOS permet, par l'utilisation d'observateurs, de ramener toute propriété de sûreté à l'accessibilité d'un état d'erreur défini à cet effet. Or l'outil POLKA est particulièrement approprié aux calculs d'accessibilité.

Notons également, en quelques mots, qu'un langage synchrone donne des descriptions réalistes du comportement de systèmes réactifs comme le contrôleur de passage à niveau décrit plus loin. En effet, on y distingue nettement les entrées et les sorties d'un système réactif, et les entrées doivent être acceptées telles que, le système ne maîtrisant que les sorties. Il existe en revanche de nombreuses descriptions du même genre de problèmes dans des langages ou formalismes à base de rendez-vous [], pour lesquelles les propriétés recherchées — par exemple: la barrière est
baissée lorsque le train passe — est assurée trivalement par un rendez-vous entre la barrière et le train : en quelque sorte, la barrière “arrête” le train si elle est ouverte !

## 11.2 Les systèmes hybrides et le modèle considéré

Dans les systèmes dits *hybrides*, des composants discrets contrôlent une activité continue. Dans le cas général l'activité continue devrait être décrite par des systèmes d'équations différen-tielles, qui constituent un modèle hors de portée des capacités d'analyse de propriétés par des méthodes informatiques. De nombreux travaux portent donc sur la définition de modèles moins expressifs que ce modèle général, mais pour lesquels on peut trouver des langages de propriétés analysables automatiquement.

Pour l'extension ARGOS hybride nous utilisons un modèle qui associe aux états et transi-tions d'un automate des systèmes de contraintes linéaires portant sur des variables numériques continues et sur leurs dérivées.

Plus précisément : les états portent des systèmes d'inéquations linéaires dans lesquels inter viennent les dérivées des variables. Les dérivées sont supposées constantes dans chaque état, même si elles sont manipulées comme des constantes symboliques. Les conditions des transitions sont des systèmes d'inéquations linéaires sur les variables elles-mêmes, et les actions associées aux transitions sont des affectations des variables, pour lesquelles on ne s'autorise que des expressions linéaires. Ce modèle est analysable par des méthodes approchées développées par N. Halbwachs et implémentées dans l'outil POLKA. Ces méthodes consistent à calculer, pour chaque point de contrôle du programme, une approximation supérieure de l'ensemble des valuations de variables accessibles depuis une valuation initiale. Cette approximation est décrite par un polyèdre convexe.

## 11.3 Connexion ARGOS+POLKA : le prototype HARGOS

La connexion ARGOS/POLKA a été réalisée grâce à une légère modification du compilateur existant, qui permet de prendre en compte des pragmas. La nouvelle version de l'environne-ment ARGONAUTE, en cours de développement, intègre les extensions nécessaires à un traitement général des pragmas. La connexion à l'outil POLKA n'est plus qu'un cas particulier.

On utilise des pragmas d'états et de transitions, et un pragma global qui permet de définir les variables utilisées. Le compilateur ARGOS ignore ces pragmas et les transmet inchangés à POLKA, qui les analyse et peut alors y découvrir des erreurs de syntaxe. Pour éviter de reporter aussi tard la détection d'erreurs de syntaxe dans les pragmas, on peut imaginer que le compilateur ARGOS fasse appel à un programme séparé fourni par l'environnement aval. Ici, le concepteur de POLKA peut fournir un filtre qui renvoie, pour un pragma, un compte-rendu d'analyse. Le compilateur ARGOS, qui dispose de toutes les informations relatives au fichier source (numéro de ligne, ...) peut reporter ce compte-rendu assorti d'informations de position, et ne pas s'engager dans la phase de génération de code.

## 11.4 Exemple d'utilisation de HARGOS : le passage à niveau

On considère un passage à niveau sur une voie simple ou double, muni d'une barrière et activé lorsque le train écrase une pédale placée sur la voie. La région étudiée a pour longueur $D' = 1500m$, et la barrière est située à $D = 1000m$ de la pédale d'entrée (cf. figure 11.1). La vitesse maximale du train est de $S = 60m/s$. La barrière se ferme ou s'ouvre avec une vitesse
angulaire de 10°/s. Initialement, il n'y a pas de train dans la région étudiée, et la barrière est
ouverte. A tout instant, ensuite, il y au plus un train sur chaque voie, dans chaque région.

<figure><img src="image_56.png" /><figcaption>FIG. 11.1 – Le problème du passage à niveau</figcaption></figure>

ARGOS hybride constitue une utilisation particulière de la technique des pragmas présentée ci-
dessus. On associe aux états des invariants sous forme de systèmes d'inéquations linéaires portant
sur les variables ou leurs dérivées, et aux transitions des conditions de franchissement données
sous la même forme, et des affectations parallèles. Un pragma global permet de "déclarer" toutes
les variables continues utilisées dans les invariants ou les gardes de transitions.

11.4.1 Première description en ARGOS hybride

Le système pourrait être décrit par un automate temporisé, par exemple en ARGOS temporisé
(cf. chapitre 10). Il suffit pour cela de se ramener à une seule échelle de “temps” : le temps
minimum qui séapre l’entrée du train dans la région et l’instant où il atteint la barrière est donné
par 1000/60 = 16.67s. Il lui faut en suite un temps supérieur à (1500 – 1000)/60 = 8.34s pour
quitter la région. La fermeture (ou l’ouverture) complète de la barrière prend 90/10 = 9s.

Toutefois, nous donnons ici une description à temps multiforme, plus naturelle. La figure 11.2
donne le programme ARGOS hybride qui modélise le système complet : un train, la barrière (gate)
et le contrôleur de passage à niveau.

En ARGOS hybride on peut associer aux états et transitions des automates de base des sys-
tèmes d'inéquations linéaires portant sur des variables continues ou leurs dérivées.

Le train est un système à trois états qui gère une variable continue $x$ pour mesurer la distance du train au point d'entrée. On déclare, globalement, que $x \le 60$. Le train est initialement hors de la région ; la variable $x$ est mise à zéro lorsque le train entre dans la région — signal *enter* émis vers le contrôleur ; tant que $x \le 1000$, le train s'approche de la barrière, et l'atteint dès que $x = 1000$. Il est encore dans la région tant que $x \le 1500$, puis la quitte dès que $x = 1500$, en émettant un signal *exit* vers le contrôleur.

La barrière gère une variable continue $\alpha$ pour mesurer son angle avec la position horizontale. La barrière est initialement ouverte ($\alpha = 90^\circ$). Dès qu'elle reçoit une commande *lower* elle commence à descendre avec une vitesse angulaire de 10 degrés par seconde ($\dot{\alpha} = -10$), jusqu'à être complètement fermée ($\alpha = 0$). Elle reste fermée ($\dot{\alpha} = 0$) jusqu'à ce qu'elle reçoive une commande *raise*. Elle s'ouvre alors avec une vitesse angulaire de 10 degrés par seconde ($\dot{\alpha} = +10$).
Le contrôleur reçoit les signaux *enter* et *exit* et compte les trains qui occupent la région. La variable *k* est une variable *discrète*, c'est-à-dire que sa valeur n'est modifiée que par les affectations explicites attachées aux transitions. Sa dérivée est globalement déclarée nulle. La région est vide de train lorsque $k = 0$. Les signaux *lower* et *raise* qui commandent la barrière lui sont envoyés quand la région devient occupée ou se libère, respectivement.

Si l'on considère un système simple à un train, il suffit de mettre en parallèle le contrôleur, la barrière, et un exemplaire du système train ci-dessus, en déclarant locaux les signaux *enter*, *exit*, *lower* et *raise*.

### 11.4.2 Compilation et analyse par POLKA

Le compilateur ARGOS produit, à partir de ce programme, un système de transitions à 15 états et 56 transitions. Les transitions sont étiquetées par des systèmes d'inéquations linéaires sont certains sont non satisfaisables.

La connexion à l'outil d'analyse de contraintes POLKA permet de supprimer ces transitions, et l'on obtient le système réduit suivant :

<figure><img src="image_57.png" /><figcaption>FIG. 11.3 – Première description en ARGOS hybride, après réduction par POLKA</figcaption></figure>

Il semble donc que l'état *barrière levée/train présent* soit accessible. Cela révèle une erreur de conception : lorsque la barrière s'ouvre, elle ne tient pas compte des signaux *lower* qui peuvent lui parvenir, et continue donc à s'ouvrir même si un nouveau train survient. On corrige facilement la description de la barrière :
<figure><img src="image_58.png" /><figcaption>FIG. 11.2 – Programme ARGOS hybride du passage à niveau</figcaption></figure>
<figure><img src="image_59.png" /><figcaption>FIG. 11.4 – Correction de la barrière</figcaption></figure>

Le système obtenu ne peut plus être décrit par un automate temporisé. En effet, lorsque le mouvement d'ouverture de la barrière est interrompu par une commande *lower*, la barrière doit redescendre de l'angle qu'elle avait atteint. Le temps nécessaire à ce mouvement de fermeture partiel n'est pas connu statiquement.

Si l'on compile le programme obtenu en remplaçant la description erronée de la barrière par la description ci-dessus, on obtient un programme ARGOS à 10 état et 22 transitions, dont POLKA ne conserve que la structure suivante, sur laquelle nous avons également reporté les résultats de l'analyse :

<figure><img src="image_60.png" /><figcaption>FIG. 11.5 – Résultats de l'analyse pour un train</figcaption></figure>
# 11.5 Pour aller plus loin...

## Analyse symbolique

L'outil POLKA peut être utilisé pour “découvrir” la distance minimum *D* entre la pédale d'entrée et la barrière, permettant d'assurer que la barrière est fermée quand le train passe. Il suffit de remplacer la distance 1000 par une constante symbolique *D*, et la distance 1500 par l'expression *D*+500. *D* est considéré par POLKA comme une variable de dérivée 0. L'outil montre que les états erronés (ceux pour lesquels le train passe uen barrière ouverte) ne sont accessibles que lorsque *D* ≤ 540 (la barrière se ferme en 9 secondes, et, pendant cet intervalle de temps, le train parcourt au plus 60 × 9 = 540*m*.

Cette caractéristique de l'outil rend la connexion ARGOS+POLKA intéressante même lorsque les systèmes étudiés peuvent être décrits par des automates temporisés : l'outil KRONOS ne permet pas de manipuler les constantes de délai de manière symbolique.

## Plusieurs trains

Pour prendre en compte plusieurs trains, il faut savoir distinguer les signaux *enter* et *exit* en provenance de trains distincts, afin de savoir tenir compte des occurrences simultanées de tels signaux. La figure 11.6 donne le nouveau contrôleur de barrière en ARGOS hybride. On y constate immédiatement la complexité des étiquettes. Une extension d'ARGOS pour prendre en compte des signaux valués (comme en ESTEREL) dont les valeurs peuvent être combinées en cas d'émission multiple réduirait quelque peu la description, mais les conditions à exprimer sont intrinsèquement complexes.

<figure><img src="image_61.png" /><figcaption>FIG. 11.6 – Contrôleur de barrière pour deux trains</figcaption></figure>

Le compilateur ARGOS fabrique un automate à 37 états et 206 transitions, dont POLKA extrait une structure à 13 états. Les états problématiques ne sont pas accessibles.

## Traitement du non déterminisme

Les descriptions de systèmes hybrides mais aussi, plus généralement, des systèmes équipés de pragmas, sont souvent non déterministes lorsqu'on s'abstrait des pragmas pour ne garder que la structure de contrôle ARGOS. Nous sommes là typiquement dans l'un des cas invoqués comme motivations du travail sur le non déterminisme dans les langages synchrones, exposé au chapitre 4. Je n'y reviendrai pas ici.
Quatrième partie

Environnement de programmation
<figure><img src="image_62.png" /></figure>
# Chapitre 12

## Edition graphique et débogage symbolique d'argos

Sources: *Les réflexions présentées ici doivent beaucoup aux discussions avec Philippe Schaar, lors de son année de stage à Vérimag, et avec Vincent Quint, du projet INRIA Opéra, au sein duquel a été conçu et développé l'outil Grif. L'expérience menée au cours de l'année 1993 autour de l'implantation d'un éditeur ARGOS en Grif est mentionnée dans [QV94]. Le travail de P. Schaar est décrit dans [Sch94].*

### 12.1 Présentation du problème

Le problème de l'édition graphique d'ARGOS s'est posé très tôt. A la fin de ma thèse, il existait un environnement de programmation complet pour ARGOS, comprenant un éditeur graphique syntaxique et la première version du compilateur, et connecté à l'outil d'analyse ALDÉBARAN []. L'éditeur avait été entièrement spécifié en LPG (un langage de types abstraits algébriques[]) et programmé en XWindows-10, par un groupe de 4 étudiants du DESS de Génie Informatique de l'Université Joseph Fourier. Parallèlement à ce développement expérimental, des réflexions étaient menées sur les fonctionnalités nécessaires dans un éditeur syntaxique de langage graphique, renforcées plus tard par les commentaires de Muriel Jourdan confrontée à l'utilisation de l'éditeur pour décrire le premier "gros" programme ARGOS.

L'éditeur était conçu comme un simple programme d'application au-dessus d'une bibliothèque de manipulation d'arbres abstraits et de représentation graphique des objets du langage. Une utilisation non interactive de la même bibliothèque avait permis d'obtenir un débogueur symbolique<fnref n="1" /> d'ARGOS, en modifiant le compilateur de manière à ce qu'il associe, aux états et transitions de l'automate global d'un programme, les ensembles d'états et de transitions des automates de base dont ils proviennent. On pouvait donc exécuter l'automate global en observant, sur la forme graphique du programme, les états actifs et les transitions déclenchées.

Le résumé des reflexions et commentaires tirés de ces expériences tient en quelques points importants. Tout d'abord, pour réaliser un éditeur de langage graphique, il a deux solution extrêmes, entre lesquelles on peut imaginer toute une variété de solutions mixtes :

**Analyse syntaxique 2D** : on peut utiliser un éditeur graphique général, et réaliser une analyse

<footnote n="1">1. Au sens où gdb est un débogueur symbolique de C, par exemple ; "symbolique" faisant ici référence à la table des symboles du programme, conservée au cours de la compilation comme information de retour au source.</footnote>
de la figure pour y repérer les objets du langage (c'est exactement l'approche suivie pour les langages séquentiels, où l'on invente une syntaxe concrète à base de séparateurs et de mots-clés pour représenter linéairement, sans perte d'information, une structure typiquement arborescente. L'analyse syntaxique consiste alors à reconstruire l'arbre abstrait à partir du texte linéaire). Il est préférable d'utiliser un éditeur qui fournit des objets de base comme les rectangles et les lignes, plutôt qu'un éditeur de bitmap. Si tous les éléments de syntaxe concrète du langage correspondent à des objets graphiques connus de l'éditeur, une partie du travail de reconnaissance est épargné. Reste toutefois à repérer l'organisation de ces objets (typiquement, dans un éditeur d'automate, quel critère de proximité peut-on utiliser pour reconnaître l'association flèche-texte qui définit une transition ?). Cette approche, qui peut sembler sans espoir, a pourtant été utilisée dans d'autres contextes, en particulier avec l'éditeur Idraw de l'INRIA qui produit du postscript commenté par les types d'objets. D'autre part il existe des travaux théoriques sur la généralisation des algorithmes d'analyse syntaxique de texte à des sources 2D. Voir par exemple [CTC91, CTC90], dans lesquels on utilise une relation spatiale entre objets.

**Edition syntaxique:** on peut développer un éditeur syntaxique, basé sur un outil de dessin. On se trouve alors confronté à trois types de problèmes :

- des problèmes de dessin plus ou moins interactif: typiquement, dans un éditeur d'automates, il est bien agréable de disposer d'un placeur automatique de transitions, et on aimerait que le déplacement de la boîte qui représente un état s'accompagne d'un déplacement harmonieux des flèches représentant les transitions qui y sont attachées

- des problèmes classiques de manipulation d'arbre abstrait: doit-on imposer une construction ascendante ou descendante, quelles opérations de suppression de sous-arbre peut-on autoriser...? sont quelques unes des questions qui se posent au concepteur.

- des problèmes de choix du degré d'analyse garanti par l'éditeur: peut-on se contenter d'un éditeur qui ne gère que les aspects de syntaxe hors-contexte, ou doit-on également garantir une analyse des aspects de syntaxe contextuelle (ou sémantique statique)? Dans ce dernier cas, à quels blocs s'applique l'analyse, et quand? (La réponse "partout, tout le temps" conduit à définir un éditeur dans lequel tout objet à peine ébauché doit être correctement constitué avant de pouvoir être utilisé comme composant d'un objet plus complexe. C'est un comportement extrêmement contraignant, pour ne pas dire pénible).

Nous n'avons jusque là considéré que les aspects de création et modification de programmes. Un autre aspect important concerne les choix de présentation des programmes. En effet, comme exposé dans [Mar91] pour ARGOS, un langage graphique est intrinsèquement peu concis<fnref n="2" />. Il faut donc prévoir des techniques de présentation partielle des programmes — par exemple en ne montrant pas systématiquement le contenu des états raffinés — et imaginer des opérations de manipulation de la présentation — zoom sur un composant raffinant, etc.

<footnote n="2">2. Contrairement à l'idée reçue qui veut qu'un dessin vaille mieux qu'un long discours</footnote>
## 12.2 Première tentative: Andromède

La première réalisation d'un éditeur ARGOS est un éditeur syntaxique. Nous avons en quelque sorte reinventé les problèmes d'édition d'arbre abstrait — et leurs solutions les plus immédiates —, au cours du développement, par manque de culture dans ce domaine. Le prototype Andromède propose une édition ascendante — avec placeur automatique des transitions des automates et des composantes d'une mise en parallèle — couplée à des vérifications de sémantique statique incrémentales. Pour modifier l'étiquette d'une transition appartenant à un automate pris dans une construction complexe à plusieurs étages d'opérateurs, il faut “déconstruire” l'arbre afin d'isoler l'automate, le modifier, puis reconstruire l'arbre. Toute modification locale, comme l'insertion d'un opérateur unaire portant sur un sous-arbre, est réalisée par déconstruction et reconstruction. Cet aspect, à lui seul, rend le prototype inutilisable en pratique.

Et pourtant... ce problème d'édition graphique est mis de côté temporairement, et on définit une syntaxe textuelle très simple pour ARGOS, afin de pouvoir utiliser le compilateur et continuer à travailler sur la sémantique en disposant d'un outil.

## 12.3 Le prototype Aglae: éditeur ARGOS en Grif

La deuxième tentative conduit au prototype Aglaé, conçu et développé par Philippe Schaar dans le cadre de son mémoire de thèse CNAM en 1993 [Sch94]. Confronté au problème dans son entier, et à une démonstration de l'éditeur Andromède, encore exécutable à l'époque, P. Schaar a fait preuve d'une remarquable et salutaire curiosité. Après avoir trouvé, compris et testé un certain nombre de bibliothèques, “méthodes” ou environnements de conception d'interfaces homme/machine — le chapitre 4 de son mémoire de thèse est un bon résumé de ce tour d'horizon — il a finalement suggéré d'utiliser Grif [], développé au sein du projet INRIA Opéra (Outils Pour les documents Electroniques, Recherche et Applications). Plus exactement, il a suggéré une interview des chercheurs du projet Opéra, sur les aspects d'édition “intelligente” d'arbres abstraits. Cette rencontre s'est concrétisée par la décision d'implanter l'éditeur ARGOS en Grif, en utilisant l'interface programme-application (API) en cours de définition pour Grif.

### 12.3.1 Bref aperçu de Grif

Grif est un outil d'édition de documents structurés, qui propose de définir séparément la structure *logique* du document et ses différentes *présentations*. La structure logique est décrite par une grammaire hors-contexte équipée de liens hyper-texte. Une présentation est décrite en associant à chaque élément de la structure logique un ensemble de règles définissant son aspect graphique. Plusieurs présentations différentes peuvent être définies, pour la même structure logique. L'édition est contrôlée par la structure: toute action de l'utilisateur, sensible sur une des présentations du document, est traduite en termes de la structure logique, et peut-être répercutée sur les autres présentations. L'édition est générique, au sens où l'éditeur propose des actions de base de manipulation des arbres sous-jacents, comme la création, le déplacement ou la suppression de sous-arbres. L'éditeur propose aussi une opération de "copier/coller" intelligente, c'est-à-dire respectant les règles de définition de la structure logique.
### 12.3.2 Aglaé

Aglaé s'appuie sur Grif pour définir un éditeur ARGOS mi textuel, mi graphique. Les principes de base sont les suivants : la description des automates n'est pratique que si l'on dispose de l'édition graphique. Toutefois l'édition des informations textuelles associées (étiquettes de transitions, nom et commentaires associées aux états) est plus agréable dans un éditeur de texte. La structure générale des processus s'édite plus facilement sous une forme textuelle, qui montre les imbrications par des indentations de manière plus concise que la syntaxe graphique à deux dimensions. La présentation graphique des processus composés est entièrement calculée.

L'éditeur Aglaé fournit des outils de classement des automates et des processus définis dans le programme, de recherche par nom, de renommage global, etc.

Bien que l'implantation effective se soit heurtée aux performances encore insuffisantes de l'API de Grif en ce qui concerne les objets graphiques, le travail de définition d'Aglaé a permis d'établir le cachier des charges de ce que serait un véritable éditeur mixte graphique/textuel pour un langage comme ARGOS. Sans doute faudrait-il reprendre l'étude aujourd'hui, avec la version actualisée de Grif.

## 12.4 Travaux de même nature

### 12.4.1 Autograph

Valérie Roy (CMA - Ecole de Mines, Sophia Anitpolis) travaille depuis presque 10 ans sur l'outil AUTOGRAPH [RS89, RdS90, Roy90] de manipulation des représentations graphiques de systèmes de transitions ou de réseaux de processus. La version actuelle offre un algorithme de placement automatique. L'idée la plus intéressante d'AUTOGRAPH réside dans le mécanisme de placement guidé d'un système de transitions : l'outil propose les états par "tranches" successives depuis l'état initial. Ainsi on place d'abord les états immédiatement successeurs de l'état initial, puis on explore chacun d'entre eux et on place ses propres successeurs, etc...

Nous avons envisagé dès le début l'utilisation d'AUTOGRAPH pour l'édition de programmes ARGOS. Il nous a paru difficile d'adapter l'outil à la manipulation des structures de programmes.

### 12.4.2 Arged (GMD, Sankt Augustin, projet Synchronie)

Leszek Holenderski, qui travaille dans l'équipe d'Axel Poigné (GMD, Sankt Augustin) sur l'intégration des langages ESTEREL, LUSTRE et ARGOS dans un environnement unique, s'est lancé dans le développement d'un éditeur ARGOS en TCL/TK, nommé Arged.

Outre les problèmes de performance liés à une première version interprétée — qui seraient sans doute “aisément” résolus par une programmation mixte TK/C, en version compilée — le prototype présente les défauts d'Andromède : la manipulation des arbres abstraits est extrêmement contraignante, bien que Leszek ait défini tout un ensemble de manipulations “naturelles” comme l'insertion d'un opérateur d'encapsulation en position de noeud interne.

Dans la version la plus récente, on retrouve une partie des manipulations d'arbres abstraits qui avaient été proposées par Philippe Schaar pour Aglaé. On peut ainsi sélectionner un sous-arbre de l'arbre abstrait d'un processus, et lui appliquer des opérations comme l'ajout d'un opérateur unaire, ou l'ajout d'un composant parallèle. Toutefois il manque encore une opération de copier/coller respectant la structure typée de l'arbre abstrait, pour pouvoir réaliser des constructions descendantes ou ascendantes.
L. Holenderski a également prévu le retour au source, et le même outil peut être utilisé pour simuler le comportement d'un programme en montrant les états courants et les transitions tirées.

### 12.4.3 Editeur des SyncCharts (Université de Nice)

Charles André (Université de Nice) travaille sur une extension d'ESTEREL par des constructions hiérarchiques héritées des Statecharts (dans le style d'ARGOS) et par des constructions héritées du Grafcet. L'ensemble est traduit en ESTEREL. Il existe un éditeur pour ce nouveau langage à syntaxe graphique, également programmé en TCL/TK, mais beaucoup plus efficace qu'Arged cité ci-dessus.
# Chapitre 13

# Compilation et connexion aux outils

Sources: *Documentation du nouveau compilateur.* Les versions antérieures ont été décrites dans *Jou91, Jou94, MV92b*

## 13.1 Schéma général du compilateur, formats et étapes

La figure 13.1 donne le schéma de la structure interne du nouveau compilateur. On y trouve les différentes formes intermédiaires et les différents chemins qui conduisent du format source ARGOS à un programme exécutable ou à un modèle analysable. Certaines phases ne sont pas encore implantées ou pas encore intégrées dans ce nouveau cadre, mais ont été testées indépendamment dans des prototypes (c'est le cas par exemple de la traduction ARGOS vers DC).

### Analyse

Partant d'un programme ARGOS source (un texte à la syntaxe décrite au chapitre 6), la phase d'analyse syntaxique produit un arbre abstrait, puis un abre abstrait correct vis-à-vis des types et de l'utilisation des noms (déclarations, ...).

### Traitement du non-déterminisme

L'étape suivante consiste à obtenir un arbre abstrait décrivant un ensemble de processus déterministes. Deux cas sont traités :

- Si l'on n'accepte pas le non déterminisme intrinsèque en entrée, certains cas de non déterminisme peuvent être traités comme des abréviations (voir chapitre 6). Les autres provoquent des erreurs de compilation.

- Si l'on accepte le non déterminisme intrinsèque en entrée, on applique la phase d'introduction des oracles décrite au chapitre 4 pour obtenir un programme déterministe et pouvoir enchaîner les phases suivantes.

### Générations d'équations puis de programmes DC

A partir d'un abre abstrait correct décrivant un ensemble de processus déterministes, on génère des équations booléennes (structure du format DC). On peut suivre différents chemins
<figure><img src="image_63.png" /><figcaption>FIG. 13.1 – Phases et formats intermédiaires de la chaîne de compilation</figcaption></figure>
selon que l'on expanse le programme ARGOS préalablement ou non.

- En cas d'expansion préalable, la génération produit un système d'équations éventuellement bouclées (c'est-à-dire un noeud DC, aux équations bouclées)

- Si l'on n'expanse pas le programme ARGOS, la génération d'équations produit un noeud DC par processus ARGOS, aux équations potentiellement bouclées également.

Chaque système d'équations peut être débouclé indépendamment du contexte dans lequel le processus correspondant est utilisé. Ce débouclage peut produire une erreur de compilation s'il est impossible d'obtenir un ensemble d'équations débouclées. L'expansion au niveau des noeuds DC peut réintroduire des boucles, que l'on doit de nouveau éliminer.

Si l'on expanse le programme ARGOS préalablement, les boucles éventuelles d'un processus sont reproduites en autant d'exemplaires que d'appels de ce processus, et le travail de débouclage est donc dupliqué (d'autre part il est plus facile, et plus clair, de reporter l'impossibilité de déboucler sur un programme non expansé). Un débouclage local à chaque processus, avant expansion, minimise ce travail. On n'échappe pas, pourtant, à une deuxième phase de débouclage, une fois les équations expansées, mais elle ne porte plus que sur un petit ensemble de signaux locaux (et on sait qu'une erreur découverte à cette étape provient de la structure des appels de processus, et non de la structure d'un processus particulier).

La génération de programmes au format DC est une simple étape d'impression des systèmes d'équations manipulés jusque là. Puisqu'on accepte les boucles de définition en DC, il est possible de produire des programmes DC à n'importe quelle étape.

## Obtention d'automates explicites

L'obtention d'un automate explicite (format OC d'automates interprétés pour la connexion au générateur de code OCC, format TARGOS d'automates booléens à pragmas pour la connexion à POLKA, format AUT d'automates pour la connexion à ALDÉBARAN, etc.) peut être réalisée à partir d'un système d'équations non bouclées.

On peut aussi espérer des outils de génération d'automates explicites à partir de DC.

## Traitement des pragmas

Le mécanisme de composition des pragmas a été décrit au chapitre 6. Il permet de conserver, dans la structure des pragmas, le maximum d'information sur la structure des processus.

Deux aspects doivent être étudiés pour l'implantation de ce mécanisme :

- Le comportement des pragmas lors de l'expansion des processus : on décide que les pragmas de processus sont hérités par les objets du processus, de la même manière que le pragma d'un état est hérité par les objets du processus qui raffine cet état (voir l'exemple au chapitre 6).

- Un mécanisme permettant de transmettre les pragmas ARGOS aux variables des programmes DC qu'on obtient en bout de chaîne : la question se pose puisque, lors de l'étape de codage des programmes ARGOS en équations booléennes — que ce soit après ou avant l'expansion — on perd les structures syntaxiques auxquelles les pragmas étaient attachés. Si chaque état a été codé par une variable, le pragma d'état peut devenir le pragma de la variable. Pour les transitions, rien de tel n'est possible. Une solution est d'associer à chaque
transition syntaxique du programme ARGOS un signal de sortie. Ainsi la variable associée à ce signal est vraie exactement lorsque la transition est tirée. Le pragma de transition peut être attaché à cette variable.

## Autres connexions

Les connexions diverses qui avaient été implantées dans les premières versions du compilateur sont toujours possibles à partir d'un programme ARGOS expansé, c'est-à-dire à un seul processus. C'est le cas de la connexion à MEC [ABC94] et TOUPIE [Rau92]. Il faudrait réétudier la question pour une génération avant expansion.

La connexion à KRONOS est obtenue comme un cas particulier de la connexion à POLKA.
Cinquième partie

Recherche et enseignement
<figure><img src="image_64.png" /></figure>
# Chapitre 14

## Automates et programmation par
evénements en DEUG

Sources: *Ce chapitre est issu du travail réalisé avec P.-C. Scholl, M.-C. Fauvet et F. Lagnier pour l'enseignement de l'informatique en DEUG scientifique à Grenoble. La première partie, qui traite de l'étude des algorithmes de parcours séquentiels, est publiée dans [SFLM93], et effectivement enseignée. Suivent deux propositions, qui découlent assez naturellement de ce travail, et qu'il serait intéressant d'expérimenter : une approche de la preuve d'algorithmes séquentiels à travers leurs représentations en automates, et la description d'algorithmes de parcours par des programmes ARGOS.*

### 14.1 Motivations

Le but de ce chapitre est de montrer le lien étroit entre le domaine des systèmes réactifs et une application des techniques et outils définis dans ce cadre à des activités d'enseignement de premier cycle. La place manque pour replacer le chapitre dans le contexte global de l'enseignement de la filière considérée, et il sera donc peut-être difficile de juger du contenu sur des critères pédagogiques. L'essentiel du raisonnement, et la méthode consistant à définir des congruences par le biais d'abstractions, sont déjà développés dans le chapitre 3, à propos d'un modèle général permettant d'exprimer plusieurs modes de communication synchrone, afin de les comparer.

Les paragraphes 14.2 et 14.3 proposent une approche pour l'étude des algorithmes itératifs dans laquelle l'accent est mis sur la découverte des variables nécessaires à l'itération. Dans le cas où ces variables ont un domaine fini — de taille raisonnable — nous proposons au paragraphe 14.4 de représenter les algorithmes de parcours de séquence par des automates. Cette idée a deux aspects : conception des algorithmes sous forme d'automate, pour s'abstraire de la mécanique d'accès à la séquence et se concentrer sur la mise à jour de la mémoire ; preuve d'algorithmes représentés sous forme d'automates. Enfin nous proposons au paragraphe 14.5 d'utiliser les constructions d'ARGOS pour décrire des algorithmes itératifs.

### 14.2 Etude des algorithmes itératifs

La plupart des ouvrages d'initiation à l'algorithmique traitent de la construction des itérations en insistant sur la correction et sur la terminaison. C'est l'occasion d'introduire les invariants, les axiomes de la logique de Hoare, et de raisonner formellement sur des programmes. D'un point
<figure><img src="image_65.png" /><figcaption>FIG. 14.1 – Une machine d'accès séquentiel</figcaption></figure>

de vue méthodologique, on suggère également que la construction d'une itération commence par l'écriture de son invariant.

La question du choix des variables de l'itération est, en revanche, rarement abordée. Cela constitue pourtant un problème parfois difficile. D'autre part on juge souvent les algorithmes écrits par les étudiants sur des critères plus ou moins conscients d'élégance et de simplicité, et un mauvais choix des variables d'une itération conduit souvent à écrire un algorithme peu élégant, au sens où certaines informations manipulées sont inutiles au traitement demandé.

Ramenons tout de suite ces considérations à l'exemple typique "compter les 'LE' dans un texte". Les algorithmes sont donnés dans la notation algorithmique adoptée dans [SFLM93]. Il s'agit d'un pseudo-Pascal dont les mots-clé sont en français. On utilise un modèle d'accès séquentiel du type avec marque de fin (les chaînes de caractères en C par exemple), et on fournit les primitives suivantes données figure 14.1.

Exemple 14.1 : Un algorithme itératif : Compter les 'LE'

Version 1 :

<figure><img src="image_66.png" /></figure>

Version 2 :

<figure><img src="image_67.png" /></figure>

<figure><img src="image_68.png" /></figure>
Dans la version 1, on mémorise le caractère précédent, et c'est une information trop riche pour le traitement demandé. On s'en rend compte en observant comment est utilisée la variable *CarPrec*: elle n'apparaît que dans un test *CarPrec* = 'L'. Il suffit donc de mémoriser le booléen *CarPrec* = 'L'. Ce choix donne la deuxième version de l'algorithme, que beaucoup jugeront plus élégante. Un critère objectif d'élégance, dans ce cas précis, est le caractère minimal de la mémoire utilisée. La mémoire n'est pas minimale s'il en existe une abstraction qui est encore suffisante pour le traitement demandé ("abstraction" est pris au sens: image par une fonction non injective).

Il est intéressant de placer le discours à ce niveau, parce qu'aucun critère quantitatif de place mémoire ne peut justifier qu'on préfère un booléen à un caractère : les booléens, aussi bien que les caractères, sont en général codés sur un octet. On peut éventuellement discuter des temps d'exécution respectifs des instructions d'assemblage qui ont toutes chances d'être produites par la compilation de "si CarPrec = 'L'" et "si PrecEstUnL"<fnref n="1" />, mais le véritable argument est plus fondamental.

## 14.3 Un schéma général d'itération

L'étude détaillée des exemples où ce type de raisonnement sur la mémoire nécessaire intervient, nous a conduits à proposer un schéma général d'itération dans lequel on distingue des variables *d'historique* et des variables *résultat*. L'application systématique de ce schéma doit permettre de raisonner plus facilement sur la mémoire nécessaire au traitement.

### 14.3.1 Le schéma (figure 14.2 ci-dessous)

Le type typR, la fonction AccumulationDe, la constante ResInit et la variable R sont introduits pour décrire le calcul du résultat. Le type Histoire, la constante HistoireInitiale, la variable H et la fonction MiseAJour permettent de manipuler l'histoire, c'est-à-dire l'information qu'on a choisi de mémoriser pour permettre le calcul du résultat. Dans les commentaires, on fait référence à la partie gauche de la séquence, notée *pg*, déjà parcourue et traitée, qui représente la mémoire maximale que l'on pourrait conserver durant le parcours. Toutefois cette partie gauche n'est pas mémorisée. L'histoire H est une abstraction de la mémoire maximale, définie par une fonction non injective notée *Ab*, qui doit avoir la propriété suivante, dite *propriété de mise à jour*: $Ab(pg • EC) = f(Ab(pg), EC)$. En d'autres termes, la nouvelle histoire $Ab(pg • EC)$ doit pouvoir s'exprimer en termes de $Ab(pg)$ (l'histoire conservée jusqu'ici) et EC (l'élément courant) seulement. On exprime ainsi que l'abstraction choisie représente une information suffisante au traitement à réaliser, et on peut donc écrire $H \leftarrow MiseAJour(H, EC)$.

<footnote n="1">1. en 68000, il faut comparer, à mode d'adressage égal, les temps d'exécution des instructions *cmp* et *tst*, qui ne diffèrent pas sur des octets ; en SPARC la distinction n'existe pas, et ces deux opérations sont réalisées par des soustractions.</footnote>
<figure><img src="image_69.png" /><figcaption>FIG. 14.2 – Schéma de parcours séquentiel avec variables d'historique</figcaption></figure>

14.3.2 Utilisation du schéma pour raisonner sur la mémoire nécessaire

Lorsque le traitement à réaliser est complexe, et qu'il est difficile de choisir la mémoire, on
peut toujours commencer par écrire un algorithme où la mémoire est maximale. En analysant
ensuite, dans l'expression de la fonction AccumulationDe, comment est utilisée l'histoire, on peut
déterminer une abstraction suffisante.

**Exemple 14.2 : Un algorithme de parcours : majuscules et minuscules**

On considère une séquence de lettres. On désire construire une séquence modifiée, dans laquelle
les lettres de rang pair sont reproduites en majuscules, et les lettres de rang impair en minuscules.
On suppose l'existence de deux fonctions de traduction Maju et Minu. □

Si l'histoire utilisée est la partie gauche de la séquence (la mémoire maximale), on a :
$$ResInit = [] \text{ (la séquence vide) et}$$
$$AccumulationDe(H, EC, R) = R \bullet \text{ (si pair(longueur (H)) alors Minu(EC) sinon Maju(EC))}$$

Autrement dit, pour ajouter une lettre au résultat R en cours de construction, il suf-
fit de savoir déterminer pair(longueur (H)). On choisit donc comme fonction d'abstraction :
$Ab(s) = pair(longueur(s))$ où s est une séquence. Cette fonction d'abstraction a la propriété
requise pour la mise à jour, puisque : $Ab(s \bullet e) = pair(longueur(s \bullet e)) = pair(longueur(s) + 1)$
$= non\ pair(longueur(s)) = non\ Ab(s).$

Avec cette abstraction booléenne, on peut instancier le schéma général :

Histoire : le type booléen
ResInit : la séquence []
HistoireInitiale : le booléen vrai
MiseAJour (H, EC) = non H
AccumulationDe (H, EC, R) = R • (si H alors Minu(EC) sinon Maju(EC))
### 14.3.3 Abstractions trop fortes

Pour prouver *P* par récurrence, il peut être nécessaire de prouver une propriété plus forte que *P*, parce que *P* elle-même n'est pas inductive.

De même, dans la démarche décrite ci-dessus, l'examen de l'utilisation qui est faite de *H* dans la fonction d'accumulation (le calcul du résultat) peut conduire à une abstraction trop forte. Dans ce cas la fonction proposée n'a pas la propriété de mise à jour. Il peut être difficile de trouver l'histoire nécessaire et suffisante à un traitement donné. D'autre part la définition formelle de cette caractéristique est basée sur la notion de bisimulation de systèmes de transitions, et la présentation de ces aspects dépasse le cadre des enseignements de DEUG.

Il est toutefois possible d'illustrer la notion de mémoire trop, ou pas assez riche, sur des exemples décrits par des automates (voir paragraphe 14.4 ci-dessous).

### 14.3.4 Relation avec la conception des systèmes réactifs

Le schéma général proposé permet de faire abstraction de la structure de l'algorithme itératif (progression, terminaison), et doit donc permettre de se concentrer sur le choix et la fonction de mise à jour des variables d'historique.

Lorsqu'on décrit un système réactif dans un langage synchrone, on s'abstrait également des aspects d'interaction avec un environnement extérieur, pour se concentrer sur le noyau réactif. Si l'on programme dans un style impératif, on raisonne sur la mémoire (explicitement en ARGOS, où il faut inventer les états, implicitement en ESTEREL, où les structures de contrôle du langage cachent des états). En LUSTRE, au contraire, tout se passe comme si on décrivait simplement la fonction de calcul des sorties (assimilable à AccumulationDe) et jamais l'histoire. C'est le compilateur qui détermine une histoire suffisante au traitement demandé. Dans le cas de la génération d'automate minimal, le compilateur calcule l'histoire nécessaire et suffisante au traitement demandé. En ARGOS, comme en ESTEREL, il est possible d'écrire des programmes non minimaux. Si le compilateur produit des systèmes de transitions étiquetées, un outil comme ALDÉBARAN permet de minimiser l'automate résultat vis-à-vis d'une relation d'équivalence comme la bisimulation.

## 14.4 Automate d'états finis pour la représentation des algorithmes

Dans le cas où l'histoire est un type à domaine de valeurs fini, ses valeurs peuvent être représentées par les états d'un automate, et les mises à jour par les transitions de cet automate. Nous proposons d'étudier les algorithmes itératifs en se ramenant à l'étude des automates.

### 14.4.1 Exemple de système interactif: l'interface homme/machine d'un éditeur

Dans cette étude de cas, on raisonne sur l'automate qui décrit les opérations du menu *FI-CHIER* d'un éditeur. Le travail consiste à s'interroger sur la mémoire nécessaire à la réalisation des opérations courantes. Par exemple, si, lorsque l'on quitte l'éditeur, le logiciel propose de sauvegarder les fichiers pour lesquels cette précaution n'a pas été prise, mais seulement ceux-là, c'est qu'il est capable de "se rappeler" qu'il y a eu une modification du tampon d'édition depuis la dernière sauvegarde. Cela demande simplement un élément booléen dans la mémoire complète.
La spécification informelle du comportement de l'éditeur conduit ainsi à se poser 3 questions :

- Le tampon est-il vide ?

- Existe-t-il un nom de fichier courant ?

- Y a-t-il eu une sauvegarde du tampon depuis la dernière modification ?

Répondre à ces trois questions suffit, en toute circonstance, à déterminer la réaction de l'éditeur à un événement extérieur de l'ensemble { sauver, sauver_dans, charger, modifier, fermer, quitter } .

A première vue, cela pourrait donc donner 2 × 2 × 2 états pertinents. Toutefois certains d'entre eux sont inaccessibles. On développe le graphe d'états, à partir de l'état initial *tampon vide - pas de nom de fichier courant - tampon sauvegardé*, en envisageant les réactions à tous les événements extérieurs. 4 états seulement, parmi les 8 possibles, sont accessibles.

Le travail demandé est de deux ordres : travailler directement sur l'automate, pour prendre en compte des variantes de la spécification ; produire un algorithme itératif de simulation du comportement de l'éditeur, par un codage systématique des transitions de l'automate.

Parmi les variantes de spécification, on propose de supprimer l'action de fermeture de fichier. C'est un cas où la suppression de certaines transitions conduit à un automate non minimal pour la bisimulation. On pose alors la question : *tous les états sont-ils toujours nécessaires ?* On peut même coder l'automate dans un format accepté par ALDÉBARAN, et montrer aux étudiants le résultat de la réduction.

### 14.4.2 Preuve d'algorithmes représentés par des automates

On poursuit l'idée de représentation des algorithmes par des automates dans la direction de la preuve. Dans quelle mesure la représentation sous forme d'automate peut-elle aider à raisonner sur les algorithmes itératifs, et par exemple à prouver l'équivalence de deux algorithmes ? L'exemple exposé pourra sembler trop bien choisi pour ce propos, mais la démarche est applicable à tous les algorithmes de parcours de séquence, pour peu qu'ils soient à mémoire finie.

On s'intéresse au problème de la reconnaissance des multiples de 3 notés en base 2. La suite des chiffres est accessible grâce à une machine séquentielle qui fournit les chiffres des poids forts vers les poids faibles.

On écrit donc :

V : un entier $\ge 0$
Démarrer ; V $\leftarrow 0$
tant que non FinDeSéq
V $\leftarrow 2 * V + EC$
Avancer
Ecrire (V mod 3 = 0)

{ Calcul de la valeur entiere du nombre }

Toutefois il est inutile de calculer la valeur entière du nombre, puisqu'on ne s'intéresse qu'à sa valeur modulo 3, qu'on peut calculer de manière incrémentale en utilisant la remarque suivante : ajouter un chiffre 1 consiste à multiplier par 2 puis à ajouter 1, ajouter un chiffre 0 consiste à multiplier par 2. Or, si $x \equiv 0[3]$, alors $2x \equiv 0[3]$ et $2x + 1 \equiv 1[3]$ ; si $x \equiv 1[3]$, alors $2x \equiv 2[3]$ et $2x + 1 \equiv 0[3]$ ; si $x \equiv 2[3]$, alors $2x \equiv 1[3]$ et $2x + 1 \equiv 2[3]$.
<figure><img src="image_70.png" /><figcaption>FIG. 14.3 – Reconnaissance des multiples de 3 en base 2 – définition directe</figcaption></figure>

D'où l'algorithme :

V3 : un entier dans $[0..2]$

Démarrer ; V3 ← 0

tant que non FinDeSéq

selon V3 :

V3 = 0 : si EC = 1 alors V3 ← 1

V3 = 1 : si EC = 0 alors V3 ← 2 sinon V3 ← 0

V3 = 2 : si EC = 0 alors V3 ← 1

Avancer

Ecrire (V3 = 0)

Ce qui correspond à l'automate de la figure 14.3, où l'état 0 est accepteur.

D'autre part un théorème d'arithmétique établit qu'un nombre est congru, modulo $b + 1$, à la différence entre la somme de ses chiffres en base $b$ de rang pair, et la somme de ses chiffres en base $b$ de rang impair.

La preuve est simple : on considère un entier $c$ dont on suppose, sans perte de généralité, qu’il a un nombre pair de chiffres en base $b$ (le cas échéant, on rajoute un chiffre 0 à gauche).

$$c = \sum_{i=0}^{n} c_i \cdot b^i \text{ avec } n = 2m + 1$$

$$c = \sum_{i=0}^{m} (c_{2i} \cdot b^{2i} + c_{2i+1} \cdot b^{2i+1}) = \sum_{i=0}^{m} (c_{2i} - c_{2i+1} + c_{2i} \cdot (b^{2i} - 1) + c_{2i+1} \cdot (b^{2i+1} + 1))$$

or $b^{2i} - 1$ et $b^{2i+1} + 1$ sont des multiples de $b + 1$, puisque $-1$ en est une racine, et ceci quel que soit $i \ge 0$. D'où

$$c \equiv \sum_{i=0}^{m} c_{2i} - \sum_{i=0}^{m} c_{2i+1} \quad [b+1]$$

Donc les multiples de $b + 1$ en base $b$ sont tels que la différence entre la somme des chiffres de rang pair et la somme des chiffres de rang impair est aussi un multiple de $b + 1$. On écrit un algorithme basé sur cette propriété :

Sp, Si : des entiers $\ge 0$ ; Pair : un booléen

Démarrer ; Sp ← 0 ; Si ← 0 ; Pair ← faux

tant que non FinDeSéq

si Pair alors Sp ← Sp + EC sinon Si ← Si + EC

Pair ← non Pair

Avancer

Ecrire ((Sp - Si) mod 3 = 0)

Bien sûr la différence des sommes peut être calculée directement, et l'on obtient :
<figure><img src="image_71.png" /><figcaption>FIG. 14.4 – Reconnaissance des multiples de 3 en base 2 – propriété</figcaption></figure>

S : un entier ; Pair : un booléen
Démarrer ; S ← 0 ; Pair ← faux
tant que non FinDeSéq
si Pair alors S ← S + EC sinon S ← S − EC
Avancer
Ecrire (S mod 3 = 0)

Et, de nouveau, il est inutile de calculer S puisque l'on ne s'intéresse qu'à sa valeur modulo 3, qui peut être déterminée incrémentalement. Le nouvel algorithme se déduit des propriétés du modulo exposées précédemment et de l'alternance entre rangs pairs et rangs impairs. Il correspond à l'automate de la figure 14.4, où les états 0i et 0p sont accepteurs.

Prouver l'équivalence de deux algorithmes (par exemple, prouver qu'ils conduisent à la même valuation des variables, s'ils travaillent sur les mêmes données) n'est pas chose aisée ; c'est même en général indécidable. Toutefois, dans le cas où les algorithmes de parcours séquentiel manipulent des histoires à domaine fini, on peut les représenter par des automates, et l'équivalence d'algorithmes se ramène alors à l'équivalence de traces de ces automates.

Ainsi il est aisé de montrer que les automates des figures 14.3 et 14.4 sont équivalents par l'équivalence de traces, et reconnaissent donc le même langage sur le vocabulaire {0, 1} des chiffres en base 2.

Ceci fournit d'ailleurs une démonstration automatique du théorème d'arithmétique, pour une base particulière. On pourrait donner une définition générale des deux automates exhibés ci-dessus, pour une base quelconque, et montrer qu'ils sont équivalents pour l'équivalence de trace, mais ce ne serait plus automatique.

14.5 **Proposition :**
description des algorithmes itératifs en ARGOS

Jusque là nous avons décrit les algorithmes itératifs par des automates, c'est-à-dire des struc-
tures plates. Je propose ici d'utiliser les constructions d'ARGOS comme la mise en parallèle et le
raffinement, pour décrire des algorithmes dans lesquels une boucle unique impose de trop fortes
contraintes.

La figure 14.5 donne un algorithme de calcul de la longueur moyenne des mots dans un texte
<figure><img src="image_72.png" /><figcaption>FIG. 14.5 – Calcul de la longueur moyenne des mots dans un texte pourvu de commentaires</figcaption></figure>

pourvu de commentaires délimités aux deux extrémités par des accolades. Remarquons tout d'abord que la longueur moyenne des mots est simplement le résultat de la division du nombre de lettres par le nombre de mots (on oublie volontairement le cas où le nombre de lettres est nul). Il faut pour compter les lettres et les mots ne tenir compte que des parties *significatives* du texte, c'est-à-dire celles situées hors des commentaires.

Le programme ARGOS reflète exactement la structure qu'il faut plaquer sur le texte lu pour réaliser les calculs demandés : la structure principale exprime que le dernier caractère (la marque de fin) est traité à part, et que tout le comportement qui raffine l'état EN COURS doit être interrompu lorsqu'on lit la marque. La structure intérieure a deux états COMM et HORS COMM qui définissent les portions de commentaires : elles commencent par une accolade ouvrante, et se terminent par une accolade fermante. Au début du texte, on est hors de tout commentaire. Enfin la structure qui raffine l'état HORS COMM est une composition parallèle : le premier composant s'occupe de compter les lettres, et n'a pas de mémoire ; le deuxième composant définit la notion de mot : on reconnaît un début de mot comme un couple constitué d'un séparateur et d'une lettre : ceci nécessite une mémoire booléenne, l'état Hors Mot signifiant “*le dernier caractère lu était un séparateur*”. Notons que le début du texte est aussi un début de mot.

Quelques remarques :

- Si l'on écrit directement un algorithme itératif de parcours de la séquence, basé sur cette structure du texte, on obtient assez naturellement des itérations emboîtées :
Démarrer

Tant que non FinDeSéq

tant que non FinDeSéq et puis EstS(EC) : Avancer

...

Les itérations emboîtées sont également conditionnées par non FinDeSéq. On observe sou-
vent chez les étudiants des écritures incorrectes basées sur une interprétation erronée de
la sémantique du tant que, qui consiste à croire que la condition du tant que le plus ex-
terne “s’ajoute”, en quelque sorte, aux conditions des itérations emboîtées, et qu’il est donc
inutile de la rappeler.

Nous écrivions au chapitre 9 que *Dans les langages séquentiels, il est possible de comprendre le corps d'une itération en s'abstrayant de la condition de continuation. En revanche, un chien de garde ESTEREL interagit avec son corps à tout instant de l'exécution de celui-ci.*
Cette même remarque s'applique ici: lorsque l'algorithme est décrit en ARGOS, l'automate contrôleur du raffinement (qui joue le rôle du chien de garde) fonctionne en parallèle avec le processus raffinant: lui seul s'occupe de la détection de fin de séquence, et contrôle tous les parcours décrits dans les processus raffinants.

- La composition parallèle (sans communication ici) correspond très exactement au méca-
nisme de repliage des fonctions. Si l'on écrit d'une part un algorithme de parcours séquentiel
qui compte les lettres, d'autre part un algorithme de parcours séquentiel qui compte les
mots, il est ensuite aisé de les rassembler pour décrire le même calcul en un seul parcours
de la séquence. En style fonctionnel, cela revient à fusionner deux fonctions à un résultat
en une seule fonction à résultat couple.

La composition parallèle permet de décrire l'indépendance des deux calculs, sans imposer
la structure de mots à la portion de programme dans laquelle on compte les lettres.

14.6 Conclusion provisoire

Le point de vue développé ici sur la construction des itérations conduit à un raisonnement
sur la quantité et la nature des informations nécessaires à un traitement donné, qui peut être
développé indépendamment de toute technique de programmation. En un sens, et au risque de
paraître pompeux, disons que c'est “l'essence” du raisonnement informatique.

Ce niveau de réflexion peut sembler hors de portée des étudiants de DEUG. La manipulation
éditeur de textes permet de concrétiser quelque peu les choses. L'expérience montre que certains
étudiants produisent intuitivement la réduction d'un automate par l'équivalence de trace.
# Chapitre 15

## Description de circuits en Lustre et VHDL, niveau Licence

Sources: *Ce chapitre rassemble quelques réflexions issues du travail dans l'équipe du module ALM (Architectures Logicielles et Matérielles) de première année de l'Ecole Universitaire d'Informatique de Grenoble. Les enseignements décrits sont anciens et il est parfois difficile d'en retrouver toutes les sources, mais pour les 6 dernières années il faut remercier P. Amblard, J.-C. Fernandez, F. Lagnier, P. Sicard et Ph. Waille.*

### 15.1 Le contexte

Le module *Architectures Logicielles et Matérielles* rassemble dans une présentation unifiée les enseignements traditionnels de logiciel de base (programmation en assembleur, vie des programmes, première approche des systèmes d'exploitation) et d'architecture des machines (algèbre de Boole, circuits combinatoires et séquentiels, structure des processeurs, etc.). Pour les aspects matériels, l'objectif est de faire comprendre la structure des circuits et de montrer, en particulier, que la démarche de conception de ces "algorithmes matériels" est identique à la démarche de conception des algorithmes "logiciels" (spécification de blocs, abstraction et réutilisation...). On arrive ainsi à la conclusion que de nombreux problèmes peuvent recevoir des solutions logicielles ou matérielles, voire mixtes, selon les critères que l'on privilégie.

Cette année les travaux pratiques de conception de circuits sont réalisés en VHDL. On utilise des outils commerciaux de simulation et un outil de synthèse pour carte Xilinx. Puisque l'enseignement vise à faire comprendre dans les détails la structure des circuits, et la frontière entre matériel et logiciel, il est hors de question d'utiliser le langage VHDL dans toute sa puissance d'expression, et de faire confiance aux outils de synthèse pour produire des circuits difficilement analysables. On se restreint donc à un sous-ensemble dit *structurel*, qui ressemble énormément à LUSTRE booléen avec tableaux (on ne manipule pas directement les entiers, par exemple, mais des nappes de fils). Les mêmes sujets de travaux pratiques sont traités en VHDL pour une partie de la promotion de première année, et en LUSTRE pour l'autre partie (avec utilisation d'outils de Vérilog).

Puisque la distance est si faible entre LUSTRE et le sous-ensemble de VHDL utilisé, l'idée de traduire l'un dans l'autre est assez naturelle. Si l'on décrit un circuit en LUSTRE, on bénéficie de tous les environnements de preuve, test et simulation de la communauté synchrone. Une traduction en VHDL permet ensuite d'accéder aux outils de synthèse pour les cartes Xilinx
<figure><img src="image_73.png" /><figcaption>FIG. 15.1 – *Structure d'un additionneur n bits*</figcaption></figure>

(rappelons que la thèse de F. Rocheteau [Roc92] traitait de la programmation des cartes Xilinx en LUSTRE avec tableaux).

D'autre part, puisqu'on sait mélanger ARGOS et LUSTRE, il ne doit pas être trop difficile de mélanger ARGOS et VHDL. Les techniques de réalisation matérielle d'algorithmes dits partie contrôle/partie opérative constituent d'excellents exemples de description mixte impératif/déclaratif.

## 15.2 Traduction Lustre vers VHDL

Nous donnons ici un exemple de circuit décrit en LUSTRE et en VHDL (tables 15.1 et 15.2). La version LUSTRE est due à J.-C. Fernandez et la version VHDL à un étudiant. C'est un additionneur n bits décrit comme composition de n additionneurs 1 bit (voir figure 15.1). Les deux programmes sont très similaires, à des détails de syntaxe près. La principale difficulté de traduction de l'un vers l'autre réside dans les mécanismes de description des circuits génériques répétitifs. En LUSTRE on dispose d'opérations sur des tranches de tableaux. En VHDL on écrit des boucles FOR et on manipule explicitement les indices dans les tableaux.

## 15.3 Argos et VHDL

Les outils VHDL dont on dispose acceptent des descriptions de parties contrôle sous forme de machines de Moore ou de Mealy. Dans les travaux pratiques, nous montrons comment coder systématiquement, à la main, une machine de Moore en équations booléennes.

L'utilisation d'ARGOS n'apporte donc rien pour la description de parties contrôles simples, données sous forme d'automates. L'intérêt d'ARGOS réside dans ses constructions, qui autorisent la description des parties contrôle par des coopérations d'automates, et non plus seulement par des automates plats. Cela peut permettre, en utilisant la structure du programme, de déterminer un codage astucieux et économique des états (voir [DY90] déjà cité au chapitre 5 et [VNG91] qui décrit le langage des SPECCHARTS, une variante des Statecharts compilable en VHDL).

Enfin on pourrait proposer une syntaxe pour ARGOS avec tableaux, en s'inspirant à la fois de LUSTRE avec tableaux et de la syntaxe de VHDL pour les vecteurs.
node add1 ( x, y, cin : bool)
    returns ( s, cout : bool);
let
    s = x xor y xor cin;
    cout = if cin then (x or y) else (x and y);
tel
node addn ( const n : int; X, Y : bool^n)
    returns ( S : bool^n; cout, v : bool);
var
    C : bool^n;
let
    (S[0], C[0]) = add1bit(X[0], Y[0], false);
    (S[1..n-1], C[1..n-1]) =
        add1bit(X[1..n-1], Y[1..n-1], C[0..n-2]);
    cout = C[n-1];
    v = (X[n-1] and Y[n-1] and not S[n-1]) or
        (not X[n-1] and not Y[n-1] and S[n-1]);
tel
node add4 ( X, Y : bool^4)
    returns ( S : bool^4; cout, v : bool);
let
    S, cout, v = addn (4, X, Y);
tel

<caption>TAB. 15.1 – *Additionneur n bits en LUSTRE*</caption>
entity add1 is port (x, y, cin : in bit; s, cout : out bit);
end add1;
architecture add1_int of add1 is
begin
  s <= x xor y xor cin;
  cout <= (x and y) or (x and cin) or (y and cin);
end add1_int;

ENTITY addn IS
  GENERIC (n:INTEGER);
  PORT (X, Y : IN BIT VECTOR (n-1 downto 0);
        S : OUT BIT VECTOR (n-1 downto 0); cout, v : OUT BIT );
END addn;

ARCHITECTURE addn_int OF addn IS
  COMPONENT add1 PORT (x,y,cin : IN BIT ; s, cout : OUT BIT );
  END COMPONENT;
  FOR ALL : add1 USE ENTITY work.add1(add1_int);
  SIGNAL retenue : BIT VECTOR (n downto 0);
BEGIN
  retenue (0) <= '0';
  cout <= retenue (n);
  v <= (X(n-1) and Y(n-1) and not S(n-1)) or
       (not X(n-1) and not Y(n-1) and S(n-1));
  etiq1 : FOR i IN 0 TO n-1 GENERATE
    etiq2 : add1 PORT MAP (X(i),Y(i),retenue(i),S(i),retenue(i+1));
  END GENERATE;
END addn_int;

entity add4 (X4, Y4 : IN BIT VECTOR (3 downto 0);
             S4 : OUT BIT VECTOR (3 downto 0); cout4, v4 : OUT BIT );
END add4;

ARCHITECTURE add4_int OF add4 IS
  CONSTANT NBits : INTEGER := 4;
  COMPONENT addn
    GENERIC (n : INTEGER);
    PORT (X, Y : IN BIT VECTOR (n-1 downto 0);
          S : OUT BIT VECTOR (n-1 downto 0); cout, v : OUT BIT );
  END COMPONENT;
  FOR ALL addn USE ENTITY work.addn(addn_int);
BEGIN
  etiq: addn      GENERIC MAP (n => NBits)
                            PORT MAP (X4, Y4, S4, cout4, v4);
END add4_int;

<caption>TAB. 15.2 – *Additionneur n bits en VHDL structurel*</caption>
# Chapitre 16

## Quelques remarques en guise de
conclusion

On trouvera les points “bilan” et “perspectives” d’une conclusion classique dans les remarques présentées ci-dessous. Le résumé des activités fait partie de l’introduction. Les remarques se rangent dans un ou plusieurs points ci-dessous :

- Tout d’abord, une tentative de réponse à la question : “à quoi ça sert ?”, qu’il est assez naturel de se poser après 10 ans de travail sur un sujet — et qu’on me posera sans doute.

- L’exposé d’une direction pour la suite, à la fois direction de recherche et choix de la nature du travail. Cela s’appuie naturellement sur un bilan des résultats obtenus et de leur diffusion, mais aussi sur un ensemble de réflexions plus personnelles à propos de la place d’un enseignant/chercheur dans une équipe de recherche engagée dans des collaborations industrielles.

- Un retour sur les influences réciproques entre enseignement et recherche, accompagné de quelques réflexions sur la place de mon domaine de recherche au sein de la discipline informatique. En une dizaine d’années d’enseignement de sujets assez divers à des publics variés, on finit par se forger une certaine image globale de la discipline, qui rejaillit sur la manière d’aborder les problèmes, sur la manière de les enseigner et, de façon plus fondamentale, sur le choix de ce que l’on enseigne. Il s’agit ici de mettre en forme cette image globale — aussi subjective soit-elle — pour essayer de répondre à la question : “Quels résultats/approches/techniques de ce domaine de recherche sont ou pourraient être utilisés en enseignement, pourquoi, et à quel niveau ?”.

### Recherche

#### Bilan

Puisque le titre de ce document annonce “un langage à base d’automates”, la question se pose de savoir si l’on peut considérer ARGOS comme un véritable langage. La réponse est non, pour une grande variété de raisons.

En particulier, je ne crois pas à un véritable langage dont la syntaxe serait uniquement graphique. Les défauts d’une syntaxe graphique sont exposés en introduction du chapitre 9 comme l’une des motivations de l’approche ARGOS+ESTEREL, et les difficultés liées à la définition
d'un outil d'édition sont relatées au chapitre 12 (la notion d'analyseur syntaxique d'un langage à deux dimensions n'est pas aussi naturelle que ne l'est devenue celle de l'analyse syntaxique de texte, et les éditeurs sont donc nécessairement syntaxiques). D'autre part, indépendamment de la syntaxe concrète, qu'on pourrait après tout choisir textuelle, les constructeurs d'ARGOS sont en nombre limité, et il est assez contraignant d'utiliser des automates pour décrire certains types de comportements réactifs. Enfin l'environnement de programmation autour d'ARGOS n'est qu'un ensemble de maquettes plus ou moins éprouvées, complété par des prototypes de connexion à différents outils du domaine.

Toutefois cet état de faits relève d'une décision délibérée. Les travaux sur ARGOS n'ont pas été réalisés avec un objectif de transfert rapide vers l'industrie, ni même de large diffusion. L'industrialisation de LUSTRE ou ESTEREL montre bien l'ampleur de la tâche, et la nature des activités qu'il faut avoir : développement et maintenance de logiciel très conséquent, études de cas nombreuses, etc. Ces activités diverses et difficiles — car il y a un pas énorme entre le développement d'une petite maquette à des fins d'expérimentation dans un environnement de recherche, et le développement d'un prototype au moins maintenable et si possible évolutif — ne peuvent être menées qu'en équipe et, à mon sens, par du personnel "suffisamment" permanent pour assurer un minimum de continuité. Pour se lancer dans des activités de développement avec des objectifs de diffusion ou de transfert, il faut donc s'en donner les moyens matériels et humains, et cela n'est envisageable qu'une fois le sujet raisonnablement cerné.

L'étude du langage ARGOS proprement dit a joué jusqu'à présent un rôle exploratoire, et la question de son transfert ne se pose véritablement que maintenant. En effet, les problèmes de fond d'un langage synchrone à base d'automates, et d'un environnement de programmation synchrone multi-langages, ont été étudiés et résolus.

Malgré l'absence d'un prototype largement diffusable, les idées d'ARGOS émergent, parmi les douzaines de sémantiques proposées pour les Statecharts, comme la base formelle raisonnable d'un langage réactif offrant des automates hiérarchiques. Joe Buck, de Synopsys, travaille sur une extension d'ESTEREL qui introduit une construction tirée du raffinement d'ARGOS. L'équipe d'Axel Poigné à la GMD travaille sur un environnement de programmation synchrone intégrant LUSTRE, ESTEREL et ARGOS. Charles André, à Nice, a défini le formalisme des SyncCharts, où la structure hiérarchique des automates a la sémantique du raffinement Argos ; les SyncCharts sont en voie d'industrialisation. Nous travaillons d'autre part à l'introduction de structures à états et transitions dans SAO+ (l'environnement de programmation basé sur Lustre et industrialisé par la société Vérilog), et la sémantique d'Argos est déjà une base de travail intéressante.

D'autre part le prototype de compilateur, connecté à l'outil KRONOS de Vérimag, a été utilisé avec succès dans le cadre du stage post-doctoral de Muriel Jourdan dans l'équipe de Bernard Espiau.

En ce qui concerne les travaux sur le multi-langages, étudier la programmation mixte AR-
GOS/LUSTRE ou ARGOS/ESTEREL a permis d'identifier ce que peut apporter ARGOS à un environ-
nement de programmation des systèmes réactifs basé sur l'un des langages bien établis. Ainsi le
langage mixte ARGOS/ESTEREL peut-être vu comme une proposition d'extension d'ESTEREL, par
introduction d'une structure de contrôle temporelle inspirée du raffinement ARGOS, mais héri-
tant de la richesse des modes de terminaison ESTEREL. Le langage mixte ARGOS/LUSTRE permet
de s'intéresser au problème de la réinitialisation dans un langage flot de données, et d'étudier
comment les constructions d'automates se marient avec une structure flot de données.

En résumé, les travaux autour d'ARGOS ont permis d'explorer les compositions d'automates synchrones, et de montrer les points de convergence entre les langages de description graphiques
à la Statecharts et un langage parfaitement défini comme ESTEREL ou LUSTRE. Les extensions temporelles et hybrides, ainsi que l'utilisation des automates en algorithmique, suggèrent d'autres champs d'exploration.

## Perspectives

Les divers travaux autour de la définition d'ARGOS me semblent maintenant parvenus à un point de convergence.

Pour les raisons énoncées plus haut, le développement complet de ce qui serait un véritable langage, muni de son environnement de programmation propre, ne constitue pas nécessairement la seule poursuite envisageable. Le travail me semble pouvoir maintenant être organisé selon deux axes :

- L'étude des compositions d'automates dans des contextes plus larges que le contexte des langages synchrones, avec de nouveaux objectifs d'exploration de la définition des langages, plutôt que de production d'environnements de programmation. Ceci demande le développement d'un prototype de compilateur ARGOS comme moteur de composition d'automates synchrones décorés, utilisable comme langage de description dans tout environnement qui manipule des automates plats. C'est ce que nous avons fait pour POLKA, et l'idée est généralisable. Un tel environnement permettrait également d'expérimenter les idées sur l'introduction du non déterminisme dans les langages synchrones, et l'utilisation des compositions synchrones d'automates dans l'enseignement de l'algorithmique. C'est un projet maîtrisable en développement logiciel, dans un contexte universitaire.

- L'utilisation et l'application de l'expérience et des résultats acquis sur les constructions d'automates dans le cadre synchrone.

La demande industrielle nous oriente vers la définition d'une extension de LUSTRE à l'aide d'automates, avec un point de vue assez différent de l'approche "édition de liens" que nous suivions jusqu'ici. Il s'agit d'utiliser un automate comme structure de contrôle appliquée à la définition d'un ensemble de flots $X_1, X_2, \text{etc.}$, dont chaque état définit un mode d'évolution possible de chacun des flots. La définition globale des flots est une union de ces différentes définitions. Un exemple typique consiste à calculer une fonction affine par morceaux : dans un état le flot $X$ est défini par $X = \text{pre}(X) + 1$, dans un autre état par $X = \text{pre}(X) - 1$. Il s'agit bien du même $X$. On peut proposer une syntaxe où des équations LUSTRE apparaissent dans les états d'un automate, mais l'interprétation n'est plus celle du raffinement ARGOS : l'ensemble d'équations d'un état ne constitue pas un processus qu'il faudrait détruire et relancer dans son état initial. Si l'on adopte une vision circuit séquentiel, le changement d'état consiste à remplacer, en cours de fonctionnement, une fonction de transition par une autre, en conservant la mémoire. La variable $X$ est ainsi globale à l'automate.

Cette approche, si elle semble ne poser que des problèmes théoriques déjà bien cernés, pose des problèmes spécifiquement "langage". Il sera toujours possible de proposer une sémantique pour un langage mixte de ce genre, mais correspondra-t-elle à l'interprétation intuitive ? Si la définition d'une variable $X$ apparaît dans certains états et non dans d'autres, doit-on considérer qu'il existe une définition par défaut $X = \text{pre}(X)$, ou bien que les états jouent le rôle d'horloges LUSTRE, et que la variable $X$ est non disponible lorsque non explicitement définie ? La structure d'automate plat suffit-elle, ou doit-on prévoir l'extension
à des contrôleurs structurés, au moins hiérarchiquement ? Toutes ces questions doivent être étudiées à partir d'un ensemble d'exemples significatifs.

D'autre part, dans un contexte plus théorique, et comme préalable à l'introduction de non déterminisme dans les constructions synchrones, il faut se pencher sur l'étude d'une relation d'équivalence d'objets non déterministes, compatible avec le point de vue selon lequel un objet non déterministe représente un ensemble d'objets déterministes. C'est un travail peut-être moins technique que de bibliographie, puisque ce point de vue prévaut dans une certaine communauté, à propos de raffinements de spécifications vers des programmes. Mais il me semble intéressant d'essayer de comprendre les rapprochements possibles entre les résultats de cette communauté, et ceux de la communauté algèbres de processus — que je connais mieux — où la bisimulation est reine.

## Enseignement et recherche

La position d'enseignant/chercheur dans une UFR qui a la charge des enseignements d'informatique du premier jusqu'au troisième cycle offre de nombreuses possibilités d'intervention.

Enseigner directement son sujet de recherche est une possibilité, mais c'est par nature limité à des enseignements optionnels d'ouverture ou à des enseignements de troisième cycle. D'autre part c'est une vision à mon avis un peu étroite de ce que peut apporter un domaine de recherche à l'enseignement ; il y a bien des choses à enseigner aux étudiants de premier et second cycle, avant d'en faire des experts en systèmes réactifs (par exemple). Une autre façon de voir les choses, à mon avis plus riche, est de considérer que chaque domaine se caractérise par des préoccupations, une démarche, des résultats et des techniques particulières, qu'il est intéressant d'utiliser pour colorer l'enseignement général en premier et second cycle. La richesse des équipes d'enseignants vient souvent — pour ne pas dire toujours — d'une confrontation de points de vue ; et ces points de vue sont souvent le reflet des préoccupations d'environnements de recherche différents.

## Utilisation de la culture "méthodes formelles pour les systèmes réactifs"

Plus précisément, quelles sont les préoccupations, la démarche, les résultats et les techniques utilisés dans la conception et la validation des systèmes réactifs ? La calculabilité est à la base de nombreux choix, puisqu'on essaie toujours de trouver des compromis entre décidabilité et expressivité des modèles de programmes. L'analyse de complexité est une priorité parce que les algorithmes sont étudiés pour être implantés et traiter des exemples conséquents ; de plus, c'est un domaine où l'on fait peu de distinction, en pratique, entre des problèmes de très grande complexité (qu'on ne pourrait résoudre qu'avec des algorithmes très coûteux) et des problèmes indécidables. D'où l'émergence des techniques de vérification approchée, qui conduisent à réfléchir sur les abstractions raisonnables des programmes. La théorie du point fixe et la sémantique sont nécessaires puisqu'on s'intéresse à la définition formelle des langages ; la compilation et les techniques usuelles de développement des compilateurs sont indispensables dans un cadre qui privilégie l'interconnexion des outils par une grande variété de formats et de langages intermédiaires.

Sans prétendre avoir des compétences très élaborées sur chacun de ces différents points, il me semble que le travail de définition de méthodes et outils de validation des systèmes réactifs, sachant que le preuve formelle du système réel est hors d'atteinte, et en tenant compte de
préoccupations relatives à la définition de langages, donne une expérience assez large, depuis les aspects formels jusqu'à l'implantation.

Cette expérience et ce point de vue m'ont confirmé l'idée que les enseignements de base, disons de première année de second cycle pour fixer les idées, sont intimement liés, et gagneraient à être présentés de manière moins indépendante. Les outils théoriques ont par exemple leur place dans des enseignements du style "mathématiques pour l'informatique" <fnref n="1" />, et une bonne partie des sujets qui y sont abordés est également à la base de toutes les définitions syntaxiques et sémantiques des langages. Parallèlement, l'expérience sur la définition et l'implantation des langages s'acquiert avec l'algorithme en général, la compilation, des aspects de plus bas niveau comme le logiciel de base, et même la conception de circuits décrits dans des langages comme VHDL<fnref n="2" />. La mise en place d'un projet de programmation d'un assembleur/éditeur de liens pour sparc, sous la forme d'une collaboration entre les modules L&P et ALM, m'a convaincue de l'intérêt, pour les étudiants, d'un contexte dans lequel les connaissances acquises dans deux modules différents, avec des ambiances d'enseignement différentes, sont utilisées conjointement. J'aimerais compléter le schéma en étendant le projet aux modules qui traitent des outils théoriques nécessaires, dont par exemple les machines d'états finies utilisées en analyse lexicale.

Finalement, du domaine plus particulier des *langages synchrones* pour la description et la validation des systèmes réactifs, on peut extraire la notion de *parallélisme de description* — par opposition au parallélisme d'exécution, qu'il soit réel ou simulé — et essayer de l'utiliser comme paradigme de programmation. Dans [SFLM93], on insiste sur la variété des modes d'expression, et on illustre ce discours par l'étude des paradigmes fonctionnel, actionnel et relationnel. Il faudrait compléter cet ensemble par la programmation concurrente ou logique, l'orienté objet, les tableaux, etc. Pour les aspects de programmation concurrente, il me semble que les langages synchrones sont le moyen idéal d'introduire la conception parallèle sans s'encombrer de vrai parallélisme — c'est-à-dire de machines parallèles et d'algorithmique distribuée — simplement comme un autre moyen de concevoir les programmes séquentiels. Nous avons vu au chapitre 14 paragraphe 14.5 une version ARGOS d'un algorithme de parcours de séquence de lettres qui calcule la longueur moyenne des mots. Le parallélisme qui y apparaît est purement descriptif, et le programme est fait pour être compilé en code séquentiel. C'est la même notion de "parallélisme" que celle qui apparaît en filigrane dans la technique de repliage des fonctions: comment faire en un seul parcours d'une séquence, à la fois le calcul de la longueur et le calcul de l'élément maximum? Il s'agit en fait de décrire l'exécution "parallèle" de deux algorithmes de parcours de séquence.

## A propos du transfert des méthodes formelles

Une question rituelle se pose dans les environnements de recherche où l'on s'occupe de "méthodes formelles", quelle que soit l'étendue du domaine que cela recouvre: "comment assurer le transfert de ces fameuses méthodes formelles, de la recherche vers l'industrie?". J'aimerais ici apporter quelques arguments pour une réponse à cette question, en adoptant le point de vue d'un enseignant-chercheur, pour qui le problème est aussi celui du transfert des méthodes formelles de la recherche vers la formation.

C'est une vision à long terme, qui certes demande de la patience dans la simple observation des résultats. Mais, quand on y songe un peu, c'est bien aujourd'hui qu'il faut se préoccuper de

<footnote n="1">1. à Grenoble il existe plusieurs modules intitulés "Outils Formels pour l'Informatique" au niveau Bac+3</footnote>

<footnote n="2">2. à Grenoble, cela concerne donc à Bac+3 les modules L&P — Langages et programmation — et ALM — Architectures Logicielles et Matérielles</footnote>
la formation des ingénieurs qui réaliseront les systèmes informatiques des avions dont dépendra notre sécurité dans 10 ou 15 ans.

La question du transfert des méthodes formelles recouvre donc aussi la question “comment enseigner les méthodes formelles?”. Commençons par préciser quelque peu les objectifs d’un tel enseignement, ainsi que les contenus susceptibles de remplir ces objectifs.

Une manière de répondre à ces questions — *comment, pourquoi et quoi?* — consiste à proposer, par exemple, l'étude de la théorie des logiques temporelles dans un cours de DEA. Une autre manière, qui suppose moins d'acquis du public, consiste à définir une option de niveau Bac+4 à propos des systèmes temps-réel, "spécification en logique temporelle et validation de protocoles décrits en Lotos" ; ou bien "des observateurs synchrones pour un système de contrôle/commande décrit en Lustre". Mais cela suppose encore de nombreux acquis.

A l'opposé, si l'on cherche à décomposer très finement l'ensemble des techniques et méthodes qu'il faudrait maîtriser pour assimiler parfaitement un cours sur la spécification formelle d'un système réactif, on se rend compte que nombre des points qui apparaissent peuvent être présentés, d'une part indépendamment des systèmes réactifs, et d'autre part assez tôt dans la formation, par exemple en premier cycle.

A mon sens, on commence à enseigner les méthodes formelles en habituant les étudiants à l'idée qu'un programme est, certes, exécutable, mais que c'est aussi un objet sur lequel il est possible de raisonner : on peut analyser un programme pour lui trouver des propriétés particulières ; le transformer de manière systématique en respectant le sens ; évaluer sa complexité en temps, etc. On a même le droit, toutes choses égales par ailleurs, de préférer une version à une autre pour des critères d'élégance et de simplicité. On oublie sans doute trop souvent que cette idée est loin d'être naturelle pour des étudiants de premier cycle qui se sont forgé leur image personnelle de la discipline dans la presse informatique.

La deuxième étape dans cette formation de longue haleine peut consister à pratiquer la preuve ou la comparaison de programmes dans des cas très simples, par exemple en étudiant des systèmes séquentiels à nombre fini d'états. Il est même possible, dans ces cas simples, de passer à l'étage supérieur : l'automatisation de telles preuves. Je m'appuie ici sur l'expérience décrite au chapitre 14, où il s'agissait de programmer l'interface d'un éditeur de textes à l'aide d'automates. On arrivait assez naturellement, et sans besoin de développer une théorie élaborée, à la notion d'équivalence de trace de systèmes de transitions étiquetées, et donc à la notion d'équivalence des programmes correspondants, produits de manière systématique.

L'étape suivante consiste à travailler sur la preuve de programmes séquentiels non finis, en introduisant une représentation symbolique des états par des prédicats. On peut d'ailleurs assez vite se restreindre à l'utilisation de ces assertions pour la construction des programmes plutôt que pour leur preuve a posteriori.

Il reste finalement à particulariser cette culture de raisonnement plus ou moins automatisable sur les programmes, au cas des systèmes réactifs.
Bibliographie

[AB84] Austry (D.) et Boudol (G.). – Algèbre de processus et synchronisation. *TCS*, vol. 30, avril 1984.

[ABC94] Arnold (A.), Bégay (D.) et Crubillé (P.). – *Construction and analysis of transition systems with MEC*. – World Scientific Publishing, 1994.

[ACH+92] Alur (R.), Courcoubetis (C.), Halbwachs (N.), Dill (D.) et Wong-Toi (H.). – Minimization of timed transition systems (extended abstract). In: *CONCUR'92, Stony Brook*. – LNCS 630, Springer Verlag.

[AD90] Alur (R.) et Dill (D.). – Automata for modeling real-time systems. In: *Proceedings of ICALP 90*, éd. par Paterson (M.S.). pp. 322–335. – Springer Verlag.

[AG95] André (Charles) et Gaffé (Daniel). – *Sequential Function Charts: a Synchronous Point of View*. – Rapport technique n° RR 95-08, Sophia-Antipolis, France, I3S, février 1995.

[And96] André (C.). – Representation and analysis of reactive behaviors: A synchronous approach. In: *Computational Engineering in Systems Applications (CESA)*. pp. 19–29. – Lille (F), juillet 1996.

[Arn92] Arnold (A.). – *Systèmes de transitions finis et sémantique des processus communaute*. – Masson, 1992.

[BCM90] Berthet (C.), Coudert (O.) et Madre (J. C.). – New ideas on symbolic manipulations of finite state machines. In: *International Conference on Computer Design (ICCD), Cambridge*.

[Ber91] Berry (G.). – A hardware implementation of pure ESTEREL. In: *ACM Workshop on Formal Methods in VLSI Design, Miami*.

[Ber93] Berry (G.). – Preemption in concurrent systems. In: *Proceedings of FSTTCS 93*. – Springer Verlag, LNCS 761.

[BG92] Berry (G.) et Gonthier (G.). – The Esterel synchronous programming language: Design, semantics, implementation. *Science Of Computer Programming*, vol. 19, n° 2, 1992, pp. 87–152.

[CCI89] CCITT. – *Specification and Description Language*. – Rapport technique n° Tome X, ITU, 1989.
[CGP94] Caspi (P.), Girault (A.) et Pilaud (D.). – Distributing reactive systems. *In: Seventh International Conference on Parallel and Distributed Computing Systems, PDCS'94*. – Las Vegas, USA, octobre 1994.

[CGS91] Courcoubetis (C.), Graf (S.) et Sifakis (J.). – An algebra of boolean processes. *In: Workshop on Computer-Aided Verification*. – Aalborg, juillet 1991.

[CHPP87] Caspi (P.), Halbwachs (N.), Pilaud (D.) et Plaice (J.). – LUSTRE, a declarative language for programming synchronous systems. *In: 14th Symposium on Principles of Programming Languages*. – Munich, janvier 1987.

[CS95] C2A-SYNCHRON. – *The common format of synchronous languages – The declarative code DC version 1.0*. – Technical report, SYNCHRON project, octobre 1995.

[CTC90] Costagliola (G.), Tomita (M.) et Chang (S.). – Dr parsers: a generalization of lr parsers. *In: IEEE Workshop on Visual Languages*. pp. 174–180. – Skokie (Illinois), octobre 1990.

[CTC91] Costagliola (G.), Tomita (M.) et Chang (S.). – A generalized parser for 2-d languages. *In: IEEE Workshop on Visual Languages*. pp. 98–104. – Kobe (Japan), octobre 1991.

[CV89] Collette (P.) et Villar (B.). – *Intégration de formalismes déclaratifs et impératifs pour la spécification des systèmes réactifs*. – Thèse, Universié de Louvain-La-Neuve, 1989.

[DY90] Drusinsky-Yoresh (D.). – A simple single-block implementation and efficient state-assignments for statecharts. *In: Synthesis and Simulation Meeting and International Interchange (SASIMI)*. – Kyoto, 1990.

[GBBG85] Guernic (P. Le), Benveniste (A.), Bournai (P.) et Gauthier (T.). – *Signal: A Data Flow Oriented Language for Signal Processing*. – Rapport technique, IRISA report 246, IRISA, Rennes, France, 1985.

[GC92] Girault (A.) et Caspi (P.). – An algorithm for distributing a finite transition system on a shared/distributed memory system. *In: PARLE'92, Paris*.

[Hal] Halbwachs (N.). – ...

[Hal93] Halbwachs (N.). – Delay analysis in synchronous programs. *In: Fifth Conference on Computer-Aided Verification*. – Elounda (Greece), juillet 1993.

[Har87] Harel (D.). – Statecharts : A visual approach to complex systems. *Science of Computer Programming*, vol. 8, 1987, pp. 231–275.

[HGdR88] Huizing (C.), Gerth (R.) et de Roever (W.P.). – Modelling statecharts behaviour in a fully abstract way. *In: 13th CAAP*. – LNCS 299, Springer Verlag.

[HLR93] Halbwachs (N.), Lagnier (F.) et Raymond (P.). – Synchronous observers and the verification of reactive systems. *In: Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93*, éd. par Nivat (M.), Rattray (C.), Rus (T.) et Scollo (G.). – Twente, juin 1993.
[HM95] Halbwachs (N.) et Maraninchi (F.). – On the symbolic analysis of combinational loops in circuits and synchronous programs. *In: EUROMICRO*. – Como, Italy, septembre 1995.

[HMP95] Halbwachs (N.), Maraninchi (F.) et Proy (Y. E.). – The railroad crossing problem, modeling with hybrid argos - analysis with polka. *In: Second European Workshop on Real-Time and Hybrid Systems*. – Grenoble (France), juin 1995.

[HNSY92] Henzinger (T.), Nicollin (X.), Sifakis (J.) et Yovine (S.). – Symbolic model-checking for real-time systems. *In: LICS'92*.

[HP88] Harel (D.) et Pnueli (A.). – On the development of reactive systems. *In: Logic and Models of Concurrent Systems, NATO Advanced Study Institute on Logics and Models for Verification and Specification of Concurrent Systems*. – NATO ASI series F, Springer Verlag.

[IEE91] Another look at real-time programming. *Special Section of the Proceedings of the IEEE*, vol. 79, n° 9, septembre 1991.

[JLMR93] Jourdan (M.), Lagnier (F.), Maraninchi (F.) et Raymond (P.). – Embedding declarative subprograms into imperative constructs. *In: Fifth International Symposium on Programming Language Implementation and Logic Programming*, Tallin, Estonia.
– Springer Verlag, LNCS 714.

[JLMR94] Jourdan (M.), Lagnier (F.), Maraninchi (F.) et Raymond (P.). – A multiparadigm language for reactive systems. *In: 5th IEEE International Conference on Computer Languages*. – Toulouse, mai 1994.

[JM94a] Jourdan (M.) et Maraninchi (F.). – A modular state/transition approach for programming real-time systems. *In: ACM Sigplan Workshop on Language, compiler and tool support for real-time systems*. – Orlando, FL, juin 1994.

[JM94b] Jourdan (M.) et Maraninchi (F.). – Studying synchronous communication mechanisms by abstractions. *In: IFIP Working Conference on Programming Concepts, Methods and Calculi*. – San Miniato, Italy, juin 1994.

[JM95] Jourdan (M.) et Maraninchi (F.). – Static timing analysis of real-time systems. *In: ACM Sigplan Workshop on Language, compiler and tool support for real-time systems*.
– La Jolla, California, novembre 1995.

[JMO93] Jourdan (M.), Maraninchi (F.) et Olivero (A.). – Verifying quantitative real-time properties of synchronous programs. *In: International Conference on Computer-Aided Verification*. – Elounda, juin 1993.

[Jou91] Jourdan (M.). – *Etude des techniques de compilation applicables à un langage de description des systèmes réactifs*. – Dea, Grenoble, Université Joseph Fourier, Grenoble, juin 1991.

[Jou94] Jourdan (M.). – *Un environnement multi-langages et multi-outils pour la programmation et la vérification des systèmes réactifs*. – Thesis, Grenoble, Université Joseph Fourier, Grenoble, septembre 1994.
[Jou96] Jourdan (M.). – Integrating formal verification methods of quantitative real-time properties into a development environment for robot controllers. In: *AMAST Workshop on Real-time Systems*.

[LT89] Lynch (N. A.) et Tuttle (M. R.). – *An Introduction to Input/Output Automata*. – CWI-Quaterly n° 3, 1989.

[Mal93] Malik (S.). – Analysis of cyclic combinational circuits. In: *ICCAD’93*. – Santa Clara (Ca), 1993.

[Mar90] Maraninchi (F.). – *Argos: un langage graphique pour la conception, la description et la validation des systèmes réactifs*. – Thesis, Grenoble, Université Joseph Fourier, Grenoble, janvier 1990.

[Mar91] Maraninchi (F.). – The argos language: Graphical representation of automata and description of reactive systems. In: *IEEE Workshop on Visual Languages*. – Kobe, Japan, octobre 1991.

[Mar92] Maraninchi (F.). – Operational and compositional semantics of synchronous automaton compositions. In: *CONCUR*. – LNCS 630, Springer Verlag.

[MH96a] Maraninchi (F.) et Halbwachs (N.). – Compiling argos into boolean equations. In: *Formal Techniques for Real-Time and Fault Tolerance (FTRTFT)*. – Uppsala (Sweden), septembre 1996.

[MH96b] Maraninchi (F.) et Halbwachs (N.). – Compositional semantics of non-deterministic synchronous languages. In: *European Symposium On Programming*. – Linkoping (Sweden), avril 1996.

[Mil80] Milner (R.). – A calculus of communication systems. In: *LNCS 92*. – Springer Verlag, 1980.

[Mil89] Milner (R.). – Communication and concurrency. In: *International Series in Computer Science*. – Prentice Hall, 1989.

[MV92a] Maraninchi (F.) et Vachon (M.). – *Argos Programming Examples: The Multi-Function, Six Digit LCD Watch Circuit With Alarm, Three Stopwatch Modes and Event Counter*. – Tr, LGI/IMAG, mars 1992.

[MV92b] Maraninchi (F.) et Vachon (M.). – An experience in compiling a mixed imperative/declarative language for reactive systems. In: *International Workshop on Compiler Construction (poster session)*. – Springer Verlag, LNCS 641.

[PPST93] Pandey (Rajeev K.), Pesch (Wolfgang), Shur (Jim) et Takikawa (Masami). – *A Revised Leda Language Definition*. – Rapport technique n° 93-60-02, Department of Computer Science, Oregon State University, 1993. Fri, 15 Dec 1993 03:16:57 GMT.

[PS88] Pnueli (A.) et Shalev (M.). – *What is in a Step*. – Rapport technique, Dept. of Applied Mathematics and Computer Science, The Weizmann Institute of Science, Israel, mai 1988.
[QV94] Quint (V.) et Vatton (I.). – Making structured documents active. *Electronic Publishing – Origination, Dissemination and Design*, vol. 7, n° 2, juin 1994, pp. 55-74.

[Rau92] Rauzy (A.). – *Toupie: Technical Report*. – Rapport technique, LaBRI-CNRS-Université Bordeaux I, juillet 1992.

[Ray96] Raymond (P.). – Recognizing regular expressions by means of dataflows networks. In: *23rd International Colloquium on Automata, Languages, and Programming, (ICALP’96) Paderborn, Germany*. – Springer Verlag.

[RdS90] Roy (V.) et de Simone (R.). – Auto and Autograph. In: *International Workshop on Computer Aided Verification*, éd. par Kurshan (R.). – Rutgers (N.J.), juin 1990.

[RM95] Rutten (E.) et Martinez (F.). – SIGNALGTI, implementing task preemption and time interval in the synchronous data-flow language SIGNAL. In: *7th Euromicro Workshop on Real Time Systems*. – Odense (Denmark), juin 1995.

[Roc92] Rocheteau (F.). – *Extension du langage Lustre et application à la conception de circuits: Le langage Lustre-V4 et le système Pollux*. – Thèse, Institut National Polytechnique de Grenoble, juin 1992.

[Roy90] Roy (V.). – *Autograph, Un outil de visualisation pour les calculs de processus*. – Thèse, France, Université de Nice, 1990.

[RS89] Roy (V.) et Simone (R. de). – *An AUTOGRAPH Primer*. – Rapport de recherche, Sophia-Antipolis, INRIA, mai 1989.

[Sch94] Schaar (P.). – *Un environnement de programmation pour le langage graphique Argos*. – Rapport technique, Conservatoire National des Arts et Métiers, mars 1994.

[SECK93] Simon (D.), Espiau (B.), Castillo (E.) et Kapellos (K.). – Computer-aided design of a generic robot controller handling reactivity and... *IEEE Transactions on Control Systems Technology*, vol. 1, 1993.

[SFLM93] Scholl (P.-C.), Fauvet (M.-C.), Lagnier (F.) et Maraninchi (F.). – *Cours d’information: langages et programmation*. – Masson, 1993.

[Shu91] Shur (Jim). – *Implementing Leda: Objects and Classes*. – Rapport technique n° 91-60-11, Department of Computer Science, Oregon State University, 1991. Fri, 15 Dec 1995 03:15:02 GMT.

[SKEJ95] Simon (D.), Kapellos (K.), Espiau (B.) et Jourdan (M.). – Formal verification of robotic missions and tasks. In: *European Workshop on Hybrid Systems*. – Grenoble, juin 1995.

[Smo94a] Smolka (Gert). – *A Calculus for Higher-Order Concurrent Constraint Programming with Deep Guards*. – Research Report n° RR-94-03, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany, Deutsches Forschungszentrum für Künstliche Intelligenz, février 1994.

[Smo94b] Smolka (Gert). – A foundation for higher-order concurrent constraint programming. In: *1st International Conference on Constraints in Computational Logics*, éd. par Jouannaud (Jean-Pierre). pp. 50-72. – München, Germany, 7-9 septembre 1994.
[Sto88] Stoughton (Allen). – *Fully Abstract Models of Programming Languages*. – Pitman, 1988, *Research Notes in Theoretical Computer Science*.

[SY96] Sifakis (J.) et Yovine (S.). – Compositional specification of timed systems. *In: 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS'96*. Lecture Notes in Computer Science 1046, pp. 347–359. – Grenoble, France, février 1996.

[US94] Uselton (A.C.) et Smolka (S.A.). – A process algebraic semantics for statecharts via state refinement. *In: IFIP Working Conference on Programming Concepts, Methods and Calculi*. – San Miniato, Italy, jun 1994.

[vdB94] von der Beeck (M.). – A comparison of statecharts variants. *In: FTRTFT*. – LNCS 863, Springer Verlag.

[VNG91] Vahid (F.), Narayan (S.) et Gajski (D.D.). – Speccharts: A language for system level synthesis. *In: Computer Hardware Description Languages*.

[ZJ93] Zave (Pamela) et Jackson (Michael). – Conjunction as composition. *acm Transactions of Software Engineering and Methodology*, vol. 2, n° 4, octobre 1993, pp. 379–411.
Sixième partie

Dossier
<figure><img src="image_74.png" /></figure>
# Chapitre 17

# Curriculum Vitae

## 17.1 Informations personnelles

Nom: Maraninchi Florence

Date et lieu de naissance: 9 octobre 1964 à Vif (Isère)

Nationalité: Française

Situation de famille: célibataire

Adresse personnelle: 8, rue Pierre Loti, 38000 Grenoble

Téléphone: Bureau: 04 76 63 48 53

### Fonctions :

- De novembre 1987 à octobre 1989, Allocataire de Recherche (MRT).

- D'octobre 1989 à octobre 1990, Allocataire d'Enseignement et de Recherche à l'Institut National Polytechnique de Grenoble (Ensimag).

- Depuis octobre 1990, Maître de Conférences à l'Université Joseph Fourier, Grenoble I (ticularisation le 01/10/1991).

### Etudes et titres universitaires :

- Juin 1982: Baccalauréat Série C à Grenoble, mention Très Bien

- Juin 1984: DEUG A (Sciences des Structures et de la Matière), Université Joseph Fourier (Grenoble I), mention Bien

- Juin 1985: Licence d'Informatique, Université Joseph Fourier, mention Très Bien

- Juin 1986: Maîtrise d'Informatique, Université Joseph Fourier, mention Bien

- Juin 1987: DEA d'Informatique, "Statecharts : sémantique et application à la spécification de systèmes", Institut National Polytechnique, Grenoble. Responsable: M. Jacques Voiron. Mention Très Bien.

- Janvier 1990: Thèse d'Informatique, "Argos: un langage graphique pour la conception, la description et la validation des systèmes réactifs", soutenue à Grenoble le 12 Janvier 1990, Université Joseph Fourier (Grenoble I). Mention Très Honorable.
Membres du jury :

M. Sacha Krakowiak, Professeur, Université J. Fourier, Grenoble (président).

M. Jacques Voiron, Professeur, Université J. Fourier, Grenoble (directeur)

M. Gérard Berry, Maître de Recherches, Ecole des Mines de Paris (rapporteur)

M. Michel Sintzoff, Professeur, Université Catholique de Louvain (rapporteur)

M. Joseph Sifakis, Directeur de Recherche CNRS, Grenoble.

# 17.2 Activités d'enseignement

## 17.2.1 Cadre

Après une année d'enseignement à l'ENSIMAG (algorithmique en première année et projet de compilation en deuxième année), mes activités d'enseignement se sont déroulées au sein de l'UFR IMA (Informatique et Mathématiques Appliquées) de l'Université Joseph Fourier, dans plusieurs contextes :

- dans la section MPI (Mathématiques, Physique, Informatique) de la deuxième année de DEUG A de 1990 à 1996, puis dans la filière MIAS (Mathématiques, Informatique et Applications aux Sciences) du DEUG rénové.

- en première année de l'Ecole Universitaire d'Informatique, modules L&P (Langages et Programmation) et ALM (Architectures Logicielles et Matérielles)

- en DESS Informatique Double Compétence, module Base de Données.

J'ai d'autre part participé à une action de formation permanente pour le personnel de la société Schneider Electric (anciennement Merlin-Gérin), mise en place par l'Université Joseph Fourier et l'Université Pierre Mendès-France, pour les années 93/94 et 94/95.

Les étudiants de la section MPI du DEUG suivaient 6h d'enseignement d'Informatique par semaine, pendant toute l'année, réparties en : 2h de cours, 2h de TD sur papier, 2h de TD sur machine, dits TD d'"expérimentation". Le contenu de [SFLM93](https://www.cldp.org/) constituait le support des enseignements. Il en est de même actuellement pour les modules proposés dans le cadre de la réforme des premiers cycles, pour le DEUG mention MIAS.

Les enseignements en première année de l'Ecole sont divisés en trois blocs principaux: *Langages et Programmation*, *Architectures Logicielles et Matérielles* et *Outils Formels pour l'Informatique*. Les deux premiers blocs sont organisés en Cours, Travaux Dirigés et Travaux Dirigés dits "d'application". Les années 90/91 et 91/92 ont été des années de transition dans l'UFR, puisque l'ensemble des filières informatiques de second cycle (maîtrise classique, MST Experts en Systèmes Informatiques et MIAGE) ont été réorganisées pour former l'Ecole Universitaire d'Informatique. J'ai participé aux réflexions préliminaires dès le printemps 1990, et j'ai démarré mes enseignements au sein de l'Ecole dès la rentrée 90. Dans le cadre des Travaux Dirigés d'application du bloc Langages et Programmation, l'équipe d'enseignants a dû, lors de cette année d'installation de l'Ecole, définir un ensemble de "scénarios" d'expérimentation, sorte de TP couvrant sur 4 ou 5 semaines. J'ai ensuite participé aux enseignements du module ALM, en assurant une partie du cours (système à l'exécution, assemblage et édition de liens, systèmes de gestion de fichiers et de processus), en assurant les travaux dirigés de programmation en assembleur Sparc, et en définissant le projet de programmation d'un assembleur/éditeur de liens pour Sparc. Plus récemment j'ai participé aux travaux dirigés de description de circuits.
Le DESS IDC (Informatique Double Compétence) accueille des étudiants titulaires d'une maîtrise scientifique ou de diplômes plus élevés (DEA, plus rarement thèses), de domaines aussi différents que la biologie ou les mathématiques pures. L'hétérogénéité du public, ainsi que leur exigence d'une formation informatique suffisamment large, pose des problèmes de définition du contenu et de choix du niveau de discours. La forte motivation des étudiants et la diversité de leurs cultures scientifiques font de cette formation un cadre de travail très intéressant.

### 17.2.2 Rédaction de documents

Le travail en DEUG a donné lieu à un polycopié, puis à l'ouvrage [SFLM93]. Avec mes collègues du module ALM de première année de l'Ecole d'Informatique, nous avons commencé la rédaction d'un ouvrage intitulé 'Architectures Logicielles et Matérielles', qui devrait être prêt fin 98.

La définition de travaux pratiques et de projets de programmation donne lieu, par ailleurs, à la rédaction de documents.

### 17.2.3 Définition de travaux pratiques et projets de programmation

Dans le cadre du DEUG les travaux pratiques sont souvent organisés autour de programmes dont les étudiants complètent certains modules. Cela demande une préparation conséquente, et une écriture extrêmement rigoureuse des portions de programme effectivement lisibles par les étudiants.

L'essentiel de ma contribution (réalisée une première fois en Pascal sous environnement unix, et cette année en C/Unix) concerne :

- Une bibliothèque de fonctions (y compris l'affichage de cartes sur un écran graphique) pour programmer des réussites

- Un programme d'analyse lexicale et syntaxique d'un langage d'expressions qui décrit des motifs graphiques, complété par la construction du motif et l'affichage graphique

- Un programme de simulation d'automate

Dans le cadre de la première année de l'Ecole d'Informatique, l'essentiel de mon travail est la définition d'un projet de programmation en C d'un assembleur/éditeur de liens pour Sparc. Le programmme est entièrement réalisé et une version à compléter est utilisée par environ 120 étudiants chaque année depuis 4 ans. Le programme est écrit en utilisant l'outil noweb de programmation instruite ('literate programming'). La documentation complète comprend des chapitres de cours sur l'assemblage/édition de liens, et le programme à compléter, abondamment commenté. La version encore utilisée cette année produit des fichiers objet au format sun os. La disparition probable, dans un avenir proche, de la dernière machine fonctionnant encore sous ce système m'a incitée cette année à effectuer le portage à Solaris, ce qui a demandé une refonte assez conséquente du module de génération des fichiers objets.

## 17.3 Charges collectives

* Membre élu de la commission de spécialité des 5ème, 6ème et 27ème sections de l'UJF, depuis 1992.
• Responsable de la conception et du développement du serveur W3 de l'UFR Informatique et Mathématiques Appliquées (IMA) de l'UJF.

## 17.4 Activités de recherche

Les activités de recherche étant décrites en détail dans le présent document, nous ne parlons ici que du cadre de travail.

### 17.4.1 l'unité mixte VERIMAG

Mes activités de recherche se déroulent au sein de l'Unité Mixte de Recherche du CNRS n° C9939 VERIMAG qui regroupe le projet SPECTRE (Spécification et Programmation des Systèmes Communicants et Temps Réel) animé par Joseph Sifakis et la société VERILOG. Spectre est un projet IMAG et INRIA Rhône-Alpes.

L'objectif du projet est d'aider le concepteur de certains types d'applications parallèles et temps-réel pour lesquelles le développement d'une méthode de conception rigoureuse, appuyée par des outils automatiques, semble à la fois nécessaire et réaliste à l'heure actuelle. Les axes de recherche principaux sont : la programmation, la spécification et la validation de ces systèmes dits *critiques*.

### 17.4.2 Collaborations et relations nationales et internationales

- Les travaux de recherche autour des langages synchrones et de la vérification des systèmes ont conduit à des collaborations avec des équipes du même domaine (équipe d'André Arnold à Bordeaux, de Gérard Berry à Sophia-Antipolis, d'Albert Benveniste à Rennes) ou de domaines dans lesquels notre approche est utilisable (projet INRIA BIP dirigé par Bernard Espiau à Grenoble, équipe de Brigitte Plateau, avant-projet INRIA SHOOD dirigé par Toan Nguyen).

- Le projet SYNCHRONIE de la GMD (Allemagne) animé par A. Poigné, est consacré au développement d'un environnement de programmation synchrone multi-langages. Leur choix s'est porté sur Esterel, Lustre et Argos. La collaboration porte sur les aspects multi-langages, déjà étudiés dans la thèse de Muriel Jourdan.

- J'assiste très régulièrement depuis 1990 aux réunions du groupe C2A (Collaboration CAO Automatique) animé par Albert Benveniste, qui réunit des laboratoires publics français dans lesquels sont développés des langages synchrones (VERIMAG à Grenoble, IRISA à Rennes, INRIA à Sophia-Antipolis...) et des industriels intéressés par les aspects synchrones. Une des activités de ce groupe de travail a consisté à définir les formats de la "plateforme synchrone", en vue de la normalisation. Ce groupe a également donné naissance au projet européen Eureka SYNCHRON auquel je participe. Les partenaires sont : l'INRIA et les sociétés Vérilog, TNI et Schneider Electric (Merlin-Gérin) en France ; Saab Military Aircrafts et Logikkonsult en Suède.

- Je participe depuis octobre 1989 aux "Basic Research Actions" ESPRIT dans lesquelles le projet Spectre est engagé, d'abord SPEC, puis REACT. Parmi les partenaires on trouve les Universités de Liège, Kiel, Eindhoven, Oxford, Tampere (Finlande) et Uppsala (Suède) et le Weizmann Institute à Rehovot, Israël. Cela a donné lieu à de nombreux exposés (avril
et septembre 1990, septembre 1991, juin 1993, février et juillet 1994), dont 3 à l'occasion des revues de projets.

- Dans le cadre de la coopération Franco-Israélienne, j'ai effectué en mai 1991 un séjour d'une dizaine de jours au Weizmann Institute, Rehovot, Israël, sur l'invitation d'Amir Pnueli. La coopération portait sur des aspects de définition de la sémantique des langages synchrones impératifs. Une comparaison d'Argos avec diverses sémantiques des Statecharts a été développée à cette occasion.

- En novembre 1994 et décembre 1996 à Dagstuhl (Allemagne) et en novembre 1995 à Marseille, j'ai participé aux séminaires consacrés aux langages synchrones, sur l'invitation des organisateurs. Y participaient une quarantaine de personnes, représentant la majorité des équipes travaillant sur le sujet.

- En octobre 1995, j'ai participé à une réunion du groupe de travail WG2.1 de l'IFIP, à Ulm, en tant qu'observateur invité.

### 17.4.3 Encadrement d'étudiants

**Année Universitaire 1990-1991** : Encadrement du **DEA** de Muriel Jourdan sur le sujet : étude des techniques de compilation applicables à un langage de description des systèmes réactifs, le cas d'Argos. La première partie du travail concerne la traduction d'Argos vers une des formes intermédiaires de la chaîne de compilation Esterel. Muriel Jourdan effectuait en parallèle avec son DEA un **magistère** d'Informatique à l'Université Joseph Fourier, formation pour laquelle j'étais également tuteur.

**D'octobre 1991 à octobre 1994** : Encadrement de la **thèse** de Muriel Jourdan sur le sujet : un environnement de programmation multi-langages et multi-outils pour les systèmes réactifs. La soutenance a eu lieu le 29 septembre 1994. Les rapporteurs étaient MM Michel Sintzoff, Professeur à l'Université Catholique de Louvain, et Gérard Berry, Maître de Recherches à l'Ecole des Mines de Paris. Muriel Jourdan a ensuite effectué un stage post-doctoral dans l'équipe de Bernard Espiau (projet BIP, INRIA Rhône-Alpes) où elle a étudié les possibilités d'utilisation de nos outils pour l'analyse des systèmes de contrôle/commande en robotique. Elle est maintenant chargée de recherche à l'INRIA, dans le projet Opéra de V. Quint.

**Année 1993** : Encadrement du mémoire du cycle C du **CNAM** de Philippe Schaar, sur le sujet : *Un environnement de programmation pour le langage graphique Argos*. L'idée était de réaliser un prototype d'éditeur syntaxique pour ARGOS basé sur l'utilisation de l'éditeur de documents structurés GRIF, développé au sein du projet OPERA de l'INRIA à Grenoble. Le prototype permet l'édition de programmes ARGOS sous forme graphique ou textuelle et la connexion au compilateur.

**Année 1994/1995** : Tutorat de **Magistère** de Pascal Laffont, sur le sujet : *une étude de cas programmée en Argos et Lustre*.

**De mars 96 à juin 96** : Encadrement du mémoire de DEA de l'Université de Iasi (Roumanie) de Traian Popovici, sur le thème : *Intégration de langages synchrones impératifs et déclaratifs : étude d'un processeur DC*.

**Année 1996/1997** : Tutorat de **Magistère** de Yann Remond, sur le sujet : *Programmation multi-langages - Etude d'un mécanisme d'édition de liens de programmes DC*.
### 17.4.4 Cours, séminaires et jurys de thèses

#### Cours

- Dans le cadre du Programme Affilié de l'Institut IMAG — programme de formation des industriels, auquel sont également conviés les chercheurs du laboratoire —, j'ai donné un cours assorti de démonstration du logiciel Argonaute, sur la programmation des systèmes réactifs dans les langages synchrones et en Argos en particulier (1989 et 1990).

- En mai 1993, j'ai organisé à Grenoble un cours de deux jours sur les langages synchrones et les méthodes et outils de vérification développés dans le laboratoire, à l'intention d'ingénieurs de la société Parallax Software Technologies.

- En mai 1993 également, j'ai participé, avec Paul Caspi et Xavier Nicollin, à un cours d'une journée sur l'approche synchrone, le langage Argos et les méthodes de vérification de propriétés temporelles, au CEA à Saclay.

- En mars 1995 j'ai été invitée par Lionel Marcé à Brest pour présenter le langage Argos et l'environnement de programmation-vérification Argonaute aux étudiants du DESS Informatique et Automatique de l'Université de Bretagne Occidentale. Cette présentation de 6h était divisée en Cours et TD.

#### Séminaires divers

- Le groupe C2A fournit l'occasion de présenter des résultats de recherche devant un public d'industriels et de chercheurs, éventuellement de culture différente, comme les automatisciens.

- J'ai participé en décembre 1993 à une réunion du groupe de travail Afcet sur la "sécurité des systèmes informatiques".

- Les invitations d'autres équipes sont généralement l'occasion de séminaires. J'ai ainsi présenté deux articles de conférence à l'équipe d'André Arnold (Bordeaux) en juin 94. Fabienne Lagnier et moi avons présenté l'approche synchrone, les langages Argos et Lustre et les aspects de vérification lors d'un séminaire de l'unité mixte Bull Imag en février 94.

#### Jurys de thèses, revues d'articles

J'ai participé en décembre 92 au jury de la thèse préparée par Guido Gherardi à l'Université de Nice sous la direction de Gérard Berry, en tant que co-rapporteur. En octobre 1994, j'ai été examinateur dans le jury de thèse de Frédéric Mignard (Ecole des Mines de Paris), également encadré par Gérard Berry.

Je participe régulièrement au travail de revue d'articles pour des conférences ou des revues d'audience internationale, dont AMAST (Algebraic Methods and Software Technologies), PROCOMET (Programming Concepts, Methods and Calculi), CONCUR (), ESOP (European Symposium on Programming), ECC (European Control Conference), FTRTFT (Formal Techniques for Real-Time and Fault-Tolerant Systems), IEEE TSE (Transactions on Software Engineering), SCP (Science of Computer Programming), ...
### 17.4.5 Développement de logiciels

Le développement de logiciels autour d'Argos et de l'environnement associé Argonaute a commencé en 1988. Le premier environnement argonaute était composé de :

- l'environnement d'édition réalisé en Xwindows version 10 par 4 étudiants de DESS Génie Informatique de Grenoble que j'encadrais en 1987-88.

- le debugger symbolique associé, que je développai par la suite en complétant l'éditeur.

- la première version du compilateur, développée en C dans le cadre de ma thèse, après une tentative de prototypage en Lisp.

Muriel Jourdan, en thèse de 91 à 94, a réalisé quelques améliorations, puis la connexion à une bibliothèque de bdd, pour tous les aspects de calcul booléen dans les programmes. Elle a implanté la traduction en format IC (un format intermédiaire de la chaîne de compilation Esterel) et une technique d'élimination du raffinement. Elle a pris en charge la connexion à Kronos, et le petit prototype de traduction Argos vers Lustre.

J'ai travaillé pour ma part aux connexions du compilateur aux outils Bac (analyse de causalité sur la forme équationnelle) et Polka (analyse de systèmes hybrides) de Nicolas Halbwachs.

Plus récemment, j'ai démarré une refonte complète du compilateur et de ses connexions aux divers outils de vérification, en passant par le format DC. J'ai donc entrepris la programmation en C++ et noweb du compilateur à partir d'une syntaxe qui autorise la structuration des programmes en "processus", analogues aux noeuds Lustre.

L'ambition de ce projet est de réaliser un environnement de programmation autour d'un petit langage permettant de composer des automates, décorés d'informations diverses selon les besoins. Cet environnement utilisera DC comme format intermédiaire, pour permettre l'édition de liens avec des programmes Lustre ou Esterel.

## 17.5 Publications

[HM95] N. Halbwachs et F. Maraninchi. On the symbolic analysis of combinational loops in circuits and synchronous programs. Dans *EUROMICRO*, Como, Italy, septembre 1995.

[HMP95] N. Halbwachs, F. Maraninchi et Y. E. Proy. The railroad crossing problem, modeling with hybrid argos - analysis with polka. Dans *Second European Workshop on Real-Time and Hybrid Systems*, Grenoble (France), juin 1995.

[JLMR93] M. Jourdan, F. Lagnier, F. Maraninchi et P. Raymond. Embedding declarative sub-programs into imperative constructs. Dans *Fifth International Symposium on Programming Language Implementation and Logic Programming*, Tallin, Estonia. Springer Verlag, LNCS 714, août 1993.

[JLMR94] M. Jourdan, F. Lagnier, F. Maraninchi et P. Raymond. A multiparadigm language for reactive systems. Dans *In 5th IEEE International Conference on Computer Languages*, Toulouse, mai 1994. IEEE Computer Society Press.

[JM94a] M. Jourdan et F. Maraninchi. A modular state/transition approach for programming real-time systems. Dans *ACM Sigplan Workshop on Language*,
compiler and tool support for real-time systems, Orlando, FL, juin 1994.
http://www.cs.umd.edu/~pugh/sigplan_realtime_workshop_94/.

[JM94b] M. Jourdan et F. Maraninchi. Studying synchronous communication mechanisms by abstractions. Dans *IFIP Working Conference on Programming Concepts, Methods and Calculi*, San Miniato, Italy, juin 1994. Elsevier Science Publishers.

[JM95] M. Jourdan et F. Maraninchi. Static timing analysis of real-time systems. Dans *ACM Sigplan Workshop on Language, compiler and tool support for real-time systems*, La Jolla, California, novembre 1995. ACM Sigplan Notices.

[JM96] M. Jourdan et F. Maraninchi. Vérification de systèmes réactifs en argos temporisé. Dans *Congrès AFCET: Modélisation des systèmes réactifs*, Brest (France), mars 1996.

[JMO93] M. Jourdan, F. Maraninchi et A. Olivero. Verifying quantitative real-time properties of synchronous programs. Dans *International Conference on Computer-Aided Verification*, Elounda, juin 1993. LNCS 697.

[Mar87] F. Maraninchi. Statecharts, sémantique et application à la spécification de systèmes. DEA, LGI/IMAG, Grenoble, Grenoble, juin 1987.

[Mar89] F. Maraninchi. Argonaute, graphical description, semantics and verification of reactive systems by using a process algebra. Dans *Workshop on Automatic Verification Methods for Finite State Systems*, Grenoble, juin 1989. LNCS 407, Springer Verlag.

[Mar90] F. Maraninchi. Argos : un langage graphique pour la conception, la description et la validation des systèmes réactifs. Thesis, Université Joseph Fourier, Grenoble, Grenoble, janvier 1990.

[Mar91] F. Maraninchi. The argos language: Graphical representation of automata and description of reactive systems. Dans *IEEE Workshop on Visual Languages*, Kobe, Japan, octobre 1991.

[Mar92] F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. Dans *CONCUR*. LNCS 630, Springer Verlag, août 1992.

[MH96a] F. Maraninchi et N. Halbwachs. Compiling argos into boolean equations. Dans *Formal Techniques for Real-Time and Fault Tolerance (FTRTFT)*, Uppsala (Sweden), septembre 1996. Springer verlag, LNCS 1135.

[MH96b] F. Maraninchi et N. Halbwachs. Compositional semantics of non-deterministic synchronous languages. Dans *European Symposium On Programming*, Linkoping (Sweden), avril 1996. Springer verlag, LNCS 1058.

[MSFL93] F. Maraninchi, P.-C. Scholl, M.-C. Fauvet et F. Lagnier. Rôle de l'expression fonctionnelle dans l'enseignement de l'informatique en deug a. Dans *2èmes journées de travail: les langages applicatifs dans l'enseignement de l'informatique*, Rennes, apr 1993. SPECIF.

[MV92a] F. Maraninchi et M. Vachon. Argos programming examples: The multi-function, six digit LCD watch circuit with alarm, three stopwatch modes and event counter. TR, LGI/IMAG, mars 1992.
[MV92b] F. Maraninchi et M. Vachon. An experience in compiling a mixed imperative/declarative language for reactive systems. Dans *International Workshop on Compiler Construction (poster session)*. Springer Verlag, LNCS 641, octobre 1992.

[SFLM93] P.-C. Scholl, M.-C. Fauvet, F. Lagnier et F. Maraninchi, *Cours d'informatique: langages et programmation*. Masson, 1993.

## 17.6 Documents pédagogiques

P.-C. Scholl, M.-C. Fauvet, F. Lagnier et F. Maraninchi, *Cours d'informatique: Langages et Programmation*, Ouvrage édité par Masson, 1993 (420 pages). Préface de Michel Sintzoff.

J.-P. Peyrin, C. Berrut et F. Maraninchi, *Langages et Programmation, rappels de cours et exercices*, polycopié pour la première année de l'Ecole Universitaire d'Informatique, 150 pages, tiré à 150 exemplaires.

C. Berrut et F. Maraninchi, *Introduction à Lisp*, polycopié, support de cours-TD pour la première année de l'EUI, 100 pages

C. Collet et F. Maraninchi, *Mini interprète Lisp*, Documentation enseignants du scénario de programmation d'un mini-interprète Lisp, support de TD pour la première année de l'EUI

P.-C. Scholl, M.-C. Fauvet, F. Lagnier et F. Maraninchi, *Informatique, exemples et exercices*, polycopié, support de cours-TD pour l'option MPI (Mathématiques, Physique et Informatique) du DEUG A 2ème année.

P.-C. Scholl, M.-C. Fauvet, F. Lagnier et F. Maraninchi, *Algorithmique, exemples et exercices*, polycopié, support de cours-TD pour le DESS Informatique Double Compétence.

F. Maraninchi, *Projet Assembleur/Editeur de liens pour Sparc, définition et documentation*, 50p. Ce document comprend une description complète du langage d'assemblage à traiter (lexicographie, syntaxe et sémantique) ainsi que les algorithmes principaux des phases d'analyse, génération de code et édition de liens. Une annexe décrit la structure du logiciel à compléter fourni aux étudiants.
# Chapitre 18

## Publications jointes

On trouvera ci-joint, et dans cet ordre :

<table><tr><td>[Mar92]</td><td>Première version de la sémantique, réécrite au chapitre 2</td></tr><tr><td>[JM94b]</td><td>Source du chapitre 3</td></tr><tr><td>[MH96]</td><td>Source du chapitre 4</td></tr><tr><td>[HM95]</td><td>Complétant la section 5.2 du chapitre 5</td></tr><tr><td>[JLMR94]</td><td>Complétant le chapitre 7</td></tr><tr><td>[JM94a]</td><td>Un exemple de programme ARGOS.</td></tr><tr><td>[JMO93]</td><td>Complétant le chapitre 10.</td></tr></table>

## Rappel des références

[Mar92] Maraninchi (F.). – Operational and compositional semantics of synchronous automaton compositions. In: CONCUR. – LNCS 630, Springer Verlag.

[JM94b] Jourdan (M.) et Maraninchi (F.). – Studying synchronous communication mechanisms by abstractions. In: IFIP Working Conference on Programming Concepts, Methods and Calculi. – San Miniato, Italy, juin 1994.

[MH96] Maraninchi (F.) et Halbwachs (N.). – Compositional semantics of non-deterministic synchronous languages. In: European Symposium On Programming. – Linkoping (Sweden), avril 1996.

[HM95] Halbwachs (N.) et Maraninchi (F.). – On the symbolic analysis of combinational loops in circuits and synchronous programs. In: EUROMICRO. – Como, Italy, septembre 1995.

[JLMR94] Jourdan (M.), Lagnier (F.), Maraninchi (F.) et Raymond (P.). – A multiparadigm language for reactive systems. In: In 5th IEEE International Conference on Computer Languages. – Toulouse, mai 1994.

[JM94a] Jourdan (M.) et Maraninchi (F.). – A modular state/transition approach for programming real-time systems. In: ACM Sigplan Workshop on Language, compiler and tool support for real-time systems. – Orlando, FL, juin 1994.
[JMO93] Jourdan (M.), Maraninchi (F.) et Olivero (A.). — Verifying quantitative real-time properties of synchronous programs. In: *International Conference on Computer-Aided Verification*. — Elounda, juin 1993.