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

Florence Maraninchi

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

## To cite this version:

Florence Maraninchi. Modélisation et validation des systèmes réactifs : un langage synchrone à base d'automates. Systèmes embarqués. Grenoble 1 UJF - Université Joseph Fourier, 1997. tel-03840029

HAL Id: tel-03840029

https://hal.science/tel-03840029

Submitted on 7 Nov 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
Document d'Habilitation à Diriger des Recherches

Université Joseph Fourier - Grenoble I

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

Florence Maraninchi

Soutenance le 22 mai 1997

devant un jury composé de :

<table><tr><td>Michel Adiba</td><td>président</td></tr><tr><td>André Arnold</td><td>rapporteur</td></tr><tr><td>Gérard Berry</td><td>rapporteur</td></tr><tr><td>Guy Vidal-Naquet</td><td>rapporteur</td></tr><tr><td>Nicolas Halbwachs</td><td>examinateur</td></tr><tr><td>Pierre-Claude Scholl</td><td>examinateur</td></tr></table>
Remerciements

Je remercie tout d'abord Michel Adiba pour avoir accepté la présidence du jury; André Arnold, Gérard Berry et Guy Vidal-Naquet pour avoir accepté de juger mon travail, et pour leurs suggestions de nouvelles pistes; Nicolas Halbwachs et Pierre-Claude Scholl pour leur participation au jury, et les nombreuses discussions qui ont contribué à la forme et au fond de ce document.

Ensuite j'aimerais profiter de cette page pour citer, plus généralement, toutes les personnes avec
qui j'ai travaillé et qui m'ont appris mon métier.

En commençant par le contexte d'enseignement, je tiens à remercier vivement les collègues qui
m'ont accueillie en 1990 et ont supporté ma naïveté avec une indulgence et une bonne humeur
que le recul me fait apprécier davantage encore. A l'Ensimag, il s'agit de Roger Mohr, Jacques
Mossière, Jean-Louis Roch et Yann Rouzaud ; à l'UFR IMA, il s'agit des équipes L&P (Philippe
Bizard, Jean-Pierre Peyrin et Catherine Berrut) et MPI (Pierre-Claude Scholl, Marie-Christine
Fauvet et Fabienne Lagnier).

Pour la période plus récente, merci de nouveau à l'équipe MPI, pour tout ce que m'ont appris
les séances de rédaction de l'ouvrage [SFLM93], et pour l'ambiance de travail en DEUG toujours
aussi agréable.

Merci aussi à mes collègues de l'équipe ALM actuelle (Paul Amblard, Jean-Claude Fernandez, Fabienne Lagnier, Pascal Sicard et Philippe Waille), avec qui l'on peut discuter de portes NAND, de compilation, des mystères du fork et de bien d'autres sujets, selon l'humeur du jour. Les séances de rédaction du futur ouvrage "Architectures Logicielles et Matérielles" m'ont déjà beaucoup appris, et ce n'est sans doute pas fini !

Côté recherche, merci à Joseph Sifakis pour m'avoir accueillie dans son équipe dès mon DEA en
87, en me proposant le sujet qui a orienté tout mon travail ultérieur. Sous sa direction VÉRIMAG
est un environnement de travail incomparable, plein de bonne humeur et foisonnant.

Nicolas Halbwachs et Gérard Berry m'ont expliqué pourquoi mon travail avait quelque chose à
voir avec le domaine de la programmation synchrone, et sont donc responsables de l'apparition
d'ARGOS dans la communauté synchrone. Merci à eux et à tous mes collègues du sous-ensemble
synchrone de Vérimag, qui savent supporter le rythme de travail irrégulier des enseignants.

Merci aussi à tous les étudiants avec lesquels j'ai travaillé et qui m'ont aidée : Ch. Bard, G. Bodoin, D. Franck, J.-P. Schmidt, T. Popovici, P. Laffont et Y. Rémond. Ph. Schaar et M. Jourdan ont beaucoup fait avancer la définition d'Argos et l'étude de l'environnement de programmation associé.
# Avant-propos

Il n'y a pas, à ma connaissance, de règle communément admise sur ce qui peut constituer un document d'habilitation à diriger des recherches. Il est bon, toutefois, de s'interroger sur la finalité d'un tel document, outre la satisfaction personnelle de rassembler et d'organiser des idées jusque là encore un peu dispersées.

Il m'a semblé qu'un exposé purement technique n'était pas de nature à mettre en valeur l'aptitude à organiser, orienter des recherches, sans même parler de les diriger. Il apparaissait donc qu'il fallût plutôt présenter une démarche, un ensemble structuré de motivations, montrer comment les problèmes étaient apparus, comment s'effectuent les choix et comment les travaux sont articulés. Vaste programme...

La difficulté de l'exercice réside dans le fait qu'il est impossible de présenter une démarche indépendamment du sujet technique sur lequel elle s'est exercée, lorsque cette démarche s'est forgée de pair avec le sujet. Le présent document revêt donc un certain caractère autobiographique dans l'exposé de l'approche suivie et de ses évolutions, en particulier lorsqu'il s'agit de reconnaître les influences extérieures qui ont orienté mon travail. Cela me paraît toutefois relever de la plus élémentaire honnêteté intellectuelle et mériter, à ce titre, de figurer ici.

Ce document n'a pas d'ambition de présentation synthétique d'un domaine de recherche, ce qui serait présompteux. Ce n'est pas non plus un document très technique présentant un ensemble de résultats fondamentaux. J'aimerais plutôt y démontrer une certaine cohérence des directions suivies, et comment les résultats convergent. Ce n'est au fond qu'une mise en forme des réflexions que m'inspirent dix années de travail qui, certes, ont conduit à la définition et à l'implantation d'un langage, mais qui, surtout, constituent mon apprentissage du métier d'enseignant/chercheur.

L'essentiel des travaux décrits, toutefois, concernent la définition et l'implantation d'un langage de programmation synchrone baptisé ARGOS, pour la modélisation et la validation des systèmes dits "réactifs", et ce document devrait pouvoir constituer, au moins pendant un certain temps, le document de référence sur ARGOS.

Les travaux décrits ici ont été réalisés en parallèle, ou plutôt en étroite relation, avec une activité d'enseignement à plein temps, sur un poste de Maître de Conférences. Il me paraît peu souhaitable, et de toute façon difficile, de tracer une frontière nette entre les activités de recherche et d'enseignement.

La diffusion des résultats ou de la culture d'une équipe de recherche par des interventions dans des formations de troisième cycle — particulièrement en DEA — est naturelle, répandue, et offre en général peu de surprises. Il est en revanche moins courant de pouvoir utiliser cette culture pour enrichir des enseignements de premier ou second cycle, et ceci à court terme. La section MPI (mathématiques, physique et informatique) du DEUG scientifique de Grenoble, et l'équipe d'enseignants qui m'y a accueillie dès 1990, m'ont offert un champ d'expérimentation passionnant. J'intègre à ce document la description de deux activités d'enseignement pour lesquelles le lien
avec des activités de recherche est évident. Je mentionne, lorsque cela est le cas, les convergences entre des modèles développés dans les deux environnements de travail, à des fins différentes, mais en partant de la même idée.

Inversement, l'influence des activités d'enseignement sur les activités de recherche ne se limite pas, comme on pourrait le croire, à un manque de disponibilité. Elle prend plusieurs formes. Enseigner les bases de données et le logiciel de base tout en travaillant sur la programmation des systèmes réactifs, peut paraître curieux, mais permet des rapprochements de points de vue qui sinon sembleraient audacieux. On ne connaît jamais si bien les algorithmes sur les graphes et leurs complexités respectives qu'après les avoir décortiqués en compagnie de 30 étudiants. Quant aux réflexions sur le rôle central des langages dans l'apprentissage de l'informatique, menées dans le cadre d'un enseignement de base en premier cycle, elles ne peuvent que profiter à la conception d'un nouveau langage, fût-il dédié aux systèmes réactifs.

D'autre part la nécessaire diversité des sujets abordés en sept années de plein service d'enseignement à des publics variés permet une approche globale d'un sujet de recherche, de la formulation théorique aux problèmes d'implantation.

Enfin, et c'est peut-être le plus important, l'ensemble des collègues que l'on côtoie régulièrement dans un contexte d'enseignement représente une grande diversité de cultures — scientifiques ou non — et, l'enseignant étant souvent bavard, les occasions d'en profiter sont nombreuses. Dans un environnement de recherche, la nécessaire concentration des efforts laisse peu de place aux manifestations de pure curiosité pour des sujets qui ne relèvent pas directement d'un projet.

J'ajouterai que la fragmentation du temps consacré aux activités de recherche, si elle constitue le handicap principal des enseignants dans une équipe de recherche, peut aussi avoir des effets bénéfiques, en obligeant à des prises de recul plus fréquentes, et en détruisant dans l'oeuf toute velléité de ré-inventer la roue.
# Table des matières

<table><tr><td>Remerciements</td><td>3</td></tr><tr><td>Avant-propos</td><td>5</td></tr><tr><td>1 Introduction</td><td>11</td></tr><tr><td>1.1 Systèmes réactifs</td><td>11</td></tr><tr><td>1.2 Modèles pour les systèmes réactifs</td><td>13</td></tr><tr><td>1.3 Les langages synchrones</td><td>14</td></tr><tr><td>1.4 Le langage ARGOS et son environnement de programmation</td><td>15</td></tr><tr><td>1.5 Organisation du document</td><td>20</td></tr><tr><td>1.6 Sources</td><td>21</td></tr><tr><td>I Définition d'Argos</td><td>23</td></tr><tr><td>2 Les constructions d'Argos</td><td>25</td></tr><tr><td>2.1 Exemple commenté</td><td>26</td></tr><tr><td>2.2 Machines de Mealy booléennes et opérations</td><td>26</td></tr><tr><td>2.3 Un langage d'expressions et sa sémantique</td><td>35</td></tr><tr><td>2.4 A propos d'expressivité</td><td>36</td></tr><tr><td>2.5 A propos de compositionnalité</td><td>38</td></tr><tr><td>3 Modèles généraux pour les langages synchrones</td><td>41</td></tr><tr><td>3.1 Motivations</td><td>41</td></tr><tr><td>3.2 Cadre général</td><td>42</td></tr><tr><td>3.3 Applications</td><td>44</td></tr><tr><td>3.4 Commentaires et réflexions</td><td>46</td></tr><tr><td>4 Non déterminisme et langages synchrones</td><td>49</td></tr><tr><td>4.1 Motivations</td><td>50</td></tr><tr><td>4.2 Formalisation de la technique des oracles</td><td>54</td></tr><tr><td>4.3 Recherche d'une autre relation d'équivalence</td><td>55</td></tr><tr><td>4.4 Application à d'autres langages synchrones...</td><td>58</td></tr><tr><td>5 Sémantique d'Argos en équations booléennes</td><td>61</td></tr><tr><td>5.1 Argos vers DC</td><td>62</td></tr><tr><td>5.2 Analyse de déterminisme et réactivité sur la forme équationnelle</td><td>67</td></tr></table>
<table><tr><td><b>6</b></td><td><b>Eléments de définition du langage Argos</b></td><td><b>73</b></td></tr><tr><td>6.1</td><td>Structuration des programmes et restriction de l'environnement</td><td>73</td></tr><tr><td>6.2</td><td>Aspects de syntaxe concrète</td><td>74</td></tr><tr><td>6.3</td><td>Un mécanisme général de pragmas</td><td>76</td></tr><tr><td>6.4</td><td>Extensions</td><td>78</td></tr><tr><td>6.5</td><td>Une proposition de syntaxe textuelle</td><td>78</td></tr><tr><td>6.6</td><td>Exemple de programme</td><td>81</td></tr></table>

## II Programmation multi-langages synchrone 83

<table><tr><td><b>7</b></td><td><b>La programmation multi-langages : motivations et première étude dans le cadre synchrone</b></td><td><b>85</b></td></tr><tr><td>7.1</td><td>Motivations et travaux sur le sujet</td><td>85</td></tr><tr><td>7.2</td><td>Programmation multi-langages dans le cadre synchrone</td><td>86</td></tr><tr><td>7.3</td><td>Conclusions</td><td>90</td></tr></table>

<table><tr><td><b>8</b></td><td><b>Argos + Lustre via DC</b></td><td><b>91</b></td></tr><tr><td>8.1</td><td>Structure des programmes et exemple</td><td>91</td></tr><tr><td>8.2</td><td>Schéma de principe</td><td>93</td></tr><tr><td>8.3</td><td>Outil de débouclage des noeuds DC issus d'ARGOS</td><td>94</td></tr><tr><td>8.4</td><td>Réinitialisation des noeuds DC issus de LUSTRE</td><td>94</td></tr><tr><td>8.5</td><td>Un mécanisme d'édition de liens au niveau DC</td><td>95</td></tr><tr><td>8.6</td><td>Travaux de même nature</td><td>95</td></tr><tr><td>8.7</td><td>Pour aller plus loin...</td><td>95</td></tr></table>

<table><tr><td><b>9</b></td><td><b>Argos + Esterel</b></td><td><b>97</b></td></tr><tr><td>9.1</td><td>Motivations</td><td>97</td></tr><tr><td>9.2</td><td>Proposition: ARGOS+ESTEREL</td><td>98</td></tr><tr><td>9.3</td><td>Schémas de traduction structurelle en ESTEREL</td><td>106</td></tr><tr><td>9.4</td><td>Preuve de conformité</td><td>110</td></tr><tr><td>9.5</td><td>Travaux de même nature</td><td>110</td></tr><tr><td>9.6</td><td>Comparaison des notions de causalité en ARGOS et ESTEREL</td><td>110</td></tr></table>

## III Extensions temporelle et hybride 115

<table><tr><td><b>10</b></td><td><b>Argos temporisé</b></td><td><b>117</b></td></tr><tr><td>10.1</td><td>Motivations</td><td>117</td></tr><tr><td>10.2</td><td>ARGOS temporisé et sa traduction en automates temporisés</td><td>119</td></tr><tr><td>10.3</td><td>Implantation et exemples d'utilisation</td><td>122</td></tr><tr><td>10.4</td><td>Généralisation</td><td>124</td></tr></table>

<table><tr><td><b>11</b></td><td><b>Argos hybride, un point d'entrée de l'outil POLKA</b></td><td><b>127</b></td></tr><tr><td>11.1</td><td>Motivations</td><td>127</td></tr><tr><td>11.2</td><td>Les systèmes hybrides et le modèle considéré</td><td>128</td></tr><tr><td>11.3</td><td>Connexion ARGOS+POLKA: le prototype HARGOS</td><td>128</td></tr><tr><td>11.4</td><td>Exemple d'utilisation de HARGOS: le passage à niveau</td><td>128</td></tr></table>
<table><tbody><tr><td>11.5</td><td>Pour aller plus loin...</td><td>133</td></tr><tr><td>IV</td><td>Environnement de programmation</td><td>135</td></tr><tr><td>12</td><td>Edition graphique et débogage symbolique d'ARGOS</td><td>137</td></tr><tr><td>12.1</td><td>Présentation du problème</td><td>137</td></tr><tr><td>12.2</td><td>Première tentative: Andromède</td><td>139</td></tr><tr><td>12.3</td><td>Le prototype Aglae: éditeur ARGOS en Grif</td><td>139</td></tr><tr><td>12.4</td><td>Travaux de même nature.</td><td>140</td></tr><tr><td>13</td><td>Compilation et connexion aux outils</td><td>143</td></tr><tr><td>13.1</td><td>Schéma général du compilateur, formats et étapes</td><td>143</td></tr><tr><td>V</td><td>Recherche et enseignement</td><td>147</td></tr><tr><td>14</td><td>Automates et programmation par événements en DEUG</td><td>149</td></tr><tr><td>14.1</td><td>Motivations</td><td>149</td></tr><tr><td>14.2</td><td>Etude des algorithmes itératifs</td><td>149</td></tr><tr><td>14.3</td><td>Un schéma général d'itération</td><td>151</td></tr><tr><td>14.4</td><td>Automate d'états finis pour la représentation des algorithmes</td><td>153</td></tr><tr><td>14.5</td><td>Proposition</td><td>156</td></tr><tr><td>14.6</td><td>Conclusion provisoire.</td><td>158</td></tr><tr><td>15</td><td>Description de circuits en Lustre et VHDL, niveau Licence</td><td>159</td></tr><tr><td>15.1</td><td>Le contexte</td><td>159</td></tr><tr><td>15.2</td><td>Traduction Lustre vers VHDL.</td><td>160</td></tr><tr><td>15.3</td><td>Argos et VHDL.</td><td>160</td></tr><tr><td>16</td><td>Quelques remarques en guise de conclusion</td><td>163</td></tr><tr><td>VI</td><td>Dossier</td><td>175</td></tr><tr><td>17</td><td>Curriculum Vitae</td><td>177</td></tr><tr><td>17.1</td><td>Informations personnelles</td><td>177</td></tr><tr><td>17.2</td><td>Activités d'enseignement.</td><td>178</td></tr><tr><td>17.3</td><td>Charges collectives</td><td>179</td></tr><tr><td>17.4</td><td>Activités de recherche</td><td>180</td></tr><tr><td>17.5</td><td>Publications</td><td>183</td></tr><tr><td>17.6</td><td>Documents pédagogiques.</td><td>185</td></tr><tr><td>18</td><td>Publications jointes</td><td>187</td></tr></tbody></table>
# Chapitre 1

# Introduction

## 1.1 Systèmes réactifs

La typologie désormais consacrée proposée par A. Pnueli [HP88] distingue parmi la grande variété des systèmes informatiques les systèmes réactifs et les systèmes transformationnels.

Les derniers sont les systèmes classiques de traitement de données, comme les compileurs. Ils mettent en oeuvre des structures de données et des algorithmes complexes, mais posent en général peu de problèmes d'interaction avec un monde extérieur.

Au contraire, les systèmes réactifs sont caractérisés par la prépondérance des aspects d'interaction avec un environnement, que ce soit un utilisateur humain ou un processus physique. Ces aspects d'interaction sont d'autant plus difficiles à décrire que ces systèmes sont souvent intrinsèquement parallèles. G. Berry a introduit une distinction supplémentaire entre systèmes interactifs, pour lesquels le rythme de l'interaction est fixé par le système, et systèmes réactifs, pour lesquels le rythme de l'interaction est fixé par l'environnement. Les systèmes réactifs doivent donc satisfaire des propriétés temporelles imposées par l'environnement, portant par exemple sur le temps de réponse aux stimuli extérieurs. C'est la raison pour laquelle on classe les interfaces homme/machine ou les systèmes d'exploitation parmi les systèmes "seulement" interactifs, et les contrôleurs de processus industriels parmi les systèmes réactifs.

La programmation des systèmes réactifs constitue un domaine de recherche en soi. D'une part, les langages séquentiels classiques sont mal adaptés à la description d'une interaction complexe avec un environnement ; d'autre part ces systèmes sont souvent critiques, au sens où leur défaillance peut entraîner de graves conséquences matérielles ou humaines. Un environnement de programmation des systèmes réactifs doit donc proposer des outils et des méthodes de validation formelle. En se restreignant à l'étude des systèmes réactifs, il est possible de développer des langages et des approches de vérification dédiés, en profitant par exemple du fait que certaines abstractions raisonnables des systèmes considérés peuvent être décrites par des objets finis, sur lesquels toute propriété imaginable devient décidable.

## Description du noyau réactif d'un système

Pour mettre en évidence les aspects d'interaction propres aux systèmes interactifs ou réactifs, on peut considérer que l'exécution d'un système suit toujours le schéma :
Initialisations

tantque vrai

Acquérir des entrées *e*

Calculer des sorties *s*

Emettre les sorties *s*

La boucle est exécutée un grand nombre de fois, peut-être même indéfiniment : puisque l'on cherche à décrire les aspects d'interaction avec l'environnement, le système a un comportement intéressant même si son exécution ne se termine pas. (Note : on pourrait se ramener à ce schéma pour les systèmes transformationnels. Tout se passe comme si la boucle était exécutée une seule fois, l'expression 'calcul des sorties' représentant tout le travail, éventuellement complexe, de transformation des données en résultats). Cette exécution en boucle est à la base du fonctionnement des automates programmables.

On appelle *noyau réactif* du système le programme chargé de l'étape de calcul des sorties. L'exécution du système est partitionnée en *cycles*. Si l'on imagine une échelle de temps logique discret correspondant aux cycles d'exécution, on peut définir la suite des entrées et la suite des sorties indicées par des entiers naturels<fnref n="1" />.

Si le calcul des sorties ne dépend que de l'entrée courante — $s_n = f(e_n)$ —, on obtient un modèle d'exécution assimilable aux circuits combinatoires. En général, toutefois, la sortie au cycle *n* dépend de l'histoire des entrées : un noyau réactif est un programme qui implante une fonction de la forme : $s_n = f(e_0, e_1, ..., e_n)$. La nième sortie dépend de l'histoire des entrées, jusqu'au rang *n* inclus. Si le système fonctionne indéfiniment, l'histoire des entrées n'est pas bornée.

## Systèmes à mémoire bornée

Dans le domaine des systèmes réactifs, on ne s'intéresse qu'à un sous-ensemble de ces systèmes, dits à mémoire bornée, pour lesquels une abstraction bornée de l'histoire des entrées suffit à calculer la sortie courante<fnref n="2" />. De manière générale, un noyau réactif fait donc intervenir une variable "mémoire" pour stocker l'abstraction de l'histoire courante des entrées, et suit un algorithme de la forme :

Initialisation de la mémoire *M*

tantque vrai

Acquérir des entrées *e*

$s = f(M, e)$ calcul de la sortie courante

$M = g(M, e)$ mise à jour de la mémoire

Emettre les sorties *s*

où *M* représente la mémoire des entrées.

### Exemple 1.1 : Un système réactif à mémoire booléenne

Imaginons un système qui lit un flot d'entrée composé de caractères *a* et *b* uniquement, et qui émet un caractère *c* sur son flot de sortie, chaque fois qu'il lit un *b*, à condition qu'il ait lu

<footnote n="1">1. Certaines implémentations de systèmes réactifs sont telles que le noyau réactif ainsi défini est activé sur interruptions, plutôt qu'exécuté périodiquement. La différence entre les deux approches a peu d'influence sur la suite, l'échelle de temps logique n'étant pas nécessairement régulière en temps physique.</footnote>

<footnote n="2">2. La mémoire de tout système informatique est bornée, à l'exécution, pour des raisons physiques; mais la taille mémoire nécessaire à l'exécution peut ne pas être prévisible. Or un programme réactif ne peut se permettre les arrêts intempestifs pour cause d'échec de l'allocation mémoire. La mémoire doit donc être bornée statiquement.</footnote>
un nombre pair de $a$ auparavant. Ce système fonctionne avec une mémoire booléenne. En effet, l'abstraction nécessaire et suffisante de l'histoire des entrées est le nombre d'entrées $a$ rencontrées, modulo 2. On a :

$$f(M, e) = \text{si } M \wedge e \ni b \text{ alors } c \text{ sinon } \emptyset$$

$$g(M, e) = \text{si } e \ni a \text{ alors } \neg M \text{ sinon } M$$

(On note $e \ni b$ lorsque le caractère $b$ apparaît dans l'entrée $e$). Les valeurs de la mémoire $M$ alternent avec les occurrences de $a$. Le caractère $c$ est émis lorsque $b$ apparaît, à la condition que la mémoire $M$ soit vraie. C'est un choix arbitraire, si l'on ne dit pas comment initialiser la mémoire $M$. Pour assurer un comportement conforme à la spécification, on doit initialiser $M$ à vrai. $\square$

Une grande partie du travail décrit dans ce document est basée sur les équivalences entre diverses formes de description des noyaux réactifs : a) algorithmes itératifs définis ci-dessus ; b) fonctions à mémoire bornée des séquences d'entrées vers les séquences de sorties ; c) ensembles d'équations de flots ; d) machines de Mealy ; e) circuits booléens séquentiels. Ainsi la programmation multi-langages ARGOS+LUSTRE (chapitre 8) s'appuie-t-elle sur l'équivalence des modèles b) et d) ; la proposition de description des algorithmes itératifs en ARGOS (chapitre 14) sur l'équivalence entre a) et d) ; la compilation symbolique d'ARGOS (chapitre 5) sur l'équivalence entre c) et d) ; la description des circuits en LUSTRE et VHDL sur l'équivalence entre c) et e), etc.

L'autre partie du travail présenté ici porte sur les aspects de définition d'un *langage*, mentionnés plus loin.

## 1.2 Modèles pour les systèmes réactifs

Tenter d'établir une liste exhaustive des langages et formalismes proposés pour la description, la vérification ou la programmation des systèmes réactifs relève de l'utopie. Nous ne nous intéressons qu'à un sous-ensemble, déjà vaste, de ce domaine, qui comprend les méthodes et outils basés sur la définition d'un modèle des systèmes étudiés.

Les modèles sont des structures mathématiques qui peuvent être plus ou moins riches selon les systèmes étudiés, ou selon le niveau de détail désiré dans la description. Ils peuvent également avoir des représentations informatiques différentes selon les outils (génération de code, vérification...) qu'on leur applique. Définir un modèle approprié à la modélisation des systèmes que l'on étudie permet de raisonner formellement sur ces systèmes, par exemple pour réaliser des vérifications.

Donnons tout de suite un exemple. Les systèmes à mémoire bornée peuvent être représentés par des machines à états finies, chaque état correspondant à une valeur possible de la mémoire. Les transitions représentent les changement d'états, c'est-à-dire la mise à jour de la mémoire et les sorties produites, en fonction des entrées lues. Les machines de Mealy (dont les transitions portent des couples entrée/sortie) constituent un modèle naturel des systèmes réactifs. Selon la nature des étiquettes de transitions (atomes, formules booléennes, formules arithmétiques, ...) on obtient des modèles plus ou moins riches.

Les traitements applicables et les questions auxquelles on sait répondre dépendent de la nature des informations associées aux états et transitions. Par exemple, si les transitions portent des formules booléennes, tout problème d'accessibilité à partir d'un état initial donné est décidable. Si les transitions portent des conditions quelconques sur des variables de types quelconques (typiquement des réels), un grand nombre de propriétés deviennent indécidables. Dans les chapitres
qui suivent on rencontrera :

- les systèmes de transitions à étiquettes abstraites (format d'entrée de l'outil ALDÉBARAN, chapitre 13)

- les machines de Mealy booléennes (définition d'ARGOS, chapitre 2), dans lesquelles les étiquettes sont enrichies d'une structure entrée/sortie, la condition d'entrée étant une formule booléenne quelconque.

- les automates interprétés généraux (compilation en C, chapitre 13) dont les transitions portent des conditions sur, et des affectations à, des variables de types quelconques, de telle sorte que le modèle a la puissance d'expression des machines de Turing, et aussi peu de propriétés de décidabilité que lesdites machines.

- les automates temporisés (ou “Timed Graphs” [AD90]) utilisés au chapitre 10, dont les transitions portent des conditions sur, et des affectations à, des variables réelles. Les conditions sont des comparaisons à des bornes entières et les affectations sont des remises à zéro. Cette restriction assure la décidabilité des formules de TCTL, une extension de la logique temporelle CTL dans laquelle les modalités sont restreintes par des bornes exprimées de manière quantitative.

- les automates hybrides (chapitre 11), plus expressifs que les automates temporisés, dont les états et les transitions sont étiquetés par des systèmes d'inéquations linéaires, et qu'on ne sait analyser que par des techniques approchées.

De nombreux autres modèles sont étudiés, pour leurs propriétés de décidabilité et d'expressivité. On trouve en particulier toute une hiérarchie de modèles entre les automates temporisés et les automates hybrides.

D'un point de vue informatique, on peut représenter ces machines en extension, en donnant explicitement l'ensemble des états et des transitions, ou symboliquement, par des systèmes d'équations.

## 1.3 Les langages synchrones

Les modèles (par exemple les machines de Mealy) sont rarement utilisables pour décrire directement les systèmes étudiés. Ils ne peuvent que constituer une représentation intermédiaire entre un véritable langage, et les outils de génération de code ou de vérification. Un langage de description des systèmes doit posséder une sémantique formelle qui décrit comment les programmes peuvent être compilés en modèles. Il est courant d'exiger de cette sémantique quelques bonnes propriétés comme la compositionnalité.

Parmi les nombreux formalismes et langages proposés pour décrire des systèmes réactifs, l'approche synchrone est sans doute celle qui fait les hypothèses les plus simples. Les langages synchrones les plus connus sont ESTEREL [BG92], LUSTRE [CHPP87] et SIGNAL [GBBG85], tous trois développés en France. Les Statecharts [Har87] sont parfois rangés parmi les langages synchrones, bien que leur sémantique ne relève pas tout à fait de l'application stricte de l'hypothèse de synchronisme. On trouve également de nombreux formalismes ou langages qui relèvent des hypothèses de la famille synchrone, et pourrait donc y être rangés, bien que leurs auteurs n'utilisent pas le même vocabulaire. C'est le cas en particulier pour le GRAFCET. Les équipes de Ch. André à Nice et de L. Marcé à Brest ont travaillé sur la sémantique synchrone du Grafcet, par
exemple par traduction en ESTEREL. Il est intéressant de noter que ces langages existent, parfois depuis longtemps, non seulement dans le monde universitaire, mais aussi dans l'industrie. C'est d'ailleurs cet heureux "hasard" qui assure le succès du transfert de LUSTRE.

Les langages synchrones proposent des constructions qui permettent de décrire un système comme la composition (par exemple parallèle) de plusieurs sous-systèmes communiquant par diffusion synchrone. L'hypothèse de synchronisme se résume à : *le temps de réaction d'un système est nul*, autrement dit les sorties sont considérées comme simultanées aux entrées qui les provoquent. Les arguments sur les avantages de l'approche synchrone, dont la réfutation de la critique usuelle selon laquelle le modèle est complètement irréaliste, sont développés dans [IEE91], et je ne m'y attarderai pas. Notons simplement que l'hypothèse de synchronisme a deux facettes.

Si l'on considère la relation entre deux sous-systèmes d'un même programme, l'hypothèse de réaction en temps nul simplifie considérablement la sémantique de la composition, et permet de définir simplement les opérations du langage — les langages synchrones étant dédiés à l'élabo-ration de programmes séquentiels, destinés à une exécution centralisée. La composition parallèle n'est donc qu'une facilité de description, elle est *compilée*, et n'a rien à voir avec un parallélisme d'exécution. Paul Caspi et Alain Girault ont étudié le problème de répartition des programmes synchrones [GC92, CGP94].

Si l'on considère la relation entre le système global et l'environnement dans lequel il s'exécute, l'hypothèse permet de s'abstraire, pendant la conception du programme, des paramètres de temps d'exécution liés à la machine. Sur le modèle d'exécution proposé plus haut, la relation entre temps logique du système et temps physique, qui doit être étudiée pour prendre en compte les contraintes de temps des systèmes réactifs, est simple. La phase de calcul des sorties doit être de complexité raisonnable, puisque c'est sur elle que portent les contraintes de temps : si le rythme de production des entrées par l'environnement est de une toutes les millisecondes, le programme doit pouvoir faire un tour dans la boucle en moins d'une milliseconde, pour ne pas risquer d'ignorer des entrées.

ESTEREL et LUSTRE sont compilables en automates interprétés généraux, et des analyses de propriétés sont réalisables depuis longtemps sur l'abstraction de ces objets qui ne conserve que la structure de contrôle, c'est-à-dire l'automate. Plus récemment, des techniques d'analyse approchées ont été proposées pour tenir compte des variables contrôlées par l'automate [Hal93, HMP95, Hal]. L'automate interprété est d'autre part utilisé pour la génération de code C, par exemple. Ce schéma justifie l'expression WYPIWYE (What You Prove Is What You Execute) de Gérard Berry, puisque le même modèle est utilisé comme support de la vérification et comme étape intermédiaire de la génération de code. Il suffit de se convaincre que l'algorithme de codage de l'automate est suffisamment simple pour qu'on soit sûr de son implantation.

L'hypothèse de synchronisme est la base sémantique commune de langages aux styles très différents (impératif pour ESTEREL, avec des structures de contrôle temporelles comme le chien de garde, déclaratif flot de données pour LUSTRE, ...). L'essentiel de ce document porte sur l'étude et l'implantation d'un langage de la famille synchrone, dont le style est inspiré des constructions d'automates des Statecharts.

# 1.4 Le langage ARGOS et son environnement de programmation

## 1.4.1 Description

ARGOS est un langage synchrone à syntaxe potentiellement graphique, qui permet la description de systèmes réactifs sous forme de compositions de machines de Mealy. Le jeu d'opé-
rateurs est en quelque sorte minimal: mise en parallèle, synchronisation par le mécanisme de
diffusion synchrone commun à tous les langages synchrones, composition hiérarchique héritée
des Statecharts. La composition parallèle de machines à états — que l'on trouve déjà dans
SDL [CCI89] par exemple — et la composition hiérarchique, rendent réaliste la description de
systèmes de taille conséquente par des systèmes d'états et de transitions explicites.

Dès le départ, le langage et l'environnement de programmation correspondant Argonaute ont été définis avec le parti pris de permettre la connexion au maximum d'outils traitant des systèmes de transitions, en particulier les outils de vérification développés à Vérimag ou dans d'autres équipes avec lesquelles nous entretenons des collaborations étroites. L'environnement Argonaute est actuellement connecté, entre autres, à: Aldébaran (calcul de relations d'équivalence sur des systèmes de transitions étiquetées, Vérimag); Kronos (évaluation de formules de logique temporelle temps-réel, Vérimag); Mec (évaluation de formules du μ-calcul, LaBri, Bordeaux); Autograph (placeur interactif de systèmes de transitions, INRIA Sophia-Antipolis); Bac (analyse de systèmes d'équations booléennes, Vérimag); Polka (analyse approchée des automates hybrides, Vérimag); Toupie (résolution de contraintes sur des entiers bornés — entre autres —, LaBri, Bordeaux).

Beaucoup plus récent que les autres langages synchrones, qui sont utilisés dans l'industrie, Argos ne dispose pas d'un environnement de programmation directement transférable. Cela est dû, en grande partie, à la nécessité de fournir un éditeur syntaxique graphique, pour l'utilisation en vraie grandeur et par des non spécialistes. En revanche sa simplicité de structure et la facilité de connexion de l'environnement Argonaute aux prototypes universitaires implantant les méthodes de vérification les plus récentes, en font un outil de travail précieux, et un bon moyen de démontrer les apports de l'approche synchrone dans des domaines où elle est encore peu utilisée.

1.4.2 Historique des travaux

Première étude des Statecharts

Les travaux autour d'ARGOS ont débuté comme une tentative de définir une algèbre de pro-
cessus inspirée des Statecharts, compatible avec la technologie de vérification développée dans le
projet Spectre, et intégrable dans les environnements de programmation et validation alors en
cours de réalisation. Cette première étude fait l'objet de mon mémoire de DEA, soutenu en 1987.
L'objet d'étude ne s'appelle pas encore ARGOS, ce n'est alors pas encore un langage synchrone, ni
même à proprement parler un langage. A l'époque, la communauté de recherche internationale
n'a pas encore donné aux Statecharts les 22 sémantiques qu'ont leur connaît maintenant [vdB94].
La conséquence première de cette année de travail est la constatation d'une impossibilité: les
Statecharts, tels qu'ils sont décrits alors dans un rapport publié ensuite dans [Har87], forment
un ensemble trop riche pour être formalisé simplement; d'autre part, certaines des construc-
tions offertes rendent le comportement des programmes ambigu ou imprévisible. La possibilité
de structuration hiérarchique des descriptions à base d'automates semble pourtant mériter encore
un peu d'attention.

Définition d'un langage de la famille synchrone

La première définition du langage synchrone ARGOS, et le premier environnement de program-
mation associé ARGONAUTE, remontent à ma thèse, en janvier 1990. L'éditeur graphique est dû
à quatre étudiants du DESS Génie Informatique de Grenoble. Il est réalisé en X10, qui devient
rapidement obsolète. A partir de 1988, et grâce à l'influence conjuguée de G. Berry et N. Halbwachs, la poursuite du travail autour d'un langage à base d'automates intégrant la structure hiérarchique des Statecharts se rapproche inexorablement du monde des langages synchrones. La définition d'ARGOS publiée dans ma thèse montre toutefois quelques réminiscences des algèbres de processus, dont le mode de communication par rendez-vous et l'indéterminisme intrinsèque des descriptions, qui se marient mal avec les aspects synchrones de la composition parallèle.

Le travail se poursuit ensuite en collaboration étroite avec Muriel Jourdan, qui effectue sous ma direction un stage de magistère, un DEA et une thèse, couvrant ainsi la période juin 1990 — septembre 1994.

## La programmation multi-langages

Dès le début de la thèse de Muriel Jourdan en 1991, les travaux "de fond" autour d'ARGOS et des sémantiques synchrones — définition de nouvelles constructions, généralisation du langage, étude d'exemples, implantation, élaboration d'un cadre sémantique commun permettant de comparer différents modes de synchronisation — sont conduits en parallèle avec une nouvelle direction de recherche : la programmation synchrone "multi-styles" ou multi-langages.

L'idée provient d'une constatation simple : les divers styles de programmation offerts par les langages synchrones existants — impératif textuel, flot de données, automates — correspondent à des cultures différentes dans l'industrie. D'autre part les styles *flot de données* et *automates*, par exemple, se révèlent également insuffisants lorsqu'ils sont utilisés seuls. Deux possibilités sont alors envisageables : définir un nouveau langage inspiré des langages existants, en associant des constructions de styles différents — c'est la programmation "multi-styles" ; ou profiter de l'existence des langages et de leurs environnements de programmation associés, en particulier les compilateurs, pour construire un environnement dans lequel des portions de programme de différents langages peuvent cohabiter — c'est la programmation "multi-langages".

Le souci de ne pas ré-inventer la roue et la disponibilité réduite d'un enseignant pour les développements logiciels conséquents nous ont dès le début conduits à choisir la deuxième possibilité, avec une contrainte forte : proposer l'intégration au niveau source des différents langages, tout en utilisant les compilateurs d'origine. Les chercheurs de l'équipe d'Axel Poigné à la GMD (...) semblent suivre depuis 2 ans une voie intermédiaire : ils proposent d'intégrer ARGOS, LUSTRE et ESTEREL dans un même environnement de programmation, et, tout en respectant scrupuleusement leur définition, développent un nouveau compilateur pour chacun de ces langages. Outre la duplication de travail, cette démarche pose le problème général des dialectes de langages, dont la communauté synchrone semblait jusqu'ici avoir été préservée.

La démarche que nous suivons, si elle évite de lourds investissements en développement logiciels, pose des problèmes théoriques intéressants. Après avoir travaillé essentiellement sur le mélange LUSTRE+ARGOS, nous nous sommes penchés récemment sur ARGOS+ESTEREL, sur la suggestion de G. Berry. Charles André, de l'Université de Nice, travaille pour sa part à la définition de SYNCHARTS [And96, AG95], un langage graphique inspiré du GRAFCET et des STATECHARTS, et compilé en ESTEREL. Les problèmes rencontrés et les solutions envisagées sont très similaires.

## Extensions temporelle et hybride

Quelque temps plus tard, vers la fin de 1992, un nouveau thème apparaît. Une partie de l'équipe commence à travailler sur le modèle des automates temporisés (*Timed Graphs* [AD90])
pour la modélisation des systèmes temporisés. Xavier Nicollin définit l’algèbre ATP (Algebra of Timed Processes) et sa sémantique en termes d’automates temporisés. Nous proposons alors une extension temporelle d’ARGOS et sa sémantique en termes d’automates temporisés. L’extension temporelle s’inspire d’une construction de temporisation des états proposée dans l’un des premiers rapports de recherche sur les Statecharts datant de 1984, mystérieusement disparue ensuite.

Ce travail est ensuite intégré à la thèse de Muriel Jourdan, intitulée : *Un environnement multi-langages et multi-outils pour la programmation et la vérification des systèmes réactifs*. M. Jourdan intègre l’extension temporelle au compilateur ARGOS existant, et nous commençons à expérimenter la modélisation de systèmes en ARGOS temporisé. Le compilateur produit des automates temporisés au format d’entrée de l’outil KRONOS développé dans l’équipe par S. Yovine et A. Olivero. KRONOS permet d’évaluer des formules de logique temporelle temps-réel sur un automate temporisé et implante un algorithme d’évaluation symbolique défini par X. Nicollin et J. Sifakis. L’utilisation du compilateur ARGOS couplé avec KRONOS trouve une application intéressante dans le stage post-doctoral que Muriel Jourdan effectue dans l’équipe de Bernard Espiau en 1994-95. Il s’agit de modéliser des schémas de synchronisation de tâches-robots en ARGOS temporisé, afin de détecter des blocages. Le travail s’intègre dans le projet ORCCAD [SECK93] (Open Robot Controller Computer Aided Design) de l’INRIA.

Pour cette première extension d'ARGOS, nous avons redéfini la sémantique des constructions, qui expriment maintenant des compositions de "machines de Mealy temporisées". Ce sont des automates dont les transitions et les états peuvent porter des informations temporelles. Cette nouvelle sémantique et sa propriété de compositionnalité s'inspirent bien sûr des travaux antérieurs, et ne représentent donc pas un travail théorique démesuré, 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.

## Généralisation : ARGOS comme constructeur d'automates décorés

Ce souci conduit alors assez naturellement à l'idée suivante : peut-on considérer ARGOS comme un jeu d'opérateurs permettant de construire de gros automates à partir d'automates plus petits, et ceci indépendamment de la nature des informations portées par les états et les transitions ? Nous appliquons cette idée à la modélisation des systèmes dits *hybrides*, dans lesquels des composants discrets contrôlent une activité continue. Dans le cas général l'activité continue est décrite par des systèmes d'équations différentielles, qui constituent un modèle hors de portée des capacités d'analyse de propriétés par des méthodes informatiques. Nous utilisons un modèle des systèmes hybrides moins expressif, qui associe aux états et transitions d'un automate des systèmes de contraintes linéaires. Ce modèle est analysable par des méthodes approchées développées par N. Halbwachs.

Ce travail aboutit à la réalisation du prototype HARGOS, qui permet de décrire des programmes ARGOS en associant aux états et transitions des automates de base des "pragmas" de nature quelconque. Ces pragmas ne sont pas analysés par le compilateur, qui se contente de produire un unique automate (le résultat de la composition) dont les états et les transitions portent des compositions de pragmas. N. Halbwachs développe la connexion d'HARGOS à son outil POLKA d'analyse de systèmes de contraintes linéaires. Un sous-produit de ce travail est un nouveau compilateur d'ARGOS temporisé en automates temporisés, qui rentre maintenant dans un cadre plus général.
## Non déterminisme et langages synchrones

C'est en traitant des exemples de systèmes hybrides grâce au prototype HARGOS que nous commençons à nous poser des questions de fond sur la signification du non déterminisme dans les langages synchrones, et sur le bien fondé de la technique des oracles pour simuler le non déterminisme des systèmes hybrides en ARGOS. Le chapitre 4 présente les problèmes de représentation du non déterminisme, en particulier pour des exemples issus de la modélisation des systèmes hybrides. Il s'agit d'une étude centrée sur ARGOS, mais qui clarifie les aspects de non déterminisme dans les langages synchrones, et est applicable à d'autres langages.

## Sémantique en systèmes d'équations

La première étude du langage ARGOS+LUSTRE avait déjà conduit à définir une traduction structurelle d'ARGOS en LUSTRE, c'est-à-dire en équations. Nous avons ensuite retravaillé cette traduction pour obtenir un programme au format d'entrée de l'outil Bac (Boolean Automaton Checker) développé par N. Halbwachs pour étudier les problèmes de causalité [HM95].

Finalement, le format commun DC [CS95] a été défini. Il s'agit d'un format équationnel commun à tous les langages synchrones, pour lequel des outils communs seront définis. L'environnement de programmation actuel d'ARGOS est basé sur une première phase de traduction d'ARGOS en systèmes d'équations, modèle sur lequel de nombreuses manipulations peuvent être effectuées de manière symbolique. La traduction en DC est ensuite facile, de même que la connexion à Bac.

### 1.4.3 Travaux en cours et perspectives

Les différentes directions de recherche suivies, qui auraient pu conduire à la dispersion du travail, semblent maintenant converger.

Nous avons défini une syntaxe textuelle pour ARGOS, dans laquelle figurent les constructions de base, les constructions nécessaires à l'extension temporisée, la possibilité d'attacher des pragmas de nature quelconque aux états et transitions des automates de base, et diverses autres extensions. La sémantique repose toutefois sur le jeu d'opérateurs primitif décrit au chapitre 2. La démarche qui consistait à simplifier le plus possible le formalisme des Statecharts afin de n'en garder que la hiérarchie des automates a conduit à un jeu d'opérateurs assez réduit, dont la sémantique s'exprime simplement, et qui a de bonnes propriétés comme la compositionnalité. D'autre part la plupart des constructions des Statecharts qui avaient été écartées dans un premier temps, pour leur sémantique ambiguë ou leur redondance, ont pu être réintroduites sous forme de macro-notations, sans changer, donc, le coeur du langage.

Le travail suit maintenant deux voies : l'étude et la réalisation d'un moteur synchrone de composition d'automates décorés (éventuellement non déterministes); la programmation multi-langage synchrone, et plus précisément la programmation mixte ARGOS/LUSTRE, ARGOS/ESTEREL ou même ARGOS/LUSTRE/ESTEREL, par compilation en format intermédiaire DC.

J. Buck de Synopsys a par ailleurs choisi ARGOS parmi toutes les variantes de langages et de sémantiques proposées pour les Statecharts. ARGOS est utilisé comme base sémantique d'un langage de description de circuits offrant des compositions hiérarchiques d'automates, et traduit en ESTEREL. Les extensions proposées suivent les idées exposées au chapitre 9.

L'équipe d'Axel Poigné à la GMD développe un environnement de programmation multi-langages en utilisant LUSTRE, ARGOS et ESTEREL.
## 1.5 Organisation du document

Le document ne suit pas un ordre chronologique. Après cette brève introduction générale au domaine de la modélisation et de la validation des systèmes réactifs, et à l'approche synchrone, il est organisé autour de quatre thèmes :

- La définition d'ARGOS: Je présente la définition actuelle, figée depuis environ 4 ans, et sur laquelle s'appuient les autres parties. Je ne reviendrai pas sur les différentes étapes de définition du langage. D'autre part une certaine déformation professionnelle d'enseignant <fnref n="3" />, jointe à quelques soucis pédagogiques apparus lors de la présentation du langage à des publics peu familiers des arcanes de la sémantique opérationnelle à la Plotkin, ont conduit à remettre cent fois sur le métier la formulation de la sémantique d'ARGOS. Dans ce document, je présente les différents thèmes de manière unifiée, en utilisant la formulation à mon avis la plus satisfaisante, c'est-à-dire la plus récente. Ceci explique la différence de forme entre les articles joints et ce document, mais devrait permettre une meilleure compréhension globale.

L'étude d'ARGOS a conduit à deux travaux théoriques, motivés rapidement et présentés dans cette partie: une solution à l'introduction du non déterminisme dans un langage synchrone; un cadre général pour comparer des modes de communication synchrone dans les algèbres de processus ou les langages.

Je présente également dans cette partie quelques réflexions relatives à la syntaxe concrète du langage.

- La programmation multi-langages: on trouve dans cette partie un rappel des premiers travaux sur le sujet, qui ont conduit aux publications [JLMR94, JLMR93] et sont exposés en détail dans la thèse de Muriel Jourdan [Jou94]. J'expose ensuite l'état actuel des travaux sur la programmation ARGOS+LUSTRE via DC, qui offre l'avantage de reporter sur le format DC le problème de détection des programmes non causaux, où il semble être plus facile à résoudre. On lira également un chapitre sur les propositions d'intégration ARGOS+ESTEREL, lesquelles ressemblent énormément aux propositions de Charles André pour les SyncCharts.

- Les extensions temporelle et hybride: cette partie reprend rapidement les motivations et les résultats de [JMO93], et présente plus en détail les applications du couplage ARGOS temporisé + KRONOS, dans une application en robotique.

- L'environnement de programmation ARGONAUTE: J'aborde ici les aspects d'édition syn-taxique graphique du langage; de compilation vers diverses représentations des systèmes de transitions; de connexion à divers outils de vérification.

La dernière partie présente quelques unes de mes activités d'enseignement et s'attache à illus-trer les influences réciproques entre enseignement et recherche. Le chapitre 14 intitulé *Automates et programmation par événements en DEUG* reprend la discussion sur la mémoire nécessaire au calcul des "sorties", pour l'étude des algorithmes itératifs.

<footnote n="3">3. lequel doit chaque année se prémunir contre l'ennui de présenter deux fois le même sujet de la même manière</footnote>
1.6 Sources

La plupart des chapitres correspondent à des articles publiés, à des travaux rédigés sous forme de rapports de recherche, à des documentations techniques, ou à des mémoires d'étudiants. L'intention des paragraphes d'introduction est de replacer l'article dans le contexte général, de reconnaître les apports extérieurs, et de compléter le contenu technique par des commentaires souvent tirés des réactions aux présentations orales. La première partie est détaillée, de manière à rendre la suite compréhensible. Les 3 autres parties sont surtout construites comme un guide de lecture des articles.

Les articles les plus significatifs sont reproduits en annexe.

Le chapitre 14 est adapté de l'ouvrage *Cours d'informatique: langages et programmation* 4, qui constitue le support d'une grande partie des enseignements d'informatique du DEUG mention MIAS (Mathématiques, Informatique et Applications aux Sciences) de Grenoble.

Pour la partie recherche, le texte de ce document est tiré des articles en anglais. Le texte est bien évidemment traduit — et souvent détaillé pour replacer les différents points techniques dans un contexte plus général. Toutefois je n'ai pas traduit les parties mathématiques, ni le texte des figures. Ainsi l'ensemble des états des machines de Mealy s'appelle-t-il S, pour states. Ceci procède d'un choix délibéré : j'ai préféré éviter d'introduire des erreurs ou incohérences dans les parties formelles présentées ici, par des renommages mal contrôlés. Je prie toutefois le lecteur de m'en excuser.

<footnote n="4">4. *Cours d'informatique: langages et programmation*. P.-C. Scholl, M.-C. Fauvet, F. Lagnier et F. Maraninchi, Masson 1993</footnote>
Première partie

Définition d'Argos
<figure><img src="image_3.png" /></figure>
# Chapitre 2

# Les constructions d'Argos

Sources : *La première sémantique qui correspond à la version du langage décrite ici fait l'objet de [Mar92]. Elle est reprise dans [Jou94]. La formulation qui fait apparaître un ensemble d'opérations sur des machines de Mealy est présentée dans [MH96a].*

Comme nous l'avons vu en introduction, un noyau réactif peut être décrit par une machine d'états finis, où les états représentent les valeurs possibles de la mémoire nécessaire au calcul des sorties. En ARGOS, les composants élémentaires des programmes sont de telles machines, dont on donne explicitement l'ensemble des états et l'ensemble des transitions. Le coeur du langage est un ensemble d'opérations qui permettent de composer des machines de Mealy booléennes. On y trouve bien sûr le produit synchrone, qui permet de représenter la mise en parallèle ; une opération d'encapsulation qui permet de définir la portée des signaux d'entrée/sortie échangés entre les différentes machines ; une opération de composition hiérarchique, ou raffinement, directement inspirée de la hiérarchie des états dans les Statecharts. Les composants qui évoluent en parallèle, ou participent à une composition hiérarchique, se synchronisent par *diffusion synchrone* de signaux.

Notons tout de suite que cette vision des choses marque une différence fondamentale avec les Statecharts, où la possibilité de tracer des transitions "inter-niveaux" empêche l'identification de composants indépendants dans un programme. Les sémantiques sont en général décrites globalement. Il n'y a pas de syntaxe qui permettrait de décrire l'ensemble des programmes de manière inductive, et donc pas de sémantique basée sur la syntaxe, dans laquelle la sémantique d'un objet composé dépend de la sémantique des composants.

Nous présentons tout d'abord les machines de Mealy booléennes et les opérations utilisées. Puis nous donnons la syntaxe d'un langage d'expressions faisant intervenir ces opérations. La sémantique de ce langage fait apparaître une notion de programme incorrect, certaines combinations d'opérations étant dépourvues de sens. Nous terminons par l'énoncé de la propriété de compositionnalité de cette sémantique.

La construction d'un véritable *langage*, à partir de cette base théorique, est une étape supplémentaire, qui fait l'objet du chapitre 6.
## 2.1 Exemple commenté

<figure><img src="image_4.png" /><figcaption>FIG. 2.1 – *Un compteur de 'a' modulo 8*</figcaption></figure>

La figure 2.1 donne un programme ARGOS de comptage des signaux d'entrée 'a', avec possibilités d'arrêt et de ré-initialisation. Puisque le système est à mémoire bornée, il s'agit nécessairement d'un compteur borné. On a représenté ici un compteur modulo 8.

La composante de comptage proprement dite est réalisée par la coopération de trois compteurs 1 bit synchronisés sur les retenues. Le compteur démarre à la reception du signal *Start*, et s'arrête à la réception de *Stop*, ou lorsqu'il a accompli un tour complet (émission du signal interne *mod8*). Dans ce dernier cas, il émet le signal *hi* vers l'extérieur.

Les opérations utilisées sont : la *mise en parallèle* des trois compteurs 1 bit ; le *raffinement* de l'état de comptage actif par le compteur proprement dit ; la déclaration des signaux *b*, *c*, *mod8* comme locaux à l'ensemble du programme décrit.

Tout programme ARGOS est construit à l'aide de ces trois opérations.

## 2.2 Machines de Mealy booléennes et opérations

Les points d'interaction élémentaires entre le système et son environnement sont appelés *signaux*. Nous décrivons ici des systèmes capables de traiter des signaux booléens. (On peut imaginer des signaux valués par des réels, par exemple, qui représentent la lecture de capteurs physiques. *ESTEREL* manipule explicitement des signaux valués de types quelconques ; en *LUSTRE* également, les types des flots d'entrée-sortie sont quelconques). Nous considérons un ensemble de noms de signaux A.
### 2.2.1 Machine de Mealy booléenne

**Definition 2.1 : Machine de Mealy booléenne**

Une machine de Mealy est un n-uplet $(S, s_0, I, O, T)$ où $I \subseteq \mathcal{A}, O \subseteq \mathcal{A}$ sont les ensembles de signaux d'entrée et de sorties ; $S$ est l'ensemble des états ; $s_0$ est l'état initial ; $T \subseteq S \times \mathcal{B}(I) \times 2^O \times S$ est l'ensemble des transitions. L'ensemble des machines de Mealy booléennes ainsi définies est noté $M$. □

$\mathcal{B}(I)$ dénote l'ensemble des formules booléennes à variables dans $I$. Sans perte de généralité, on peut considérer que les formules booléennes qui décrivent les conditions d'activation des transitions sont réduites à des monômes.

La figure 2.2 donne un exemple de système simple décrit par un automate. Les noms d'états n'ont pas de sémantique ; l'état initial est distingué par une flèche sans état source ; la structuration des étiquettes de transitions en entrée/sortie est marquée par un caractère '/' . Pour des détails plus complets sur la syntaxe concrète graphique utilisée, voir section 6.

<figure><img src="image_5.png" /><figcaption>FIG. 2.2 – Un système simple décrit par une machine de Mealy booléenne : le système émet $X$ tous les deux $A$, à condition que $B$ soit présent au même instant.</figcaption></figure>

Pour ces objets, définis syntaxiquement, on fournit une relation d'équivalence qui précise quels objets représentent en réalité le même comportement réactif, bien qu'ayant des définitions syntaxiquement distinctes. Ici c'est la *bisimulation* (pour des objets déterministes, cette relation coïncide d'ailleurs avec l'équivalence de trace).

**Definition 2.2 : Bisimulation de machines de Mealy booléennes**

Deux machines $M_1 = (S_1, s_{01}, I, O, T_1)$ et $M_2 = (S_2, s_{02}, I, O, T_2)$ sont dites *bisimilaires*, et on note $M_1 \approx M_2$, si et seulement si il existe une relation d'équivalence $\mathcal{R} \subseteq S_1 \times S_2$ telle que $s_{01} \mathcal{R} s_{02}$ et

$$s \mathcal{R} s' \quad \Rightarrow \quad \left\{ \begin{array}{l} s \xrightarrow{b/o} r \quad \Rightarrow \quad \left\{ \begin{array}{l} \exists b_1, \dots, b_m, r'_1, \dots, r'_m \text{ telle que} \\ \quad \forall i \in [1, m], s' \xrightarrow{b_i/o} r'_i \wedge r \mathcal{R} r'_i \\ \quad \wedge b \Rightarrow (\bigvee_i b_i) \end{array} \right. \\ \text{et inversement.} \end{array} \right.$$

□

Cette notion de bisimulation est une extension de l'équivalence de processus booléens présentée dans [CGS91], dans laquelle nous prenons en compte des étiquettes structurées en entrées/sorties. Dans cette équivalence, on peut faire correspondre à une transition d'un système un ensemble de transitions de l'autre système. La relation est étendue aux états :
**Definition 2.3: Equivalence d'états**

Soient $s, s'$ deux états d'une machine de Mealy booléenne $(S, s_0, I, O, T)$. Par définition $s \approx s'$ ssi $(S, s, I, O, T) \approx (S, s', I, O, T)$. $\square$

Les machines utilisées comme composants de programmes ARGOS doivent satisfaire aux deux
propriétés de déterminisme et réactivité définies par :

**Definition 2.4: Déterminisme et réactivité**

Une machine $(S, s_0, I, O, T)$ est dite *réactive* si et seulement si :

$$
\forall s \in S, \left[ \bigvee_{(s,m,o,s') \in T} m \right] = \text{true}
$$

Elle est dite *déterministe* si et seulement si :

$$
\forall s \in S, \forall t_1 = (s, m_1/o_1, s_1), \forall t_2 = (s, m_2/o_2, s_2), m_1 = m_2 \implies (o_1 = o_2) \land (s_1 \approx s_2)
$$

☐

On notera respectivement $\mathcal{M}^r$, $\mathcal{M}^d$ et $\mathcal{M}^{rd}$ les ensembles de machines *réactives*, *déterministes* et *réactives et déterministes*.

On peut rapprocher la notion de réactivité de ce que les concepteurs des IO-automates [LT89] appellent “input-enabling”. En d’autres termes, une machine réactive est capable de réagir à toute configuration des entrées, dans chacun de ses états. La réactivité (définie par rapport aux entrées) est fondamentale dans un modèle de description des systèmes réactifs, puisqu’elle symbolise le fait que l’environnement est libre. En revanche le déterminisme n’est requis que si l’on a pour but de programmer des systèmes réactifs. Le chapitre 4 discute en détails l’introduction du non-déterminisme dans les langages synchrones.

2.2.2 Produit synchrone de machines de Mealy booléennes

La figure 2.3 donne un programme parallèle sans synchronisation entre les composants. Le système émet un *A* tous les deux *a*, et de même un *B* tous les deux *b*. Le produit synchrone des deux composants est donné figure 2.4. C'est une opération commutative et associative.

<figure><img src="image_6.png" /><figcaption>FIG. 2.3 – *Une composition parallèle sans synchronisation*</figcaption></figure>
<figure><img src="image_7.png" /><figcaption>FIG. 2.4 – Expansion du produit synchrone</figcaption></figure>

Cette opération est décrite formellement par :

**Definition 2.5 : Produit synchrone**

$$ \times : \mathcal{M} \times \mathcal{M} \to \mathcal{M}. $$

$$ (S_1, s_{01}, I_1, O_1, T_1) \times (S_2, s_{02}, I_2, O_2, T_2) = (S_1 \times S_2, (s_{01}, s_{02}), I_1 \cup I_2, O_1 \cup O_2, T') $$

Où $T'$ est défini par :

$$ ((s_1, m_1, o_1, s'_1) \in T_1, (s_2, m_2, o_2, s'_2) \in T_2) \implies ((s_1, s_2), m_1 \wedge m_2, o_1 \cup o_2, (s'_1, s'_2)) \in T') \quad \square $$

Il est aisé de montrer que le produit synchrone préserve le déterminisme et la réactivité des composants.

### 2.2.3 Encapsulation

L'encapsulation n'a de sens que pour forcer la synchronisation entre deux composants. Deux composants X et Y peuvent être synchronisés s'ils fonctionnent en parallèle et si une sortie de l'un est une entrée de l'autre. Pour déclarer qu'un signal ne doit être utilisé qu'aux fins de synchronisation entre deux composants, on peut le déclarer *local* à l'ensemble de ces deux composants. Cette opération a un effet de renommage usuel, comme les déclarations de variables locales à un bloc dans un langage séquentiel classique (deux occurrences du même nom de signal, sous la portée de deux opérations de déclaration distinctes, représentent des signaux différents). D'autre part, un signal *local* n'est pas diffusé à l'extérieur de la zone définie par l'opération qui le déclare, et ne peut pas non plus provenir de l'extérieur de cette zone. Par conséquent, dans la portée d'un opérateur qui déclare un signal $x$, une transition dont la condition nécessite la présence de $x$ ne peut être exécutée que si $x$ est produit dans la même zone, durant la même réaction. (Cette opération décrit une membrane étanche dans les deux sens ; elle est analogue à la construction *signal ... in ... end* d'ESTEREL, et à la déclaration de flots locaux à un noeud en LUSTRE. La sémantique des Statecharts de [HGdR88] propose deux opérations — fermeture et abstraction — qui représentent les deux membranes semi-perméables correspondantes).
La figure 2.5 donne un système qui émet un *A* tous les 4 *a* ; c'est un compteur 2 bits. Il est composé de deux compteurs 1 bit qui se synchronisent sur le signal *l*.

<figure><img src="image_8.png" /><figcaption>FIG. 2.5 – Synchronisation et signaux locaux</figcaption></figure>

La figure 2.6 est une expansion partielle du programme de la figure 2.5, où seule la composition
parallèle a été prise en compte. On construit toutes les combinaisons possibles d'une transition
du premier processus et d'une transition du second, et l'étiquette est construite en prenant la
conjonction des conditions et l'union des ensembles de signaux émis.

<figure><img src="image_9.png" /><figcaption>FIG. 2.6 – Expansion de la composition parallèle</figcaption></figure>

La figure 2.7 donne la machine obtenue par application de l'opération d'encapsulation. Notez
que *a* reste la seule entrée du système.
<figure><img src="image_10.png" /><figcaption>FIG. 2.7 – Expansion de l'opération d'encapsulation</figcaption></figure>

Nous donnons la définition de l'opération d'encapsulation en considérant que la partie condición des étiquettes de transitions est réduite à un monôme, par souci de simplicité, et sans perte de généralité.

**Definition 2.6 : Encapsulation**

\$ : $\mathcal{M} \times 2^A \to \mathcal{M}$

$(S, s_0, I, O, T) \setminus \Gamma = (S, s_0, I \setminus \Gamma, O \setminus \Gamma, T')$, où $T'$ est défini par :

$$ (s, m, o, s') \in T \wedge m^+ \cap \Gamma \subseteq o \wedge m^- \cap \Gamma \cap o = \emptyset \implies (s, \exists \Gamma.m, o \setminus \Gamma, s') \in T' \quad \square $$

$m^+$ dénote l'ensemble des variables qui apparaissent positives dans le monôme $m$ (c'est-à-dire $m^+ = \{x \in \mathcal{A} \mid (x \wedge m) = m\}$). $m^-$ dénote l'ensemble des variables qui apparaissent négatives dans le monôme $m$ (c'est-à-dire $m^- = \{x \in \mathcal{A} \mid (\neg x \wedge m) = m\}$).

Intuitivement, une transition $(s, m, o, s') \in T$ subsiste dans la machine résultat de l'encapsulation si son étiquette satisfait à un critère local : $m^+ \cap \Gamma \subseteq o$, qui signifie que tout signal local supposé présent doit être effectivement émis par la transition ; et $m^- \cap \Gamma \cap o = \emptyset$, qui signifie que tout signal local supposé absent ne doit pas être émis. D'autre part, si l'étiquette de transition satisfait ce critère, elle est modifiée pour cacher les signaux locaux.

L'opération d'encapsulation peut ne pas préserver le déterminisme ou la réactivité de son opérande.

Le chapitre 3 reprend l'essentiel de l'article [JM94b], où cette opération d'encapsulation est généralisée dans un cadre formel qui permet d'exprimer la sémantique de plusieurs calculs synchrones. Le calcul de Milner [Mil89] et les "réactions en chaîne" des Statecharts [PS88] peuvent être décrits par une opération d'encapsulation en variant le critère local et la fonction utilisée pour masquer les objets locaux.

### 2.2.4 Encapsulation et systèmes d'équations

Il n'est pas forcément très facile de se convaincre que la définition de l'opération d'encapsulation ci-dessus correspond à l'idée intuitive de diffusion synchrone des signaux. Une définition de la diffusion synchrone à l'aide de systèmes d'équations booléennes est plus naturelle. L'exemple de la figure 2.8 illustre la correspondance.
## Calcul de l'encapsulation par résolution d'un système d'équations booléennes

<figure><img src="image_11.png" /><figcaption>FIG. 2.8 – *Composition parallèle, encapsulation et systèmes d'équations*</figcaption></figure>

Lorsque le système est dans l'état *ABC*, et que l'entrée $a \land b \land \neg c$ survient, la réaction globale est déterminée par le statut des signaux locaux *x*, *y* et *z*. Ce statut doit être unique : dans une réaction du système, un signal local est présent ou absent, mais ne change pas de statut. D'autre part, on peut écrire le système d'équations suivant :

$$ 
\begin{array}{l}
x = b \land y \lor b \land \neg y \\
y = a \land x \\
z = FALSE \\
a = b = TRUE, c = FALSE
\end{array}
 $$

pour exprimer, entre autres, que : *x* est présent à condition qu'une transition qui émet *x* soit exécutée*, c'est-à-dire lorsque $b \land y$ ou lorsque $b \land \neg y$. Le système a ici une solution unique : $x = y = TRUE, z = FALSE$. En reportant cette information sur le programme, on déduit une transition globale de l'état *ABC* à l'état $A'B'C'$, étiquetée par $a \land b \land \neg c/o$.

Un tel système, pour un état et une configuration des entrées donnés, peut ne pas avoir de solutions, ou en avoir plusieurs. S'il en a plusieurs, c'est que le statut des signaux locaux n'est pas déterminé de manière unique, et en reportant sur le programme les diverses valuations des signaux locaux, on obtient plusieurs transitions issues du même état global, pour la même configuration des entrées : le système global n'est plus déterministe. De manière analogue, le système global n'est plus réactif, s'il existe un état et une configuration des entrées pour lesquels le système est sans solution.

## Comparaison avec la définition des opérations $\times$ et $\backslash$

Le calcul de la machine de Mealy correspondant au programme de la figure 2.8 est réalisé en deux temps : l'expansion de la composition parallèle (opération $\times$), et la suppression de certaines des transitions, d'après le critère de l'encapsulation (opération $\backslash$).

Dans le système obtenu par expansion de la composition parallèle, et puisque cette composition préserve la réactivité, de tout état partent des transitions étiquetées par tous les monômes construits sur l'ensemble des signaux d'entrée *x*, *y*, *z*, *a*, *b*, *c*. Si l'on fixe une valuation *v* des signaux *a*, *b*, *c*, on doit encore trouver tous les monômes $v \land v'$, où $v'$ est une valuation des signaux *x*, *y*, *z*. D'autre part, une transition constitue un parfait résumé des conséquences d'une hypothèse sur le statut des signaux locaux, puisqu'on trouve, dans la partie émission de son étiquette, tous les signaux émis, toutes composantes parallèles confondues.
Dans l'exemple ci-dessus, parmi les transitions issues de l'état ABC pour l'entrée $a \land b \land \neg c$, on trouve : $a \land b \land \neg c \land x \land y \land \neg z/x, y, o$, ce qui signifie que, si l'on suppose $x$ et $y$ présents et $z$ absents, les transitions exécutées sont telles que l'on émet $x$ et $y$ mais pas $z$.

Avant encapsulation, les transitions issues d'un même état, pour la même configuration des signaux externes, présentent donc toutes les hypothèses sur le statut (toutes les valuations booléennes) des signaux locaux $x, y, z$. (En conséquence, si l'encapsulation porte sur $n$ signaux, on trouve $2^n$ transitions par entrée externe et par état. Cela constitue d'ailleurs une raison suffisante pour que le compilateur ne soit pas basé sur une construction explicite des machines en suivant la sémantique présentée ici).

Le critère utilisé pour conserver ou rejeter une transition revient à déterminer si la valuation (l'hypothèse sur le statut) des signaux locaux est une solution du système d'équations correspondant. L'application des deux opérations (composition parallèle et encapsulation) est donc assimilable à la résolution du système d'équations, par essai de chaque valuation des inconnues.

### 2.2.5 Condition d'activation

Il s'agit d'une opération unaire, paramétrée par une condition booléenne quelconque, qui exprime qu'un processus ne fonctionne que lorsque cette condition est vraie. Combinée avec un raffinement, elle permet d'exprimer la suspension de processus.

**Definition 2.7: Condition d'activation**

$$ \Delta : \mathcal{M} \times \mathcal{B}(\mathcal{A}) \to \mathcal{M} $$

$$ (S, s_0, I, O, T) \triangleq b = (S, s_0, I \cup \mathrm{Var}(b), O, T' \cup \{(s, \neg b, \emptyset, s)|s \in S\}) $$

$$ \text{où } T' \text{ est défini par: } (s, m, o, s') \in T \iff (s, m \land b, o, s') \in T' $$

☐

**Exemple 2.1: Filtrage des entrées**

La définition d'une condition d'activation peut être utilisée, par exemple, pour filtrer les entrées d'un processus. Pour exprimer que le processus $P$ ne réagit qu'à une occurrence du signal $a$ sur deux, on peut écrire :

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

☐

### 2.2.6 Raffinement, ou composition hiérarchique

**Exemple 2.2: Différents types de terminaison**

Dans un raffinement, un automate joue le rôle de *contrôleur*, qui peut lancer et arrêter ses processus raffinants. Une transition issue d'un état $X$ raffiné par $P$ interrompt $P$. Toutefois cette transition peut-être provoquée par un événement issu de $P$. La figure 2.9 illustre les différentes
situations. stop et reset sont des interruptions du processus raffinant ; reset tue le processus, et en relance un exemplaire dans son état initial, au cours de la même réaction. La transition end, en revanche, étant déclenchée par un signal que le processus raffinant émet lui-même, peut être considérée comme une terminaison normale.

<figure><img src="image_13.png" /><figcaption>FIG. 2.9 – Raffinement et terminaison</figcaption></figure>

☐

L'opération de raffinement, dont les arguments sont un automate à *n* états et *n* machines destinées à raffiner ces états, est décrite formellement ci-dessous.

**Definition 2.8: Raffinement**

$$ \triangleright : \mathcal{M} \times 2^{\mathcal{M}} \to \mathcal{M} $$

Notons $M = (S, s_0, I, O, T)$ où $S = \{s_0, s_1, ..., s_n\}$. Considérons également un ensemble $\{M_j\}_{j=0..n}$ de machines à utiliser pour raffiner les états de $M$, où $M_j = (S^j, s_0^j, I^j, O^j, T^j)$, et $S^j = \{s_0^j, s_1^j, ..., s_{n_j}^j\}$.

La machine composée, dans laquelle chaque $M_j$ raffine l'état $s_j$ correspondant, est de la forme :

$$ M \triangleright \{M_j\}_{j=0..n} = (S \triangleright \{S^j\}_J, s_0 \triangleright s_0^0, I \cup I^j, O \cup O^j, T^j). $$

Son ensemble d'états est de la forme :

$$ S \triangleright \{S^j\}_J = \bigcup_{j=0}^{n} \{s_j \triangleright s_k^j, k \in [0..n_j]\} $$

Et ses transitions $T'$ sont données par les deux règles suivantes :

1) Une transition de $s_a$ à $s_b$ dans la machine de contrôle, jointe à une transition de $s_k^a$ à $s_{k'}^a$ dans la machine raffinant l'état courant. Les sorties sont rassemblées. Dans l'état but global, la machine raffinant l'état $s_b$ est lancée dans son état initial, et la machine raffinant l'état $s_a$ a été tuée. Son état interne n'est plus pertinent :

$$ (s_a, m, o, s_b) \in T \wedge (s_k^a, m', o', s_{k'}^a) \in T^a \implies (s_a \triangleright s_k^a, m \wedge m', o \cup o', s_b \triangleright s_0^b) \in T' $$

2) Une transition de la machine raffinant l'état courant, de $s_k^a$ à $s_{k'}^a$, lorsqu'aucune transition issue de $s_a$ n'est activable dans la machine de contrôle :

$$ (s_k^a, m', o', s_{k'}^a) \in T^a \implies (s_a \triangleright s_k^a, m' \wedge \left[ \bigwedge_{(s_a, m, o, s_b) \in T} \neg m \right], o', s_a \triangleright s_{k'}^a) \in T' $$

☐

Le raffinement n'est pas primitif, et peut-être construit de manière structurelle à l'aide de la mise en parallèle et de la déclaration de signaux locaux. Une partie du DEA de Muriel Jourdan en
1990/91 consistait à démontrer cette propriété et à traduire ARGOS, après une phase d'élimination des raffinements, dans l'un des formats intermédiaires du compilateur ESTEREL, IC. Ce travail est implanté dans le compilateur ARGOS (voir aussi le chapitre 13).

Dans la plupart des articles où il s'agit de donner la sémantique formelle d'un jeu d'opérateurs pour prouver des propriétés de compositionnalité, ou pour étudier les problèmes de déterminisme et de réactivité, nous omettons le raffinement. Nous le présentons néanmoins comme une opération à part entière, lorsqu'il s'agit d'illustrer l'adéquation du jeu d'opérations à la description de structures courantes des systèmes, ou lorsque la présence d'opérations de raffinement explicitement voulues par le programmeur est utilisée pour améliorer une compilation d'ARGOS. C'est le cas, typiquement, lorsqu'on s'intéresse à la traduction en systèmes d'équations munies de conditions d'activation (voir chapitre 5).

**Raffinement avec initialisation** Le raffinement est une structure qui permet de contrôler l'activité d'un ensemble de processus. Le processus qui raffine un état X réagit toujours dans l'instant où le contrôleur le détruit en quittant l'état X. En revanche, le processus qui raffine un état X ne réagit jamais dans l'instant où le contrôleur le crée en entrant dans l'état X. Cette restriction impose des contraintes à la conception des systèmes.

Toutefois, si l'on introduit le raffinement avec initialisation du processus crée, il faut traiter les problèmes dits de "réincarnation", tels qu'ils apparaissent en ESTEREL dans les boucles. En effet, une transition qui boucle sur un état raffiné contrôle en fait deux instances du processus raffinant : l'une est en train de disparaître, et exécute une dernière transition ; l'autre est en cours de création, et exécute une première transition. La compilation doit tenir compte de cette possibilité d'existence de plusieurs instances d'un même objet — dont l'intersection des périodes d'existence ne couvre toutefois qu'un instant, ce qui permet de traiter le problème en évitant la duplication de code. Le problème est similaire à celui traité par P. Caspi pour l'extension récursive de LUSTRE.

Nous reviendrons sur le raffinement avec initialisation au chapitre 9 qui expose les possiblités de mélange ARGOS+ESTEREL.

## 2.3 Un langage d'expressions et sa sémantique

A partir de ce jeux d'opérateurs, on définit le langage $\mathcal{E}$ des programmes par une grammaire d'expressions d'axiome $E$, qui détermine les imbrications possibles d'opérateurs :

<table><tr><td>E</td><td>::=</td><td>E || E</td><td>Composition parallèle</td></tr><tr><td></td><td>|</td><td><span style="text-decoration: overline;">E</span><sup>Γ</sup></td><td>Encapsulation Γ ⊆ A</td></tr><tr><td></td><td>|</td><td><b>R</b><sub>M</sub>(R<sub>1</sub>, ..., R<sub>n</sub>)</td><td>Raffinement de M par les R<sub>i</sub></td></tr><tr><td></td><td>|</td><td>E when b</td><td>Condition d'activation</td></tr><tr><td>R</td><td>::=</td><td>E | NIL</td><td>Processus raffinants</td></tr></table>

La notation NIL est introduite pour identifier les états terminaux, non raffinés, des machines du programme.
La fonction sémantique $\mathcal{S} : \mathcal{E} \to \mathcal{M}^{rd} \cup \{\perp\}$ est définie récursivement par :

$$ \mathcal{S}(E_1 \parallel E_2) = \begin{cases} \perp & \text{si } \mathcal{S}(E_1) = \perp \text{ ou } \mathcal{S}(E_2) = \perp \\ \mathcal{S}(E_1) \times \mathcal{S}(E_2) & \text{sinon} \end{cases} $$

$$ \mathcal{S}(\mathbf{R}_{M^d}(R_1, \dots, R_n)) = \begin{cases} \perp & \text{si } \exists i \in [1, n] \text{ t.q. } \mathcal{S}(R_i) = \perp \\ M^d \triangleright (\mathcal{S}(R_1), \dots, \mathcal{S}(R_n)) & \text{sinon} \end{cases} $$

$$ \mathcal{S}(\overline{E^{\Gamma}}) = \begin{cases} \perp & \text{si } \mathcal{S}(E) = \perp \\ \text{sinon: soit } X = \mathcal{S}(E) \setminus \Gamma \text{ dans } & \text{si } X \in \mathcal{M}^{rd} \text{ alors } X \text{ else } \perp \end{cases} $$

$$ \mathcal{S}(E \text{ when } b) = \begin{cases} \perp & \text{si } \mathcal{S}(E) = \perp \\ \mathcal{S}(E) \triangle b & \text{sinon} \end{cases} $$

$$ \mathcal{S}(\text{NIL}) = (\{\text{NIL}\}, \text{NIL}, \emptyset, \emptyset, \{(\text{NIL}, \text{true}, \emptyset, \text{NIL})\}) $$

Un programme $P$ est dit *incorrect* si et seulement si $\mathcal{S}(P) = \perp$. Les erreurs sont détectées lors des encapsulations, si le résultat de l'opération n'est pas réactif et déterministe. La valeur d'erreur $\perp$ se propage.

Cette notion de correction est en quelque sorte minimale. Considérant que les objets construits doivent être à la fois déterministes et réactifs, et que l'hypothèse de synchronisme — qui est à la base de l'opération d'encapsulation — peut faire apparaître des objets non déterministes ou non réactifs, on ne peut pas accepter toutes les constructions.

Cette notion de correction ne correspond pas à la notion dite “de causalité” introduite pour ESTEREL. Les réflexions sur une notion de causalité pour ARGOS étant entièrement inspirées de l'exemple d'ESTEREL, elles sont reportées au chapitre 9 “Argos + Esterel”.

## 2.4 A propos d'expressivité

Toute proposition d'un jeu d'opérateurs, dans quelque domaine que ce soit, pour décrire une certaine classe d'objets, suscite une interrogation légitime: *est-ce suffisant* ? Par exemple on sait qu'en supprimant la récursivité et la boucle de type “while” dans un langage structuré (sans branchements intempestifs), on réduit l'ensemble des programmes possibles. Pour formaliser cette question, on peut considérer l'ensemble des objets à décrire $Y$, l'ensemble $E$ de toutes les expressions engendrées par le jeu d'opérateurs, et la fonction $f$ qui décrit la correspondance entre expressions et objets à décrire. On a en général $f(E) \subseteq Y$. Reste à savoir si $Y \subseteq f(E)$, c'est-à-dire si $f$ est surjective.

Dans le cas d'ARGOS exposé ci-dessus, où il s'agit de choisir un jeu d'opérateurs pour décrire des machines de Mealy booléennes, la réponse est triviale: les objets de $Y$, c'est-à-dire les machines de Mealy, sont des constantes du langage proposé, et, pour une machine $M$, $f(M) = M$. (En LUSTRE, la propriété est un peu moins triviale, on la prouve en exhibant un codage systématique des machines de Mealy en programmes LUSTRE, c'est-à-dire une fonction $g$ de $Y$ vers $E$, telle que $f(g(y)) = y$).

Nous avons signalé plus tôt que le raffinement n'est pas une opération primitive; on voit ici que la composition parallèle ne l'est pas plus. Cette notion d'expressivité n'est donc pas très intéressante. On aimerait toutefois trouver des raisons à l'introduction de certains opérateurs comme la condition d'activation.
### 2.4.1 Comparaison avec ESTEREL

Une des manières de juger l'adéquation du jeu d'opérateurs ARGOS à la description des systèmes réactifs est de le comparer aux constructions d'ESTEREL, langage pour lequel un travail considérable de choix des structures adéquates a été réalisé ([Ber93] décrit un jeu d'opérateurs à l'aide duquel on peut obtenir toutes les constructions d'ESTEREL). Le chapitre 9, en décrivant les motivations d'une utilisation mixte ARGOS/ESTEREL, fournit des éléments de comparaison précis. Je donne ici un simple exemple de construction ARGOS pour exprimer l'une des structures de contrôle temporelles d'ESTEREL : l'interruption préemptive (le “watching” fort).

<figure><img src="image_14.png" /><figcaption>FIG. 2.10 – *Expression des interruptions préemptives*</figcaption></figure>

La figure 2.10 illustre la construction des interruptions préemptives grâce à l'opération qui associe une condition d'activation au processus raffinant. L'interruption par *i* n'est pas préemptive. Ainsi, si *i* et *a* surviennent simultanément, le système passe de l'état *A* à l'état *Y* en émettant *b*. L'interruption par *p*, en revanche, est préemptive. Si *p* et *a* surviennent dans l'état *A*, le système passe dans l'état *Y*, mais sans émettre *b*.

### 2.4.2 Comparaison avec les Statecharts

ARGOS est bien sûr issu des Statecharts, mais n'en a conservé que la structure hiérarchique des automates. La sémantique construite sur l'hypothèse de synchronisme doit bien plus à ESTEREL qu'aux Statecharts (la description “officielle” de la sémantique implantée dans l'outil Statemate est basée sur une communication synchrone “retardée” : un signal émis par une composante ne peut être utilisé par les autres composantes que lors de la réaction suivante. Ce mécanisme est strictement plus faible que la véritable diffusion synchrone, mais beaucoup plus simple à décrire). ARGOS a été construit en dépouillant petit à petit les Statecharts de leurs nombreuses constructions à sémantique ambiguë. Pourtant la plupart de ces constructions peuvent être obtenues en utilisant le jeu d'opérations présenté ici, à condition de disposer de la véritable diffusion synchrone. C'est le cas, très simplement, pour les transitions inter-niveaux sortantes. Dans l'exemple commenté au paragraphe 2.1, la transition issue de l'état On avec la condition *mod8* est exactement le codage d'une transition inter-niveaux issue des trois états One, avec la condition *c*. Toutes les transitions inter-niveaux sortantes des Statecharts (dont il est en général difficile de dire si elles représentent des interruptions préemptives ou non, puisque la définition de leur portée constitue un problème en soi) peuvent ainsi être exprimées par des synchronisations entre les processus raffinants et l'automate contrôleur.
Les transitions entrantes, en revanche, supposent dans le cas général la définition du raffinement avec initialisation du processus raffinant sur les transitions entrantes, qui pose tous les problèmes de ré-incarnation d'ESTEREL. Voir le chapitre 9 pour une discussion de ces aspects.

Le chapitre 3 propose un cadre dépouillé où la comparaison des modes de synchronisation d'ARGOS et des Statecharts est simple.

## 2.5 A propos de compositionnalité

### 2.5.1 Propriété de compositionnalité pour ARGOS

Le langage ARGOS est conçu comme un jeu de construction pour fabriquer des objets définis a priori, les machines de Mealy à étiquettes booléennes. Ces objets sont définis de manière syntaxique, mais on se donne une relation d'équivalence qui exprime quelles machines doivent être considérées comme représentant le même comportement réactif. Cette relation est la bisimulation définie plus haut (définition 2.2). On exige que cette relation soit une congruence pour les opérations du langage.

Cette démarche est générale. Quel que soit le type de modèle que l'on désire construire, s'il existe une relation d'équivalence pour déterminer quels modèles représentent en fait le même comportement, malgré leurs différences syntaxiques, cette relation doit être une congruence pour les opérateurs du langage. On retrouve ce raisonnement et l'exigence de compositionnalité aux chapitres 3 et 4.

A partir de l'équivalence des modèles, on définit une équivalence de programmes, notée $\equiv$, par :

**Definition 2.9: Equivalence de programmes**

$$ P_1 \equiv P_2 \iff \left\{ \begin{array}{l} S(P_1) \neq \perp \land S(P_2) \neq \perp \land S(P_1) \approx S(P_2) \quad \lor \\ S(P_1) = S(P_2) = \perp \end{array} \right. \quad \square $$

La propriété de compositionnalité du langage présenté ici repose sur le théorème suivant :

**Théorème 2.1**

L'équivalence de programmes est une congruence pour les opérateurs du langage. Autrement dit :

$$ \forall P, Q \in \mathcal{P}, \forall C \text{ contexte d'opérateurs } P \equiv Q \implies C[P] \equiv C[Q] \quad \square $$

Si deux programmes ARGOS ont des images bisimilaires par la fonction sémantique, ils se comportent de la même façon dans tout contexte.

### 2.5.2 Congruences et complète adéquation

La comparaison entre ARGOS et les Statecharts a souvent conduit à un débat entre sémantique opérationnelle+congruence, et sémantique dénotationnelle+propriété de complète adéquation (ou "full abstraction"). A ma connaissance, les seules sémantiques à la fois compositionnelles et correctes proposées pour les Statecharts sont dénotationnelles (voir par exemple [HGdR88]). Je
ne me lancerai pas dans une comparaison formelle de ces deux techniques. Notons simplement que la sémantique d'ARGOS présentée ici possède la propriété de complète adéquation, de manière triviale.

En paraphrasant la remarquable introduction de [Sto88], on peut préciser le cadre formel en quatre points (voir figure 2.11) :

- On considère un ensemble $\mathcal{T}$ de termes, définis syntaxiquement, et formant un langage. Parmi ces termes, certains, qu'on appellera des programmes, correspondent à des comportements observables; par exemple, dans un langage impératif séquentiel classique, les expressions ne sont pas des programmes, alors que les procédures en sont. Un programme est en général un terme clos, vis-à-vis des identificateurs dont la portée est définie statiquement.

- On définit une notion de comportement observable des programmes, par une fonction $O$ d'un sous-ensemble de $\mathcal{T}$ vers un ensemble de comportements $\mathcal{B}$. Pour un langage déterministe classique, le comportement peut être une fonction des entrées vers les sorties.

- On définit une équivalence de termes par : $P \equiv Q \iff \forall C, O(C[P]) = O(C[Q])$, où $C$ représente un contexte syntaxique définissant un programme. Autrement dit, deux programmes sont dits équivalents s'ils sont interchangeables, dans tout contexte, sans effet sur le comportement global.

- On peut ensuite chercher à caractériser sémantiquement la notion d'équivalence de programmes, en trouvant un ensemble de modèles $\mathcal{M}$ et une fonction sémantique $\mathcal{S}$ de $\mathcal{T}$ vers $\mathcal{M}$ telle que $P \equiv Q$ se ramène à $\mathcal{S}(P) = \mathcal{S}(Q)$. Plus précisément, on dit que le modèle est correct lorsque seuls des termes équivalents ont même image par la fonction sémantique, c'est-à-dire $\mathcal{S}(P) = \mathcal{S}(Q) \implies P \equiv Q$. On dit que le modèle est complètement adéquat si, de plus, $P \equiv Q \implies \mathcal{S}(P) = \mathcal{S}(Q)$, c'est-à-dire que deux termes équivalents sont toujours identifiés par la fonction sémantique. D'autre part, en sémantique dénotationnelle, la fonction $\mathcal{S}$ est décrite fonctionnellement, et la substitutivité garantit que l'égalité des modèles est une congruence pour les opérations du langage.

<figure><img src="image_15.png" /><figcaption>FIG. 2.11 – Termes, programmes, comportements et modèles</figcaption></figure>

Dans le cas d'ARGOS, tous les termes sont des programmes, puisque la plus petite structure syntaxique est l'automate, et coïncide avec la notion de comportement observable. On a donc aussi $\mathcal{B} = \mathcal{M}$ et $\mathcal{S} = \mathcal{O}$. La propriété de congruence énoncée plus haut garantit donc $P \equiv Q \iff \mathcal{S}(P) = \mathcal{S}(Q)$.
# Chapitre 3

## Modèles généraux pour les langages synchrones

Sources: *Ce chapitre est tiré pour l'essentiel de [JM94b]. La comparaison des modes de synchronisation d'ARGOS et des Statecharts n'a jamais été publiée telle que.*

Le travail publié dans [JM94b], qui peut être vu comme un certain aboutissement des multiples ré-écritures de la sémantique d'ARGOS, a son origine dans de nombreuses et intéressantes discussions avec Amir Pnueli à Rehovot en 1991, au cours desquelles nous tentions de rapprocher la sémantique d'ARGOS d'une version de la sémantique des Statecharts (publiée dans [PS88]). Cet aspect du travail est encore d'actualité car, à ma connaissance, les évolutions récentes de la sémantique des Statecharts suivent les idées présentées dans [PS88] (bien que la sémantique officiellement implantée dans l'outil Statemate soit basée sur une communication synchrone retardée).

Autour du même contenu technique, les arguments ont évolué au cours de 4 ou 5 présentations à des publics plus ou moins familiers des langages synchrones. Je donne ici la structure de l'article, en complétant l'exposé des motivations. Les exposés faisaient une large part à des arguments de *compositionnalité*, que j'ai par ailleurs résumés au chapitre 2, section 2.5.2. En revanche, on oubliera avec profit la conclusion hâtive de l'article, qui tentait de rapprocher un critère esthétique essentiellement subjectif de "simplicité" d'un mode de communication synchrone, d'un critère objectif de quantité d'information nécessaire à assurer la congruence. Reste un cadre unifié permettant d'exprimer divers modes de communication synchrone.

Notons enfin que l'on retrouve dans le chapitre 14, à propos d'algorithmique en DEUG et de conception des itérations, l'essentiel du discours sur la définition de congruences par le biais de fonctions d'abstraction.

### 3.1 Motivations

La plus grande difficulté rencontrée, depuis le début, dans les tentatives de comparaison d'ARGOS— c'est-à-dire de la stricte application de l'hypothèse de synchronisme à des compositions d'automates — et des Statecharts, réside dans le caractère non compositionnel de la plupart des sémantiques proposées pour les Statecharts (à l'exception d'une sémantique dénotationnelle proposée dans [HGdR88], et de la sémantique en algèbre de processus de [US94], laquelle présente par ailleurs quelques erreurs de fond).
En plongeant la sémantique des réactions en chaîne dans le modèle général proposé ici, on fournit, par effet de bord, une sémantique compositionnelle pour un sous-ensemble du langage présenté dans [PS88]. On suggère par ailleurs comment atteindre le langage complet. Cela permet de comparer ARGOS et cette version des Statecharts en se concentrant sur la sémantique de la communication entre composants, et en s'abstrayant, temporairement au moins, des constructions comme le raffinement, avec son cortège de problèmes liés à la présence des transitions inter-niveaux.

## 3.2 Cadre général

Le cadre général que nous proposons ici doit permettre de définir la sémantique d'un mode de communication synchrone avec un minimum d'efforts, simplement en instanciant les quelques paramètres qui apparaissent dans les règles de sémantique. On peut ainsi comparer plusieurs modes de communication en comparant les paramètres utilisés. Le cadre général garantit également l'existence d'une congruence.

Il existe de nombreux formats généraux pour décrire des compositions parallèles et des modes de communication, par exemple [Arn92, AB84]. Le but n'est pas de comparer un nouveau format avec ceux-ci, sur des critères d'expressivité ou d'existence d'une axiomatisation par exemple.

Le format proposé est une variante adaptée à la recherche de congruences, défini en suivant deux idées. Tout d'abord, c'est un format d'algèbre de processus, mais les objets élémentaires sont des automates. Cela évite de considérer un opérateur de récursion, puisque la récursion n'est utilisée, en pratique, que pour décrire des automates à partir du préfixage et du choix non déterministe. En général il faut d'ailleurs résoudre les problèmes d'imbrication de la récursion et de la composition parallèle, qui produisent des objets non réguliers. D'autre part, dans la plupart des algèbres de processus, la sémantique du mode de communication est répartie entre une opération de produit — ou mise en parallèle —, et une opération unaire d'encapsulation — ou restriction, ou encore masquage. En CCS [Mil80] par exemple, les actions $a$ et $\bar{a}$ se fondent en une action invisible $\tau$, lors de la composition parallèle. L'opération de restriction est utilisée pour forcer la synchronisation entre deux composants (sur leurs actions communes) en supprimant, dans leur composition parallèle, les transitions étiquetées par $a$ ou $\bar{a}$ seul. Pour des modes de communication plus complexes, il est parfois difficile de séparer ce qui doit être exprimé dans la mise en parallèle, et ce qui doit être exprimé dans une loi d'encapsulation.

Dans le modèle proposé ici, la mise en parallèle est un simple produit qui conserve l'information maximale. La sémantique de la communication est exprimée entièrement dans la loi de l'encapsulation. Cela permet, en particulier, d'inventer d'autres opérations de composition, par exemple des opérations asymétriques comme le raffinement d'ARGOS, sans remettre en cause la communication entre composants.

### 3.2.1 Syntaxe et sémantique

On définit un ensemble $\mathcal{L}ab$ d'étiquettes, aussi bien pour les systèmes de transitions qui constituent les objets de base des programmes, que pour leurs modèles. Une étiquette est un multi-ensemble d'objets qui peuvent être atomiques ou eux-mêmes structurés, selon la complexité du mode de communication à décrire. Un système de transitions est un n-uplet $LTS = (Q, q_0, T)$ (ensemble d'états, état initial et transitions) et les transitions sont étiquetées par des éléments de $\mathcal{L}ab$ (c'est-à-dire $T \subseteq Q \times \mathcal{L}ab \times Q$).
L'ensemble $\mathcal{P}$ des programmes est décrit par la grammaire : $P ::= LTS \mid P \parallel P \mid \overline{P^Y}$, ou $\parallel$ est la composition parallèle et $\overline{P^Y}$ l'encapsulation. Noter que le paramètre de cette opération est en relation avec la nature de $\mathcal{L}ab$. Ce peut être un élément, un sous-ensemble ou une sous-structure de $\mathcal{L}ab$, si celui-ci est structuré.

La sémantique est une fonction $\mathcal{S}$ de l'ensemble $\mathcal{P}$ des programmes vers l'ensemble des systèmes de transitions étiquetées décrit ci-dessus. Pour les composants de base, on a simplement : $\mathcal{S}(LTS) = LTS$.

Dans une composition parallèle synchrone, une réaction du programme global est toujours constituée d'une réaction de chacun des composants. Notons $\mathcal{S}(P_i) = (Q_i, q_{0i}, T_i)$ le système de transitions associé au composant $P_i$ ($i \in \{1, 2\}$). $\mathcal{S}(P_1 \parallel P_2)$ est alors de la forme $(Q_1 \times Q_2, q_{01} \parallel q_{02}, T')$, et $T'$ est donné par :

$$ \frac{q_1 \xrightarrow{L_1} q'_1, \quad q_2 \xrightarrow{L_2} q'_2}{q_1 \parallel q_2 \xrightarrow{L_1 \bowtie L_2} q'_1 \parallel q'_2} \qquad [P] $$

$\mathcal{W}$ dénote l'union de multi-ensembles, qui préserve les doublons. La composition parallèle ainsi décrite préserve l'information maximale sur les deux transitions qui participent à une réaction globale du système, à condition toutefois d'accepter l'hypothèse raisonnable selon laquelle la composition parallèle est à la fois commutative et associative. Dans le cas contraire, il faudrait conserver, au lieu de l'union des multi-ensembles, un vecteur d'étiquettes. C'est le cas dans le modèle de [Arn92]; en pratique, dans le système MEC [ABC94], on peut construire explicitement la commutativité et l'associativité de la mise en parallèle, en respectant certaines contraintes sur les vecteurs de synchronisation.

Pour l'encapsulation, on utilise un prédicat $\mathcal{L}$ et une fonction de masquage $\mathcal{H}$. Notons $\mathcal{S}(P) = (Q, q_0, T)$ le système de transitions associé à $P$. Le système associé à $\overline{P^Y}$ est de la forme $(\overline{Q^Y}, \overline{q_0^Y}, T')$ où $\overline{Q^Y} = \{\overline{q^Y}, q \in Q\}$ et $T'$ est défini par :

$$ \frac{q \xrightarrow{L} q', \quad \mathcal{L}_Y(L)}{\overline{q^Y} \xrightarrow{\mathcal{H}_Y(L)} \overline{q'^Y}} \qquad [E] $$

$\mathcal{L}$ est le critère local. C'est un prédicat qui détermine quelles transitions du modèle de $P$ persistent dans le modèle du programme encapsulé. Ce prédicat ne porte que sur l'étiquette de la transition, indépendamment des autres transitions, d'où son nom de critère local. Une transition dont l'étiquette satisfait au critère est conservée; son étiquette est modifiée par la fonction $\mathcal{H}$ qui permet de cacher ce qui concerne le paramètre de l'encapsulation $Y$.

### 3.2.2 Equivalences, congruences et compositionnalité

Nous définissons une bisimulation paramétrée par une équivalence d'étiquettes notée $\mathcal{R}_L$. L'idée est de montrer que cette bisimulation est une congruence, pourvu que l'équivalence d'étiquettes soit une congruence pour les opérateurs qui portent sur les étiquettes, c'est-à-dire l'union de multi-ensembles $\mathcal{W}$ et l'opération de masquage $\mathcal{H}_Y$.

**Definition 3.1 : Bisimulation paramétrée**

Notons $(Q_1, q_{01}, T_1) \sim_L (Q_2, q_{02}, T_2)$ la bisimulation de deux systèmes de transitions, paramétrée par $\mathcal{R}_L$.

$$ (Q_1, q_{01}, T_1) \sim_L (Q_2, q_{02}, T_2) \text{ si et seulement si il existe une relation } \mathcal{R} \subseteq Q_1 \times Q_2 \text{ telle} $$
que :

$$ (q_{01}, q_{02}) \in \mathcal{R} \text{ et} $$

$$ (q_1, q_2) \in \mathcal{R} \implies \left\{ \begin{array}{rcl} q_1 \xrightarrow{L_1} q'_1 & \Rightarrow & \exists q'_2, L_2 \text{ t.q.} \quad \left\{ \begin{array}{l} q_2 \xrightarrow{L_2} q'_2 \\ (q'_1, q'_2) \in \mathcal{R} \\ \mathcal{R}_L(L_1, L_2) \end{array} \right. \\ q_2 \xrightarrow{L_2} q'_2 & \Rightarrow & \exists q'_1, L_1 \text{ t.q.} \quad \left\{ \begin{array}{l} q_1 \xrightarrow{L_1} q'_1 \\ (q'_1, q'_2) \in \mathcal{R} \\ \mathcal{R}_L(L_1, L_2) \end{array} \right. \end{array} \right. \quad \square $$

Cette définition induit une équivalence de programmes : $P_1 \equiv_L P_2 \iff S(P_1) \sim_L S(P_2)$. On peut alors prouver, par une simple induction sur la structure des programmes, que : *Si $\mathcal{R}_L$ preserve le prédicat $\mathcal{L}$ et est préservée par $\mathcal{H}_Y()$ et $\Psi$, alors $\equiv_L$ est une congruence.*

Le point intéressant de ce cadre de travail est qu'il permet d'étudier des congruences de programmes en se ramenant à l'étude de congruences d'étiquettes. D'autre part, une équivalence sur un ensemble $E$ peut être définie par l'intermédiaire d'une fonction $f$ non injective de $E$ vers $F$, en écrivant $e_1 \sim e_2 \iff f(e_1) = f(e_2)$. On se ramène donc à l'étude de telles fonctions non injectives, qu'on appelle des *abstractions*.

L'égalité d'étiquettes est la congruence la plus fine. La relation la plus intéressante est l'équivalence la plus grossière qui préserve le critère local et est préservée par les opérations sur les étiquettes. Toutefois il peut se révéler difficile de définir cette équivalence intéressante de manière constructive.

On peut essayer de l'atteindre par des affaiblissements de l'égalité, au moyen de fonctions d'abstraction $Ab$ :

$$ Ab : \text{ensemble d'étiquettes} \longrightarrow \text{ensemble d'étiquettes abstraites} \\ \mathcal{R}_L(L_1, L_2) \text{ si et seulement si } Ab(L_1) = Ab(L_2). $$

Une fois choisie une fonction d'abstraction, il reste à vérifier que l'équivalence correspondante est bien une congruence. Il est ensuite possible d'intégrer la fonction d'abstraction dans les règles de sémantique, en construisant directement les étiquettes abstraites (la congruence assure que les fonctions de test et les opérations de combinaison d'étiquettes ne s'appuient justement pas sur l'information éliminée lors de l'abstraction). On utilise alors une bisimulation classique, sans paramètre.

## 3.3 Applications

L'article présente comment exprimer trois calculs dans le cadre général défini plus haut.

### 3.3.1 Le calcul synchrone de Milner

Nous reprenons ici le cas du calcul synchrone de [Mil89]. Le calcul présenté en est une restriction au cas où les objets de base sont des automates.

Dans le calcul de [Mil89], les objets atomiques sont appelés *particules*. On utilise donc un ensemble de particules $\mathcal{P}ar = \{a, b, ...\}$. Un ensemble d'actions est défini comme un groupe commutatif $(\mathcal{A}ct, \times, -)$. 1 est l'action d'attente, $\times$ dénote l'occurrence simultanée de deux actions et la barre dénote la complémentation d'action : $a \times \bar{a} = 1$. L'ensemble des actions est
engendré par l'ensemble de particules. Une action peut toujours être mise sous la forme $a_1^{z_1}...a_n^{z_n}$, où les $a_i$ sont des particules distinctes, et les $z_i$ sont des entiers relatifs. L'opération de restriction notée $P \uparrow Y$ est paramétrée par un sous-groupe $Y$ de $\mathcal{A}ct$, et elle supprime toutes les transitions dont l'étiquette n'appartient pas à $Y$.

On plonge ce calcul dans le cadre général proposé ici en définissant les objets élémentaires comme l'ensemble des particules et complémentations de particules et les étiquettes comme des multi-ensembles d'objets de cette forme. L'opération binaire $\times$ de composition d'actions étant commutative et associative, on l'étend à un nombre quelconque d'arguments :

$$ \begin{align*} \otimes : \text{un multi-ensemble d'actions} &\mapsto \text{une action} \\ \otimes(\emptyset) &= 1 \\ \otimes(\{e\} \cup E) &= \otimes(E) \times e \end{align*} $$

Le critère local et la fonction de masquage sont définis par :

$$ \mathcal{L}_Y(L) = \otimes(L) \in Y, \quad \mathcal{H}_Y(L) = \otimes(L) $$

En abstrayant les étiquettes selon $Ab(L) = \otimes(L)$, on retrouve la sémantique usuelle du calcul de [Mil89]. En effet, une action peut être vue comme l'astraction d'un multi-ensemble de particules et complémentations de particules, en retenant seulement la différence entre le nombre de $a_i$ et le nombre de $\overline{a_i}$, pour chaque $a_i$.

### 3.3.2 Diffusion synchrone

L'ensemble des particules est l'ensemble des signaux d'entrée/sortie : $\mathcal{P}ar = \{a, b, c...\}$. Une réaction est de la forme $\alpha = \langle \alpha^+, \alpha^-, \alpha^o \rangle$, où $\alpha^+$, $\alpha^-$ et $\alpha^o$ sont des sous-ensembles de $\mathcal{P}ar$, pas nécessairement disjoints. $\alpha^+$, $\alpha^-$ donnent la condition d'entrée (le monôme dans lequel les éléments de $\alpha^+$ sont positifs et ceux de $\alpha^-$ négatifs), $\alpha^o$ donne l'ensemble des signaux émis. Les étiquettes sont des multi-ensembles de réactions.

Pour une étiquette $L$, on définit $I^+(L)$ (entrées positives), $I^-(L)$ (entrées négatives) et $O(L)$ (sorties) :

$$ I^+(L) = \bigcup_{\langle \alpha^+, \alpha^-, \alpha^o \rangle \in L} \alpha^+, \quad I^-(L) = \bigcup_{\langle \alpha^+, \alpha^-, \alpha^o \rangle \in L} \alpha^-, \quad O(L) = \bigcup_{\langle \alpha^+, \alpha^-, \alpha^o \rangle \in L} \alpha^o $$

L'opération d'encapsulation est définie en instanciant le critère $\mathcal{L}_Y(L)$ et la fonction $\mathcal{H}_Y(L)$ par :

$$ \begin{align*} \mathcal{L}_Y(L) &= (I^+(L) \cap Y \subseteq O(L) \wedge I^-(L) \cap Y \cap O(L) = \emptyset) \\ \mathcal{H}_Y(L) &= \{\alpha[Y], \alpha \in L\} \end{align*} $$

où $\alpha[Y]$ est la restriction de $\alpha$ aux signaux (particules) de $Y : \langle \alpha^+, \alpha^-, \alpha^o \rangle [Y] = \langle \alpha^+ - Y, \alpha^- - Y, \alpha^o - Y \rangle$.

Un rapide coup d'oeil aux définitions du critère local et de la fonction de masquage montre que les étiquettes peuvent être abstraites par la fonction :

$$ Ab(L) = (I^+(L), I^-(L), O(L)) $$

qui induit une congruence. On retrouve ainsi la sémantique présentée au chapitre 2, sans les aspects de détection des programmes incorrects.
### 3.3.3 Réactions en chaîne

On utilise les mêmes ensembles de particules et d'étiquettes que pour la diffusion synchrone décrite ci-dessus. Pour une étiquette $L$, on définit également $I^+(L)$, $I^-(L)$ et $O(L)$. Les réactions en chaîne diffèrent de la diffusion synchrone dans l'expression du critère local et de la fonction de masquage :

$$ 
\begin{align*}
\mathcal{L}_Y(L) &= (1) \quad (I^+(L) \cap Y \subseteq O(L) \land I^-(L) \cap Y \cap O(L) = \emptyset) \land \\
&\quad (2) \quad \exists f : L \longrightarrow [1, |L|], f \text{ bijective, telle que:} \\
&\qquad \forall n \in [1, |L|], I^+(f^{-1}(n)) \cap Y \subseteq \bigcup_{i=1}^{n-1} O(f^{-1}(i)) \\
\mathcal{H}_Y(L) &= \{ \alpha[Y], \alpha \in L \}
\end{align*}
$$

La condition (2) exprime que l'étiquette $L$ peut être totalement ordonnée (d'après la fonction de numérotation $f$) de telle manière que, dans toute réaction, les signaux supposés présents ont été effectivement émis par des réactions précédentes. Il faut donc commencer par des réactions qui sont rendues possibles en connaissant seulement le statut des signaux d'entrée.

On peut abstraire quelque peu les étiquettes, en remarquant que l'existence d'un ordre sur les diverses réactions qui composent une étiquette ne dépend pas de la partie négative des étiquettes. On écrit donc :

$$ Ab(L) = (I^{-}(L), \{ \langle \alpha^{+}, \emptyset, \alpha^{o} \rangle \mid \exists \alpha^{-} < \alpha^{+}, \alpha^{-}, \alpha^{o} \in L \}) $$

Il faut prouver que cette abstraction induit une congruence, c'est-à-dire que :

$$ Ab(L_1) = Ab(L_2) \implies \forall L, \forall Y, \begin{cases} Ab(L_1 \Psi L) = Ab(L_2 \Psi L) \\ Ab(\mathcal{H}_Y(L_1)) = Ab(\mathcal{H}_Y(L_2)) \\ \mathcal{L}_Y(L_1) = \mathcal{L}_Y(L_2) \end{cases} $$

Pour l'union de multi-ensembles et la fonction de masquage, c'est assez simple : la propriété vient de la distributivité de $I^+$, $I^-$ et $O$ sur les opérations d'union et de restriction. Le premier point de la définition du critère local est également simple à prouver. La difficulté vient du deuxième point : l'existence d'un ordre total sur les réactions qui composent une étiquette. C'est possible, toutefois, et on obtient donc une première abstraction.

Peut-on aller plus loin ? Cette première abstraction isole l'ensemble des signaux qui doivent être absents dans une étiquette, mais conserve toujours l'information maximale sur les autres. En particulier, on a encore une réaction par composant parallèle de base du programme. Or le mécanisme des réactions en chaîne induit une mise en parallèle *idempotente*. Une première simplification pourrait donc être de traiter des ensembles, et non des multi-ensembles. D'autre part, considérons une étiquette qui contient les deux réactions positives $(i^+, o_1)$ et $(i^+, o_2)$. En ce qui concerne l'existence d'un ordre, cette étiquette se comporte comme : $(i^+, o_1 \cup o_2)$. On peut imaginer quelques autres simplifications de ce style. On retrouve ici la suggestion d'Amir Pnueli d'axiomatiser l'équivalence d'étiquettes recherchée, en écrivant des axiomes du genre : $\{(i^+, o_1), (i^+, o_2)\} = \{(i^+, o_1 \cup o_2)\}$.

## 3.4 Commentaires et réflexions

### 3.4.1 Comparaison ARGOS/Statecharts

L'expression, dans notre cadre, du mode de communication des Statecharts, caractérisé par une notion de réaction en chaîne entre composants, fournit une version compositionnelle de la
sémantique présentée dans [PS88]. L'étude de quelques abstractions d'étiquettes permet d'autre part de mieux cerner la sémantique des réactions en chaîne. La proposition d'axiomatiser l'équivalence d'étiquettes est une réminiscence des discussions avec Amir Pnueli.

L'exemple du dialogue instantané illustre bien la différence entre les divers modes de communication d'ARGOS (la diffusion synchrone exposée au chapitre 2 et reprise ci-dessus) et des Statecharts (la version compositionnelle présentée ici).

**Exemple 3.1 : Dialogue instantané**

La figure 3.1 donne deux programmes ARGOS congruents qui représentent un dialogue instantané entre deux composants : en réaction à une cause extérieure *C*, le premier composant tente de changer d'état (de *A* à *B*), à condition que l'autre composant soit dans l'état *ON*. Pour cela, il émet la question *Q*, et ne change d'état que si le deuxième composant répond *Y*. La version (**a**) décrit le premier composant par deux systèmes. Dans la version (**b**), le premier composant est directement donné par un automate.

Les deux versions du premier composant sont congruentes, puisque la deuxième est la evrsion compilée de la première.

<figure><img src="image_16.png" /><figcaption>FIG. 3.1 – Deux versions du dialogue instantané</figcaption></figure>

Dans la sémantique des Statecharts présentée ci-dessus, le programme (**a**) a le comportement attendu, alors que le deuxième n'a pas de transition pour l'événement extérieur réduit au signal *C*. En effet, il est impossible de trouver une chaîne de transitions élémentaires des automates, pour expliquer une réaction globale de *X* vers *B*. □

Cet exemple conduit à s'interroger sur la notion de *causalité* adéquate pour ARGOS. La discussion apparaît au chapitre 9, paragraphe 9.6 qui propose un langage mixte ARGOS+ESTEREL.

## 3.4.2 Extensions du modèle

Nous proposons l'extension du modèle général au cas de plusieurs opérations de produit, éventuellement asymétriques, et la prise en compte d'équivalences de systèmes de transitions dans lesquelles les états peuvent également porter des informations pertinentes (et non plus seulement les transitions). La première de ces extensions permet de coder le raffinement d'ARGOS, sans remettre en cause l'expression de la diffusion synchrone entre composants ; la deuxième extension permet d'exprimer, par exemple, la détection des programmes causalement incorrects, puisqu'il
est possible d'associer à un état une information *globale* sur l'ensemble des transitions qui en sont issues.

Lors de la présentation de ce travail au groupe de travail sur les langages synchrones (Dagstuhl, novembre 1994), Albert Benveniste suggéra que la sémantique de Signal pouvait également être exprimée dans ce modèle, en utilisant des ordres partiels comme étiquettes de transitions.
# Chapitre 4

## Non déterminisme et langages synchrones

Source: *ce chapitre est tiré de [MH96], que nous joignons en annexe. Le détail des preuves n'est pas repris ici. Il me paraît préférable de consacrer ce chapitre à l'exposé des motivations et des problèmes posés.*

On fait souvent la publicité des langages synchrones en insistant sur le fait qu'ils ont réconcilié *concurrence* et *déterminisme*. Ils offrent une vue logique de la concurrence, comme notion de structuration de programmes, un mode de synchronisation puissant, et tout cela en garantissant que la composition d'objets déterministes donne un résultat également déterministe. C'est une caractéristique importante lorsque le but est de *programmer* des systèmes réactifs.

Cela peut toutefois donner l'impression que les langages synchrones sont condamnés au déterminisme. Or le déterminisme n'est pas toujours une propriété souhaitable. En particulier, si le langage est utilisé pour *spécifier* plutôt que pour *programmer*, une spécification abstraite nécessite en général des objets non déterministes. C'est un moyen simple de décrire un *ensemble* de comportements de manière concise.

Un des effets de bord de l'étude présentée ici est de montrer que les langages synchrones ne sont pas condamnés au déterminisme et peuvent, si on propose une extension raisonnable, être utilisés comme langages de spécification.

Une autre conséquence est la mise en évidence d'une distinction entre non déterminisme intrinsèque, maîtrisable, voulu par le programmeur, et non déterminisme apparaissant dans les résultats de compositions parallèles pour des raisons plus ou moins mystérieuses selon le degré de difficulté de la sémantique du langage. Les difficultés techniques rencontrées dans ce travail n'étant dues qu'au respect de cette distinction, nous commençons par motiver l'approche suivie et les choix effectués.

Enfin ce travail a conduit à s'interroger sur ce que représente le non déterminisme dans la description de systèmes informatiques, une fois admise l'idée que l'expression *programme non déterministe* constitue un oxymoron (c'est bien parce que les programmes sont toujours déterministes qu'il est si difficile de *programmer* un générateur aléatoire). Considérer que les programmes sont toujours déterministes n'est pas en contradiction avec l'existence de *spécifications* non déterministes, au sens propre du terme, c'est-à-dire *insuffisamment déterminées*. La sémantique collatérale des opérateurs booléens dans ADA par exemple, qui constitue une spécification du compilateur, est bien non déterministe, puisqu'elle ne détermine pas l'ordre dans lequel doivent
être évalués les opérandes. Les compilateurs ADA et les codes compilés sont toujours déterministes sur ce point, au moins pour des programmes séquentiels (pour les programmes parallèles, le non déterminisme apparent — c'est-à-dire la non reproductibilité des exécutions — est dû à une connaissance incomplète du système à l'exécution, et c'est précisément cet inconvénient que les langages synchrones se sont attachés à résoudre).

Techniquement, nous recherchons une équivalence des machines de Mealy booléennes non déterministes, compatible avec l'idée selon laquelle un objet non déterministe représente un ensemble d'objets déterministes.

## 4.1 Motivations

Les motivations sont de deux ordres. Elles visent à résoudre aussi bien les problèmes dans les cas où : 1) le but est de décrire des objets non déterministes (par exemple parce qu'ils représentent de manière concise l'ensemble des comportements de l'environnement du système) ; 2) le but est de décrire des objets déterministes, mais dont l'abstraction (par exemple booléenne) manipulable par les algorithmes et outils associés au langage est, elle, non déterministe.

Le deuxième cas est apparu lorsque nous avons voulu décorer les transitions des automates de programmes ARGOS par des informations sur des variables continues, afin de décrire des systèmes temporisés ou hybrides (cf. pour plus de détails les chapitres 10 et 11).

Nous détaillons tout d'abord les deux types de cas à résoudre.

### 4.1.1 Représentation d'un ensemble de comportements modélisation de l'environnement

Dans la spécification des protocoles de communication, un cas typique d'utilisation du non déterminisme est constitué par la modélisation d'une ligne de transmission non fiable, qui peut transmettre les messages correctement, les perdre ou les réordonner...

Lorsqu'on introduit dans le système un composant non déterministe pour représenter la ligne de transmission, il s'agit bien de représenter de manière concise tout l'ensemble infini des comportements possibles de la ligne qui, à chaque transmission de message, "choisit" arbitrairement de transmettre correctement, perdre ou réordonner les messages. Lorsqu'on prouve des propriétés de fonctionnement du protocole pour un tel système, on a bien prouvé quelque chose, globalement, pour tous les comportements possibles de la ligne.

Ce cas de figure se présente couramment dès qu'il est nécessaire d'intégrer une description de l'environnement d'un système, aux fins de vérification de propriétés de fonctionnement de l'ensemble. Savoir si l'environnement à décrire peut ou non être représenté par un processus complètement déterministe, pour peu que l'on connaisse les lois physiques appropriées et les conditions initiales, constitue un problème philosophique certes intéressant, mais dont l'étude dépasse le cadre de ce document et les compétences de son auteur. Quoi qu'il en soit, la modélisation détaillée et déterministe du comportement d'un environnement physique est, d'une part hors de portée de moyens informatiques, d'autre part, on l'espère, inutile. On se contente donc d'une abstraction maîtrisable, en général non déterministe, ce qui rejoint, en quelque sorte, le deuxième cas.
<figure><img src="image_17.png" /><figcaption>FIG. 4.1 – Déterminisation par un signal auxiliaire $\omega$</figcaption></figure>

### 4.1.2 Abstraction d'un comportement déterministe

Le deuxième cas courant d'apparition d'objets non déterministes est plus "technique". Il est dû aux limitations des algorithmes et outils associés au langage. On veut par exemple décrire un comportement intrinsèquement déterministe, mais pour lequel le déterminisme est assuré par des informations non traitées par le compilateur. Ces informations ne sont toutefois pas inutiles. Elles peuvent être transmises à un outil plus puissant qui saura les analyser.

C'est le cas rencontré dans le couplage ARGOS+POLKA.

**Exemple 4.1 : Traitement du non déterminisme dans ARGOS+POLKA**

L'automate ci-dessous décrit le comportement global d'un passage à niveau. Les états sont des triplets d'états des trois composants : le train, qui peut être dans la zone protégée par la barrière du passage à niveau ou en dehors (out, approach, on gate); la barrière, qui peut être ouverte, fermée ou en mouvement (open, closed, moving down, moving up); la section de voie du passage à niveau, qui peut être occupée ou libre (occupied, free). La variable $\alpha$ décrit l'angle que fait la barrière avec le sol, en degrés.

Cet automate peut être obtenu par compilation d'un programme ARGOS à trois composants parallèles, après élimination des transitions non tirables par l'outil POLKA. Cette méthode fait l'objet du chapitre 11, où nous décrivons cet exemple en détail.

Considérons ici que l'automate est décrit directement. Un cas de non déterminisme apparent est dû aux transitions déclenchées par le signal *enter* (le train entre dans la zone protégée, et émet ce signal en passant une pédale sur la voie), à partir de l'état global *out/moving_up/free*. En effet, la réaction dépend de l'état de la barrière à ce moment-là, c'est-à-dire de la valeur de l'angle $\alpha$. On trouve donc les deux conditions $\alpha = 90 \land enter$ et $\alpha \neq 90 \land enter$.

☐

On résout le problème en ajoutant un signal $\omega$ qui permet d'écrire deux conditions booléennes disjointes : $enter \land \omega$ et $enter \land \neg \omega$.
<figure><img src="image_18.png" /><figcaption>FIG. 4.2 – *Introduction d'oracles — cas simple*</figcaption></figure>

### 4.1.3 La technique des oracles

La communauté des utilisateurs de langages synchrones n'ayant pas attendu cette étude pour utiliser ces langages comme des langages de spécification, il existe depuis longtemps une astuce très simple pour représenter le non déterminisme dans un langage synchrone.

Puisque l'on décrit naturellement des systèmes à entrées/sorties, il suffit d'introduire des entrées supplémentaires, que l'on baptise *oracles*, ce qui déplace le non déterminisme à l'extérieur du système, en en rendant responsable une entité douée de la capacité de choisir, que nous appellerons par la suite *démon*<fnref n="1" />.

Nous illustrons tout d'abord par des exemples en ARGOS la technique d'introduction des oracles et les problèmes qui se posent.

**Exemple 4.2**

Dans l'exemple donné Figure 4.2, un seul cas de non déterminisme apparaît, et il est en outre binaire. L'introduction d'une entrée oracle $d_1$ suffit à résoudre le non déterminisme.

☐

La situation se complique si les cas de non déterminisme ne sont plus binaires, mais par exemple ternaires. Il faut alors introduire plusieurs oracles booléens.

**Exemple 4.3**

Dans l'exemple donné Figure 4.3, un cas de non déterminisme ternaire apparaît. On introduit deux oracles $d_1$ et $d_2$.

(c) constitue une solution correcte, alors que (b) est incorrecte. En effet, en introduisant les conditions $d_1 \wedge d_2$, $d_1 \wedge \neg d_2$ et $\neg d_1 \wedge d_2$, on a transformé un système réactif non déterministe en système déterministe mais *non réactif*.

☐

**Exemple 4.4**

<footnote n="1">1. Le choix du terme “démon” est discutable. La communauté de recherche sur les spécifications relationnelles utilise les termes de non-déterminisme “angélique” ou “démoniaque” selon que l’entité extérieure qui résoud les choix non déterministes a tendance à favoriser, ou au contraire à contrarier, la réalisation des propriétés attendues. Cette distinction n’a toutefois pas de sens dans notre contexte. Il fallait donc choisir entre ange et démon...</footnote>
<figure><img src="image_19.png" /><figcaption>FIG. 4.3 – *Introduction d’oracles — cas de non déterminisme ternaire*</figcaption></figure>
<figure><img src="image_20.png" /><figcaption>FIG. 4.4 – *Introduction d'oracles — interférence avec les constructions du langage*</figcaption></figure>

Dans l'exemple donné Figure 4.4, on montre un mauvais choix pour l'introduction d'oracles dans un système parallèle dont les deux composants présentent des cas de non déterminisme binaires.

Utiliser le même oracle pour résoudre les cas de non déterminisme dans les deux composants parallèles revient à imposer une synchronisation entre ces composants : dans le mode de communication par diffusion synchrone, les composants parallèles sont implicitement synchronisés sur leurs entrées communes. Dans le système déterminisé, la configuration d'états $A'B''$ est inaccessible depuis $AB$, puisqu'il faudrait exécuter simultanément une transition où $d_1$ est vrai, et une transition où il est faux. On se convainc facilement que toute composition parallèle impose l'utilisation de deux ensembles d'oracles disjoints. □

## 4.2 Formalisation de la technique des oracles

### 4.2.1 Schéma de principe et propriétés recherchées

Quelle que soit la motivation pour l'introduction d'entrées oracles dans un programme, on peut procéder de manière structurelle. Les composants parallèles peuvent être déterminisés indépendamment les uns des autres, pour peu que l'on choisisse des ensembles d'oracles disjoints. L'opération de raffinement permet une réutilisation partielle des entrées oracles puisque les périodes d'activation des différents comportements contrôlés sont par définition disjointes.

Une fois les oracles introduits dans les composants du programme, il est possible d'appliquer la sémantique usuelle des programmes déterministes. En particulier, on sait détecter, pour les rejeter, les constructions qui produisent des systèmes non déterministes ou non réactifs. Pour un programme correct, on obtient une machine de Mealy booléenne déterministe, dans laquelle apparaissent encore les entrées oracles. Il suffit alors de les "effacer", pour ré-obtenir un objet non déterministe. Cette transformation en trois étapes peut constituer la sémantique d'un langage acceptant le non déterminisme dans les composants élémentaires.

Les exigences naturelles associées à ce schéma sont les suivantes :

- La sémantique en trois étapes ainsi définie ne devrait pas dépendre de la manière d'introduire les oracles. Autrement dit, quelle que soit la manière choisie pour introduire les
oracles lors de la phase 2, on devrait obtenir en bout de chaîne des machines comparables
(égales, isomorphes, ...?)

- Il devrait exister, sur les machines non déterministes, une relation d'équivalence constituant une congruence pour les opérateurs du langage.

4.2.2 Les machines contrôlées
condition de séparation et résultat

Pour formaliser cette sémantique en trois étapes, on définit la notion de machine de Mealy
booléenne contrôlée, dans laquelle les transitions portent des conditions de la forme $b_i \wedge b_o$.
$b_i$ représente la condition d'origine associée à la transition, et porte sur les véritables signaux
d'entrée du système à décrire. $b_o$ est une formule booléenne construite à l'aide de signaux oracles,
introduite pour déterminiser la machine.

On décrit comment transformer tout programme ARGOS en programme dont les composants
de base sont des machines contrôlées. Il faut déterminiser séparément les composants de base, en
respectant quelques contraintes sur les ensembles de signaux oracles utilisés, comme cela a par-
tiellement illustré par les exemples (des ensembles disjoints pour des composants parallèles, etc).
La condition de séparation est une condition suffisante sur les formules booléennes introduites
lors de la déterminisation d'un automate, qui garantit en particulier que la machine contrôlée
obtenue est toujours réactive.

On prouve également que toutes les méthodes d'introduction des oracles qui respectent la
condition de séparation garantissent des automates isomorphes en fin de chaîne (déterminisation
– sémantique usuelle – effacement des oracles). Enfin, sous cette condition de séparation, on
prouve que la bisimulation est une congruence pour les opérations d'ARGOS.

4.3 Recherche d'une autre relation d'équivalence

On a donc montré que la bisimulation est une congruence pour cette nouvelle sémantique en
trois étapes. Ce résultat n'est qu'à moitié satisfaisant. Techniquement, exhiber une congruence
est un minimum, pour justifier la sémantique. Il est heureux que la bisimulation convienne :
c'est une relation bien connue, largement utilisée en association avec les algèbres de processus,
et la comparaison (inclusion dans un sens ou dans l'autre) avec d'autres relations a été étudiée
intensivement.

D'un point de vue plus philosophique, la seule relation de comparaison des systèmes non
déterministes qui nous donnerait réellement satisfaction est définie, de manière tout à fait infor-
melle, par : *un objet non déterministe représente un ensemble de comportements déterministes,
et deux objets doivent être considérés comme équivalents s'ils représentent le même ensemble de
comportements déterministes*. Puisque c'est l'interprétation du non déterminisme que nous avions
en tête, on devrait pouvoir espérer que tout, dans la formalisation, est fait pour garantir que
cette relation est une congruence. Toutefois nous avons rencontré dans la formalisation de cette
sémantique des difficultés techniques inattendues, et il serait bon de pouvoir définir formelle-
ment cette nouvelle relation d'équivalence afin de prouver qu'elle constitue bien une congruence.
Il n'est pas complètement exclu que cette conjecture soit fausse, d'ailleurs.

Cette interprétation du non déterminisme semble fort naturelle dans toute une communauté
travaillant sur les spécifications non déterministes de systèmes parallèles, ainsi que l'atteste Man-
fred Broy. De même, un programme Prolog est dit non déterministe lorsqu'il peut produire
<figure><img src="image_21.png" /><figcaption>FIG. 4.5 – Objets non déterministes et ensembles de comportements déterministes associés, dans le cas fini</figcaption></figure>

un ensemble de solutions (fourni en extension, ou décrit symboliquement par un ensemble de contraintes). En revanche, tous les spécialistes de la sphère “algèbres de processus” consultés jusque là avouent ne pas avoir rencontré de définition formelle d’une équivalence basée sur cette idée.

### 4.3.1 Définition d'une relation d'équivalence

Nous pouvons tenter de préciser quelque peu la définition informelle ci-dessus, avant de partir à la recherche d'exemples et de contre-exemples pour comparer notre relation d'équivalence avec des relations connues.

On observe facilement sur quelques exemples ce que peut être *l'ensemble de comportements déterministes décrit par un objet non déterministe*. Ce n'est pas un ensemble de comportements linéaires, ou traces — auquel cas l'équivalence cherchée serait simplement l'équivalence de trace — puisque les comportements d'entrée/sortie déterministes vis-à-vis des entrées peuvent présenter des branchements sur ces entrées. La figure 4.5 donne un exemple fini. (a) est un objet non déterministe qui représente l'ensemble { (b), (c) }.

La situation se complique lorsque l'objet non déterministe comporte des boucles. En effet, l'ensemble de comportements déterministes associé est alors, dans le cas général, un ensemble *infini* de comportements déterministes à nombre *infini* d'états. Il suffit pour cela de placer un choix non déterministe dans une boucle. La situation semble maîtrisable puisqu'on dispose, par définition, d'une représentation concise et même finie de cet ensemble, mais il paraît pour l'instant difficile de définir l'équivalence recherchée directement.

Notons $ND^1$ et $ND^2$ des automates non déterministes et $E^1 = \{d_0^1, d_1^1, ...\}$, $E^2 = \{d_0^2, d_1^2, ...\}$ les ensembles potentiellement infinis — mais certainement dénombrables — des comportements déterministes associés. On dira que $ND^1$ et $ND^2$ sont équivalents par la relation cherchée notée $\equiv$ si et seulement si les ensembles $E^1$ et $E^2$ sont égaux modulo une équivalence de comportements déterministes, par exemple l'équivalence de traces notée $\sim$. Ainsi :

$$ (ND^1 \equiv ND^2) \iff \begin{cases} \forall d_k^1 \in E^1, \exists d_j^2 \in E^2, d_k^1 \sim d_j^2 \\ \forall d_k^2 \in E^2, \exists d_j^1 \in E^1, d_k^2 \sim d_j^1 \end{cases} $$
<figure><img src="image_22.png" /><figcaption>FIG. 4.6 – Exemple prouvant que la relation recherchée n'est pas l'équivalence de trace</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>FIG. 4.7 – Exemple prouvant que la relation recherchée n'est pas la bisimulation</figcaption></figure>

## 4.3.2 Essai de comparaison avec des relations d'équivalence connues

### Exemple 4.5 : Ce n'est pas l'équivalence de trace

Les deux systèmes de transitions (**a**) et (**b**) de la figure 4.6 sont équivalents par l'équivalence de trace. Le premier, étant déterministe, représente un ensemble de comportements déterministes réduit à lui-même. Le second représente l'ensemble de comportements (**c**) et (**d**).

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

### Exemple 4.6 : Ce n'est pas la bisimulation

Les deux systèmes de transitions non déterministes (**a**) et (**b**) de la figure 4.7 ne sont pas bisimilaires, et pourtant ils représentent tous deux le même ensemble de comportements déterministes, à savoir les comportements (**c**) et (**d**) de la figure.

<figure><img src="image_25.png" /></figure>
<figure><img src="image_26.png" /><figcaption>FIG. 4.8 – Exemple prouvant que la relation recherchée n'est pas l'équivalence d'acceptation</figcaption></figure>

**Exemple 4.7 : Ce n'est pas l'équivalence d'acceptation**

Les automates (a) et (b) sont équivalents par l'équivalence d'acceptation, mais ils ne représentent pas les mêmes ensembles de comportements déterministes. En effet, (a) représente l'ensemble (c), et (b) représente l'ensemble (d). □

## 4.4 Application à d'autres langages synchrones,
autres applications de la technique des oracles

L'introduction annonçait que les résultats de ce travail permettent de ne plus considérer les langages synchrones comme étant voués au déterminisme. L'exposé est centré sur ARGOS, où le non déterminisme intrinsèquement voulu par le programmeur apparaît très naturellement dans les automates de base du programme.

Appliquer la démarche à un autre langage synchrone exige que l'on décide préalablement de l'introduction d'un brin de non déterminisme dans les programmes. Selon les structures proposées par le langage, ce n'est pas forcément évident.

Pour LUSTRE, N. Halbwachs propose l'introduction de variables locales non définies par des équations. En effet, jusque là, la modélisation du non déterminisme est réalisée en introduisant des entrées oracles au plus haut niveau du programme, qui doivent être passées en paramètres de tous les noeuds internes, jusqu'au noeud où elles jouent effectivement le rôle d'oracles. Disposer de variables locales non définies par des équations permet de ne mentionner ces oracles qu'à l'endroit où ils sont utilisés. Il reste à la charge du compilateur de les traiter comme des entrées.
Enfin la technique des oracles peut être utilisée dès que l'on doit simuler ou coder le non déterminisme dans un contexte prévu à l'origine pour traiter le cas déterministe. Considérons par exemple le codage des comportements de systèmes réactifs par des BDD. Il est connu que les fonctions sont représentées et manipulées de manière bien plus efficace que les relations. Or, si les transitions d'un système sont données par des fonctions et non par des relations, c'est que le système est déterministe. Pour coder efficacement des systèmes non déterministes (par exemple la relation de transition inverse d'un système déterministe, souvent utilisée dans les algorithmes de vérification dits "en arrière") il suffit d'introduire des oracles, comme proposé par Pascal Raymond.
# Chapitre 5

## Sémantique d'Argos en équations
booléennes

Sources: *Le codage d'ARGOS en équations booléennes, tel que présenté ici, est publicé dans [MH96a]. Toutefois les idées suivies avaient déjà été utilisées pour le codage d'ARGOS en LUSTRE présenté dans la thèse de Muriel Jourdan [Jou94], ou dans [JLMR93, JLMR94], à propos de programmation multi-langages. D'autre part l'analyse de déterminisme et réactivité présentée dans [HM95] a été expérimentée grâce à un codage d'ARGOS en équations booléennes au format d'entrée de l'outil BAC (Boolean Automaton Checker) développé par N. Halbwachs.*

La sémantique des constructions d'ARGOS présentée au chapitre 2 ne peut guère servir de
technique de compilation. La taille de l'automate plat obtenu par composition des automates de
base d'un programme est naturellement une fonction exponentielle de la taille du programme, du
fait des compositions parallèles interprétées comme des produits cartésiens. D'autre part, même
si la taille de l'objet final n'est pas prohibitive, la taille des objets intermédiaires peut l'être.

Enfin, pour appliquer une opération d'encapsulation, on doit résoudre un système d'équations
booléennes dont les variables sont les signaux locaux, et cela pour chaque état, et pour chaque
configuration possible des signaux d'entrée !

Le tout premier compilateur ARGOS résolvait ces systèmes par essai exhaustif de toutes les
configurations de valeurs de variables (cela ne relevait toutefois pas d'un choix délibéré, mais d'une
compréhension encore incomplète des relations entre diffusion synchrone et systèmes d'équa-
tions). Dans le second compilateur développé par Muriel Jourdan, la résolution des systèmes
était réalisée grâce à un codage en BDD, la production de l'ensemble des états étant toujours
réalisée de manière explicite par un parcours en avant (la technique est décrite dans [MV92b]).

L'étape suivante est le codage complet des programmes ARGOS en systèmes d'équations,
pour permettre un calcul symbolique. Cela demande une refonte complète de la technique de
compilation, mais c'est une évolution indispensable. Ce codage en équations a été utilisé tout
d'abord pour réaliser une détection symbolique des cas de non déterminisme ou non réactivité,
dans [HM95]. La technique utilisée ne conduit pas directement à la génération de code. Il s'agissait
plutôt d'expérimenter les algorithmes BDD, et de comparer la notion de correction obtenue avec
les notions dites "de causalité" définies par G. Berry pour ESTEREL, ou connues dans le domaine
des circuits séquentiels (voir [Mal93] par exemple).

Le format DC [CS95], qui constitue l'un des formats communs de la plate-forme synchrone,
permet de décrire les systèmes réactifs par des ensembles d'équations, dans le style de LUSTRE.
Toutefois, LUSTRE propose une notion générale d'horloge, alors que DC se contente d'une notion de condition d'activation. L'exécution d'un programme DC peut être vue comme l'évaluation répétée d'un ensemble d'affectations parallèles (définies par les équations). Il est possible, grâce aux conditions d'activation, de spécifier qu'il n'est pas nécessaire d'évaluer une certaine équation à tous les cycles. L'opération de composition hiérarchique d'ARGOS constitue précisément un moyen de spécifier que certaines parties du programme peuvent ne pas toujours être actives, au cours de l'exécution. Il est donc particulièrement intéressant de traduire ARGOS en DC, en essayant d'utiliser au mieux ces conditions d'activation.

# 5.1 Argos vers DC

## 5.1.1 un sous-ensemble du format DC

EQU(i, b, a) définit un flot i, comme étant égal au résultat de l'évaluation de l'expression booléenne b, mis à jour lorsque a est vrai :

$$i_0 = \begin{cases} b_0 \text{ si } a_0 \\ v \text{ sinon} \end{cases}, \quad i_n = \begin{cases} b_n \text{ si } a_n \\ i_{n-1} \text{ sinon} \end{cases} \quad \text{Quand } n > 0$$

La valeur initiale v utilisée dans la définition devrait apparaître en paramètre d'une définition. Toutefois cette valeur ne sert que lorsque la condition d'activation est fausse à l'instant initial. Dans la traduction d'ARGOS en DC, un flot défini par un EQU, et dont la condition d'activation est fausse à l'instant initial, n'est en fait utilisé nulle-part à cet instant. Les valeurs initiales des EQU sont donc non pertinentes.

MEM(i, b, a, v) définit un flot i comme la mémorisation du flot calculé par l'expression booléenne b, mise à jour lorsque a est vrai. La valeur initiale de i est donnée par v.

$$i_0 = v, \quad i_{n+1} = \begin{cases} b_n \text{ si } a_n \\ i_n \text{ sinon} \end{cases}$$

La figure 5.1 illustre les deux types de définitions. Les définitions de type MEM reproduisent leur entrée avec un décalage d'un instant. Les définitions de type EQU reproduisent leur entrée instantanément.

## 5.1.2 Utilisation des deux types de définitions :
### Codage des machines de Mealy

Le codage des machines de Mealy en définitions de type MEM ou EQU est réalisé en décidant d'utiliser une variable de flot booléen par signal, et une variable par état. On pourrait bien sûr optimiser le nombre de variables d'état par un codage en log, mais c'est alors le codage des transitions qui devient complexe. D'autre part les machines de Mealy qui interviennent comme composants de base des programmes ARGOS n'ont en général que peu d'états. Pour une dizaine d'états, il semble peu intéressant de compliquer la fonction de transition par un codage en log des états, qui ne représente qu'une petite économie de variables d'états. Une réutilisation partielle des variables d'état, guidée par la structure du programme ARGOS, est un objectif bien plus intéressant (voir plus loin le paragraphe 5.1.6).

La figure 5.2 donne un exemple de machine (a), les chronogrammes correspondants (b) et la correspondance entre instants du chronogramme et transitions exécutées (c). Pour cet exemple, les définitions sont :
<figure><img src="image_27.png" /><figcaption>FIG. 5.1 – Exemples de définitions DC et chronogrammes correspondants</figcaption></figure>

MEM($A$, $A \wedge \neg a \lor B \wedge a$, TRUE, TRUE)
MEM($B$, $B \wedge \neg a \lor A \wedge a$, TRUE, FALSE)

EQU($b$, $A \wedge a$, TRUE)
EQU($c$, $A \wedge \neg a$, TRUE)

Si une machine de Mealy est considérée comme constituant un programme, les conditions d'activation doivent être toujours vraies : considérons une machine ($S$, $s_0$, $I$, $O$, $T$). Pour chaque état $s \in S$ on définit un flot local $s$ par : MEM($s$, $rp$, TRUE, initv) où

$$rp = \left[ \left( s \wedge \neg \bigvee_{(s,b,-,\neg) \in T} b \right) \vee \left( \bigvee_{(s',b,-,s) \in T} (s' \wedge b) \right) \right]$$

De plus, si l'état est initial (c'est-à-dire $s = s_0$), initv = TRUE, sinon initv = FALSE. Pour chaque signal de sortie $o \in O$, on définit un flot local $o$ par : EQU($o$, $rp$, TRUE) où

$$rp = \left[ \bigvee_{(s,b,O \ni o, \neg) \in T} (s \wedge b) \right]$$

### 5.1.3 Codage des programmes structurés

Le codage des programmes structurés est guidé par la syntaxe : l'ensemble de définitions d'un programme $P_1 \parallel P_2$ est construit à partir des ensembles de définitions obtenus pour $P_1$ et $P_2$ indépendamment. Le codage complet est fourni dans [MH96a]. J'expose ci-dessous les principales difficultés et les idées de solution.

**Composition parallèle et émetteurs multiples d'un signal.** Lorsque deux composants parallèles émettent le même signal $o$, on obtient deux ensembles de définitions non disjoints, au sens où leur union contient deux définitions du même flot. Dans le format DC, comme en LUSTRE, chaque flot est défini par une seule équation. L'interprétation correcte de la sémantique
<figure><img src="image_28.png" /><figcaption>FIG. 5.2 – Codage des machines de Mealy, exemple</figcaption></figure>

d'ARGOS consiste à fusionner les deux définitions en prenant la disjonction de leurs parties droites. (En ESTEREL, où les signaux peuvent porter des valeurs de types quelconques, une émission multiple s'accompagne de la combinaison des valeurs associées, par une opération commutative et associative.)

**Codage du raffinement, les difficultés.** La difficulté majeure provient du codage du raffinement. D'une part, c'est une bonne idée d'utiliser les opérations de raffinement comme des indications permettant de restreindre les conditions d'activation des différents flots calculés : typiquement, il est inutile de calculer les flots d'états d'un processus qui raffine un état non actif. D'autre part, une application brutale de ce principe conduit à une traduction fausse. D'une certaine manière, les flots définissant les signaux doivent être calculés à tout instant. Enfin il faut garantir la réinitialisation des processus raffinants ; il ne suffit pas d'inhiber le calcul des variables d'états d'un processus non actif, il faut également garantir que le processus redémarre dans son état initial, s'il est tué puis relancé.

Tous ces points sont garantis par un codage *sous contexte* des expressions de programmes ARGOS. Chaque sous-arbre est codé en tenant compte de deux paramètres hérités notés KILL et ALIVE, qui signifient respectivement : *le processus représenté par ce sous-arbre est tué durant la réaction courante* ; *le processus participe à la réaction courante*.

Les paramètres sont définis a priori pour le programme principal, c'est-à-dire la racine de l'arbre abstrait : KILL = FALSE, puisque le programme principal n'est jamais tué, et ALIVE = TRUE, puisqu'il participe à toutes les réactions. On définit comment ces paramètres sont passés d'un noeud à ses fils, et comment les feuilles (les machines de Mealy qui contrôlent les raffinements) sont codés en fonction de ces paramètres hérités.

**Codage des machines de Mealy sous contexte.** L'idée de base du codage est de maintenir l'invariant : toute machine appartenant à un processus non actif est mise dans son état initial. C'était le principe de base des premières sémantiques opérationnelles d'ARGOS, qui garantissait la production de systèmes de transitions minimaux selon un certain critère [Mar90]. Pour garantir cet invariant, les machines appartenant à un processus sont remises à leur état initial lorsque ce
processus est tué.

On obtient donc, pour un état $s$, la définition $\text{MEM}(s, rp, \text{Alive}, \text{initv})$, dans laquelle :

$$rp = \left[ \left( s \wedge \neg \bigvee_{(s,b,-,\neg) \in T} b \right) \vee \bigvee_{(s',b,-,s) \in T} (s' \wedge b) \right] \begin{cases} \vee \text{Kill} & \text{si } s \text{ est initial} \\ \wedge \neg \text{Kill} & \text{sinon} \end{cases}$$

Comme auparavant, $\text{initv} = \text{TRUE}$ si $s$ est initial, sinon $\text{initv} = \text{FALSE}$.

Pour un signal $o$, la seule modification concerne la condition d'activation : $\text{EQU}(o, rp, \text{Alive})$.

**Codage du raffinement.** Le codage faux contre lequel il faut se prémunir est le suivant : si l'on ne calcule pas les sorties d'un processus $P$ lorsque $P$ est inactif, on obtient un comportement erroné des signaux émis par $P$. En effet, si un signal $o$ doit être émis lors de la réaction qui tue $P$, la valeur de son flot associé est calculée, mise à vrai, et restera vraie pendant que $P$ est inactif.

La solution choisie consiste à associer à chaque signal deux flots, calculés à des niveaux différents : $P$ calcule une version partielle du signal $o$, notée $o'$, et ceci peut être fait avec comme condition d'activation une expression définissant les instants d'activité de $P$; dans le contexte englobant (qui définit les instants d'activation de $P$), on calcule $o$ par $\text{EQU}(o, a \wedge o', x)$, où $x$ est la condition d'activation du contexte.

### 5.1.4 Exemple

<figure><img src="image_29.png" /><figcaption>FIG. 5.3 – *Un programme simple à coder en DC*</figcaption></figure>
Les définitions correspondantes :

MEM(Running, Running ∧ ¬Stop ∨ Idle ∧ Start, TRUE, FALSE)

MEM(Idle, Idle ∧ ¬Start ∨ Running ∧ Stop, TRUE, TRUE)

MEM(s₁, s₁ ∧ ¬a ∨ s₂ ∧ a ∨ Stop, Running, TRUE)

MEM(s₂, s₂ ∧ ¬a ∨ s₁ ∧ a, Running, FALSE)

MEM(s₃, s₃ ∧ ¬ℓ' ∨ s₄ ∧ ℓ' ∨ Stop, Running, TRUE)

MEM(s₄, s₄ ∧ ¬ℓ' ∨ s₃ ∧ ℓ', Running, FALSE)

EQU(ℓ', s₂ ∧ a, Running)

EQU(A', s₄ ∧ ℓ', Running)

EQU(ℓ, Running ∧ ℓ', TRUE)

EQU(A, Running ∧ A', TRUE)

### 5.1.5 Propriété de cohérence

La sémantique opérationnelle décrite au chapitre 2 donne une machine de Mealy (S, s₀, Iₐ, Oₐ, T). La nouvelle sémantique définie ici donne un programme DC sous la forme (Iₐ, Oₐ, L, D) (Iₐ et Oₐ sont les ensembles de flots d'entrée et de sortie, L est l'ensemble des flots locaux, et D est l'ensemble des définitions). Il faut trouver un dénominateur commun à ces deux objets afin de les comparer.

<figure><img src="image_30.png" /><figcaption>FIG. 5.4 – Propriété de cohérence des deux sémantiques</figcaption></figure>

On les considère tous deux comme des générateurs d'ensembles de traces d'entrés/sortie, c'est-à-dire des suites de fonctions de $I \cup O$ vers les booléens. Il est facile de se convaincre, en effet, que les deux objets sémantiques s'accordent sur la notion d'entrée/sortie, et donc $I = Iₐ = Iₐ$ et, de même, $O = Oₐ = Oₐ$. Il faut donc prouver $\forall E \in \mathcal{E} \ T_a(S(E)) = T_d(D(E))$.

On prouve plus facilement une propriété plus forte, selon laquelle ce sont en fait les traces d'entrées/sorties/états qui coïncident. Il suffit d'établir la correspondance entre les états S de la machine de Mealy et les flots définis par des MEM dans le programme DC (en tenant compte des flots dont la valeur n'est pas pertinente à un instant donné parce qu'ils appartiennent à des
processus non actifs). On retrouve ce type de raisonnement pour prouver l'équivalence de deux sémantiques dans l'article sur l'extension temporelle d'ARGOS [JMO93].

### 5.1.6 Complexité de la traduction

La taille du programme DC obtenu est linéaire par rapport à la taille du programme ARGOS de départ.

**Retour sur le codage des états** Nous avons décrit une technique de codage qui alloue un ensemble de variables pour chaque machine de Mealy composant de base. La structure de raffinement conduit naturellement à envisager une réutilisation partielle des variables d'état, guidée par la structure du programme. D. Drusinsky [DY90] a proposé un algorithme de synthèse de circuit à partir d'un Statechart, en identifiant des ensembles les plus larges possible d'états élémentaires dits *exclusifs*, pour lesquels on peut choisir un codage en log. Cette technique n'a d'intérêt que si les ensembles considérés ne sont pas limités aux ensembles d'états des machines de Mealy de base, et pour les élargir il faut tenir compte de la structure du programme.

Faut-il pour autant compliquer l'algorithme de codage — au risque d'y introduire des erreurs, ou du moins de le rendre difficilement prouvable —, ou s'en remettre à l'application a posteriori d'un algorithme d'élimination de variables du style de ceux utilisés dans les outils de conception de circuits ? Cette dernière approche est celle d'ESTEREL. Des algorithmes spécifiques ont toutefois été étudiés, capables de réaliser une réduction conséquente pour la classe de circuits obtenus comme traduction de programme ESTEREL.

Dans le cas d'ARGOS, des expériences restent à faire pour déterminer l'efficacité des algorithmes existants sur les circuits produits. Il est possible que l'idée de placer les sous-programmes inactifs dans leur état initial ait pour effet de dissimuler l'exclusivité de certaines variables d'état, et donc d'interdire une réduction sensible. L'idéal serait un algorithme d'élimination de variables dans un circuit booléen, capable de tenir compte d'un ensemble de contraintes d'exclusivité fourni par le compilateur ARGOS.

## 5.2 Analyse de déterminisme et réactivité
sur la forme équationnelle

Dans [MH96a], nous avons délibérément omis l'aspect de détection des programmes incorrects (non déterministes ou non réactifs). Pour que la traduction en DC proposée ici fournisse une nouvelle méthode de compilation d'ARGOS, il faut savoir intégrer la détection des programmes incorrects.

Dans [HM95], nous montrions comment réaliser l'analyse de déterminisme et réactivité sur la forme équationnelle des programmes. Reste donc à savoir où intégrer cette analyse, dans la chaîne de compilation (voir aussi le chapitre 13, pour un schéma global de la chaîne de compilation).

Je présente ici rapidement les résultats de [HM95], et la manière d'intégrer l'analyse qui y est décrite dans la compilation d'ARGOS.

### 5.2.1 Cadre de l'étude

On considère des *automates booléens*, dont les transitions sont définies de manière symbolique par des ensembles d'équations. Ces équations peuvent faire intervenir des variables dites * locales*, et présenter des boucles de définition.
**Definition 5.1 : automate booléen**

Un automate booléen à $n$ variables d'états, $m$ variables d'entrée, $p$ variables locales et $q$ variables de sortie est un n-uplet $A = (init, \Sigma, \Omega, \Lambda, C)$ où :

- $init \subseteq B^n$ est l'ensemble des états initiaux ($B = \{0,1\}$)

- $\Sigma$ est une fonction totale de $B^{m+n+p}$ vers $B^n$ (la fonction de transition), donnée par un vecteur $(\Sigma_k)_{k=1...n}$ de fonctions de $B^{m+n+p}$ vers $B$. Si $s \in B^n$, $i \in B^m$, $\ell \in B^p$, $\Sigma(s, i, \ell)$ représente le vecteur $[\Sigma_k(s, i, \ell)]_{k=1...n}$.

- De même, $\Omega$ est une fonction totale de $B^{m+n+p}$ vers $B^q$ (la fonction de sortie), donnée par un vecteur $(\Omega_k)_{k=1...q}$ de fonctions de $B^{m+n+p}$ dans $B$.

- $\Lambda$ est une fonction totale de $B^{m+n+p}$ dans $B^p$ (la fonction de définition des variables locales), donnée par un vecteur $(\Lambda_k)_{k=1...p}$ de fonctions de $B^{m+n+p}$ dans $B$.

- $C \subseteq B^{m+n}$ donne les contraintes sur l'environnement (cf. ci-dessous).

□

Un tel automate peut être vu comme une machine $M = (S, I, O, T)$ pourvu des contraintes $C$ sur l'environnement, avec :

$$S = B^n, \quad I = B^m, \quad O = B^q \\ (s, i/o, s') \in T \iff \exists \ell \in B^p \text{ tel que } \ell = \Lambda(s, i, \ell) \text{ et } s' = \Sigma(s, i, \ell) \text{ et } o = \Omega(s, i, \ell).$$

On appelle *configuration* du système un couple (état, entrée). Une contrainte sur l'environnement est une formule booléenne des variables d'entrée et d'état du système, qui décrit les configurations dont l'environnement garantit l'inaccessibilité. Les contraintes les plus simples ne portent que sur les variables d'entrée, et peuvent servir par exemple à exprimer que deux signaux ne surviennent jamais simultanément. Une contrainte plus compliquée, nécessitant la prise en compte des variables d'état, peut exprimer que deux signaux d'entrée alternent. Dans le domaine de la conception de circuits, on parle de "don't care sets".

La définition d'un automate booléen comprend trois systèmes d'équations : le système $s'_k = \Sigma_k(s, i, \ell), k = 1...n$ définit les nouvelles valeurs des variables d'états; le système $o_k = \Omega_k(s, i, \ell), k = 1...q$ définit les sorties courantes; le système $\ell_k = \Lambda_k(s, i, \ell), k = 1...p$ définit les valeurs courantes des variables locales.

Les variables de sortie et les variables d'états sont définies par des fonctions *totales* de l'état courant, de la valeur courante des entrées, et de la valeur courante des variables locales. Seules les variables locales peuvent être définies par des équations cycliques.

## 5.2.2 Diverses notions de cohérence

Considérons la fonction *loc*, de $B^{m+n}$ dans $2^{B^p}$ qui associe à chaque configuration $(s, i)$ l'ensemble des solutions du système d'équations $\ell = \Lambda(s, i, \ell)$. Un automate booléen sera dit *fortement cohérent* si et seulement si, pour chaque configuration accessible $(s, i), |loc(s, i)|=1$. Il sera dit *faiblement cohérent* si et seulement si, pour chaque configuration accessible $(s, i), |\{\Omega(s, i, \ell), \ell \in loc(s, i)\}|=1$ et $|\{\Sigma(s, i, \ell), \ell \in loc(s, i)\}|=1$.

Autrement dit, dans un automate fortement cohérent, la valeur des variables locales est déterminée de manière unique, dans chaque configuration accessible. Dans un automate faiblement
cohérent, certaines variables locales peuvent ne pas être déterminées, si cela n'influence ni les sorties, ni l'état suivant.

### 5.2.3 Résultat

Nous décrivons dans [HM95] une méthode de vérification de la cohérence forte, qui s'applique à un système d'équations $\ell = \Lambda(s, i, \ell)$ éventuellement cyclique et fournit deux résultats :

- Une condition $E(s, i)$ vraie exactement quand $| loc(s, i) | = 1$

- Un nouveau système d'équations $\ell = \Lambda'(s, i)$, non cyclique, et tel que $E(s, i) \implies loc(s, i) = \{\Lambda'(s, i)\}$

Ce résultat est l'application d'un théorème d'algèbre de Boole très utilisé dans la conception de circuits pour éliminer des variables dans les fonctions booléennes. L'idée est qu'on peut éliminer une variable si l'on sait prouver qu'elle est entièrement déterminée comme fonction des autres variables. On essaie donc d'éliminer successivement toutes les variables locales — sur lesquelles portent des équations cycliques.

**Le théorème utilisé** Le théorème s'énonce comme suit :

$$ (F \implies (x = f)) \iff \neg(F_x \land F_{\bar{x}}) $$

où $F$ est une fonction de $x$ et d'autres variables, et $f$ une fonction des autres variables seulement. $F_x$ et $F_{\bar{x}}$ proviennent de la décomposition de Shannon de $F$ selon $x$ :

$$ F = (x \land F_x) \lor (\bar{x} \land F_{\bar{x}}) $$

Pour exhiber une fonction $f$ solution, on peut choisir toute fonction booléenne $g$ comprise entre $F_x$ et $\neg F_{\bar{x}}$, c'est-à-dire telle que $F_x \Rightarrow g \Rightarrow \neg F_{\bar{x}}$.

**Méthode** On code tout le système d'équations de l'automate booléen par une formule $F$ dans laquelle apparaissent, en particulier, les variables locales $\{\ell_0, \ell_1, ..., \ell_k\}$. On essaie de prouver que, pour chacune d'entre elles, $F$ détermine une solution unique.

Puisque $F = x \land F_x \lor \bar{x} \land F_{\bar{x}}$, $F_x \lor F_{\bar{x}}$ est une condition nécessaire et suffisante pour qu'il existe une solution pour la variable $x$ dans le système $F$. Pour qu'elle soit de plus unique, d'après le théorème cité ci-dessus, il faut et il suffit que $\neg(F_x \land F_{\bar{x}})$.

Partant de $F^{(0)} = F$, on tente d'éliminer chaque variable locale $l_i$ à son tour, et on calcule donc successivement, pour $i \in [1..k]$ :

$$ F^{(i)} = F_{l_i}^{(i-1)} \lor F_{\bar{l}_i}^{(i-1)} $$

$$ g^{(i)} = F_{l_i}^{(i-1)} $$

$$ E^{(i)} = \neg(F_{l_i}^{(i-1)} \land F_{\bar{l}_i}^{(i-1)}) $$

Ensuite on substitue la solution $g^{(j)}$ choisie pour la variable $l_j$ à toute occurrence de $l_j$ dans les formules $g^{(i)}$ et $E^{(i)}$ où $j > i$. Le résultat est formé du système d'équations $l_i = g^{(i)}$, $i = 1..k$, et de la formule $E = \bigwedge_{i=1}^k E^{(i)}$, qui ne porte plus que sur les variables d'état et les variables d'entrée. $E$ est une condition nécessaire et suffisante pour que $F$ détermine entièrement toutes les variables locales.
**Note:** ces algorithmes étant implantés en utilisant des BDD, on ne choisit pas $g^{(i)} = F_{l_i}^{(i-1)}$ mais plutôt $g^{(i)} = F_{l_i}^{(i-1)} \uparrow F^{(i)}$, où $\uparrow$ représente l'opérateur de restriction défini dans [BCM90]. Cette fonction est bien comprise entre $F_{l_i}$ et $\neg F_{\overline{l_i}}$, et l'opération de restriction garantit un BDD plus petit.

On trouvera dans [HM95] l'exposé de la méthode d'analyse pour la cohérence faible.

### 5.2.4 Intégration dans le processus de compilation d'ARGOS

Dans l'expérimentation conduite avec l'outil BAC, un programme ARGOS est traduit globalement en un automate booléen comme défini ci-dessus, et l'analyse de déterminisme et réactivité est réalisée globalement (aux conditions d'activation près, la traduction suit les idées de la traduction d'ARGOS en DC). Cela revient à considérer que tous les signaux déclarés locaux à un sous-arbre sont en fait "remontés" jusqu'à la racine de l'arbre abstrait. Cela suppose un renommage, puisqu'un même nom de signal peut être utilisé dans deux sous-arbres distincts. La question importante concerne la sémantique.

La figure 5.5 donne un exemple de programme dans lequel un cas de non-déterminisme détecté dans le sous-arbre d'une opération d'encapsulation est ensuite levé par le contexte. Si l'on applique strictement la sémantique décrite au paragraphe 2.3, page 35, le programme est déclaré globalement incorrect, puisque la valeur $\perp$ obtenue comme sémantique du composant qui déclare a, b locaux se propage jusqu'à la racine.

<figure><img src="image_31.png" /><figcaption>FIG. 5.5 – *Un exemple de non déterminisme éliminé par le contexte*</figcaption></figure>

Si l'on applique les techniques décrites plus haut, l'analyse du sous-arbre incriminé ne produit pas la valeur $\perp$, mais une information plus riche: la condition sur les états et signaux d'entrée qui garantit que le programme est réactif et déterministe. Dans le cas de l'exemple, on obtiendra la condition $\neg(X \land Y \land i)$ — en supposant que chaque état est codé par une variable de même nom. On obtient également les équations qui définissent a et b en fonction des autres variables, dans les cas où cette condition est vérifiée, ici: $a = b = FALSE$.

On peut ainsi, pour chaque sous-arbre d'opération d'encapsulation, produire une condition
nécessaire et suffisante de correction, et un ensemble d'équations définissant les signaux de sortie et les états en fonction des siganux d'entrée, dans lequel n'apparaissent plus de variables locales.

Les conditions sont propagées dans le contexte, où elles peuvent devenir trivialement vraies, comme c'est le cas dans l'exemple ci-dessus: le contexte fournit l'équation $i = FALSE$.

A la racine de l'arbre, on obtient une condition globale. Si elle est impliquée par les contraintes sur l'environnement (exclusivité de signaux, ...), le programme peut être considéré comme correct. Dans le cas contraire, la condition peut être vraie pour des raisons d'accessibilité des états qui y interviennent. Dans ce cas l'analyse exacte de correction demande un calcul des états accessibles. On peut aussi se contenter de ce résultat trop fort, et considérer qu'une erreur de déterminisme ou de causalité dissimulée dans une partie inaccessible du programme mérite d'être signalée... et corrigée.

On retrouve ici la discussion sur la détection des erreurs de type dans les portions de code mort, qui se pose pour les langages séquentiels. A ceci près qu'une portion de code mort détec- table dans un langage séquentiel peut en général être supprimée syntaxiquement, alors que ce n'est pas le cas pour ARGOS (pour un langage à structure parallèle en général) : on peut avoir dé- tecté l'inaccessibilité d'une configuration d'états des divers composants parallèles, et ne pouvoir supprimer les états incriminés, qui participent à d'autres configurations parfaitement accessibles, elles.

**Note:** une comparaison de cette définition de correction des programmes avec la définition de *causalité* introduite pour ESTEREL est esquissée au chapitre 9.
# Chapitre 6

## Eléments de définition du langage Argos

Sources: *Non publié. En partie implémenté.*

Le chapitre 2 présente la base d'ARGOS, sous forme d'un ensemble d'opérations sur les machines de mealy booléennes. La définition de ce qui pourrait commencer à s'appeler un *langage*, à partir de cette base formelle, exige que l'on s'intéresse à des aspects aussi divers que le choix d'une syntaxe concrète (qu'elle soit graphique ou textuelle); l'introduction d'un mécanisme de structuration des textes de programmes; le support pour une répartition des programmes sur plusieurs fichiers; la définition de macro-notations pour les constructions d'usage courant; un support pour les aspects de remontée au source lors du processus de compilation; un support à toutes les extensions envisagées (présentées dans les chapitres suivants). Nous donnons ici une proposition de syntaxe concrète qui tient compte de la plupart de ces aspects.

### 6.1 Structuration des programmes et restriction de l'environnement

#### 6.1.1 Structuration

Les programmes ARGOS seront structurés en *processus* comme les programmes LUSTRE en *noeuds*. L'idée est la même, le mot *processus* étant choisi simplement pour refléter le caractère plus impératif du langage.

Un processus a un *nom*, qui permet de l'appeler dans un autre contexte ; une interface, c'est-à-dire deux listes de paramètres formels (d'entrée et de sortie), qui désignent des signaux booléens ; une liste de signaux locaux ; et un *corps* : c'est une construction à l'aide des opérateurs ARGOS définis au chapitre 2, dans laquelle les étiquettes de transitions d'automates sont construites en utilisant les signaux déclarés dans l'interface ou locaux au processus.

#### 6.1.2 Restriction sur l'environnement d'un processus

Nous avons mentionné au chapitre 5 la possibilité d'associer à un noeud DC une spécification des configurations dont l'environnement garantit l'inaccessibilité. Une *configuration* du système est un couple (état, entrée). En DC, une telle spécification est une simple formule sur les variables locales définies par des mémorisations — les états — et sur les variables d'entrée. En ESTEREL
on trouve deux types de contraintes instantanées sur les signaux d'entrées d'un module : des exclusions n-aires (notées $\#)$ et des implications. En LUSTRE le mécanisme des assertions est aussi puissant que celui de DC.

On cherche à introduire un tel mécanisme en ARGOS. Les contraintes les plus simples, comme l'exclusion de deux signaux d'entrée, sont "sans mémoire". Elles ne portent que sur les variables d'entrée. On peut décider d'attacher à la définition d'un processus une formule booléenne qui définit les entrées valides. Un tel mécanisme est plus puissant que les deux types de contraintes d'ESTEREL, mais ne permet toujours pas d'exprimer des contraintes "à mémoire", comme l'alternance de deux signaux d'entrée.

On pourrait décider que la formule qui définit les entrées valides peut faire intervenir les états des automates du processus. Dans ce cas, l'un des automates, ou même une sous-expression du corps du processus, peut être entièrement consacré(e) à la définition des entrées valides. Pour exprimer que deux signaux d'entrée $a$ et $b$ alternent, on peut introduire un automate à deux états $X$ et $Y$, qui n'émet rien. Il passe de $X$ à $Y$ sur occurrence de $a$, et de $Y$ à $X$ sur occurrence de $b$. Cet automate est placé en parallèle avec la structure qui définit le corps du processus proprement dit. La formule de définition des entrées valides s'écrit : $(a \implies X) \land (b \implies Y)$. Le choix de l'état initial, parmi $X$ et $Y$, indique lequel des deux signaux doit commencer la séquence.

On peut aussi se contenter d'autoriser l'utilisation des signaux locaux ou même des signaux de sortie du processus, dans la formule de définition des entrées valides. C'est une manière détournée de faire référence à l'état, puisque les sorties et les signaux locaux dépendent de l'état. Dans l'exemple ci-dessus, on ajoute au processus le même automate à deux états, qui émet $x$ (resp. $y$) continuellement quand il est dans l'état $X$ (resp. $Y$). La formule se transforme en $(a \implies x) \land (b \implies y)$. Puisque les signaux $x$ et $y$ ne servent qu'à définir les entrées valides, ils ne sont pas visibles à l'extérieur : ce sont des signaux locaux attachés au processus.

Un autre moyen, calqué sur la définition des observateurs de programmes synchrones, consiste à prendre pour convention que la correction des entrées est définie par l'absence d'un signal dédié.

## 6.2 Aspects de syntaxe concrète

### 6.2.1 Abréviations des conditions booléennes

La première exigence concerne la définition de conventions raisonnables permettant d'abréger la notation des conditions booléennes de transitions.

On convient naturellement d'omettre les transitions qui bouclent et qui n'émettent pas de signal. Un programme peut donc toujours être complété, sans ambiguité, par les boucles manquantes. Pour chaque état $X$ d'automate de base, la boucle manquante est étiquetée par $\neg(c_1 \lor c_2 \lor \dots \lor c_n)$, où les $c_i$ représentent les conditions des transitions issues de $X$.

### 6.2.2 Non déterminisme comme une abréviation

Nous nous plaçons dans le cas où le non-déterminisme intrinsèque des automates n'est pas accepté. Dans certains cas un non déterminisme apparent peut être interprété comme une abréviation. Si l'on écrit à partir d'un état $X$ deux transitions dont les conditions sont $a$ et $b$, l'automate est non déterministe, puisque $a \land b$ est un événement possible.

Plusieurs situations se présentent :

- On peut prouver qu'une des contraintes sur l'environnement implique que $a$ et $b$ sont deux signaux exclusifs, dans cet état $X$. Le non déterminisme n'est donc qu'apparent, et les
<figure><img src="image_32.png" /><figcaption>FIG. 6.1 – Macro-notation de temporisation des états</figcaption></figure>

conditions pourraient être remplacées sans modification de sémantique par $a \wedge \neg b$ et $b \wedge \neg a$.

- Aucune contrainte explicitement spécifiée par le programmeur n'implique que $a$ et $b$ sont exclusifs dans $X$, ou bien on ne sait pas le montrer sans exploration de l'espace d'états. Tou-tefois la propriété est peut-être vraie, ou bien le programme global dans lequel l'automate considéré est utilisé assurera peut-être cette propriété, si $a$ et $b$ sont des signaux locaux. Au lieu de rejeter l'automate — et le programme — dès la phase d'analyse de déterminisme, on peut modifier localement le programme en ajoutant la contrainte d'exclusivité de $a$ et $b$ dans l'état $X$ à la formule qui définit les entrées valides du processus. Le non-déterminisme des automates d'un processus est donc un moyen d'enrichir les contraintes d'environnement associées à ce processus.

### 6.2.3 Macro-notations

#### 6.2.3.1 Etats temporisés

La notion d'état temporisé est définie au chapitre 10. Intuitivement, lorsque le système entre dans un état temporisé par le délai $d$ sur le signal $s$, il ne peut y rester après que $d$ occurrences du signal $s$ ont été reçues. Une transition dite de "timeout" est prévue à cet effet. Le programme de la figure 6.1 permet de détecter les simples ou doubles clicks d'une souris.

L'expansion de la macro-notation de temporisation consiste à ajouter un automate compteur en parallèle avec la composante temporisée. Les deux composants communiquent dans les deux sens : le programme d'origine signale son entrée dans l'état temporisé, de manière à lancer le compteur ; il signale toute sortie normale de l'état temporisé, pour permettre de désarmer le compteur. Inversement, le compteur signale qu'il expire, et cela déclenche la transition de timeout.

Pour l'exemple de la figure 6.1 le programme expansé est donné par la figure 6.2.

#### 6.2.3.2 Equations

L'idée d'introduire des équations est née de l'étude de la programmation multi-langages AR-GOS+LUSTRE présentée au chapitre 8. Nous proposons ici une extension très simple de la syntaxe ARGOS, sous forme de macro-notation.

Une équation $x \leftarrow b$ où $x$ est un signal de sortie, et $b$ une formule booléenne quelconque faisant intervenir des signaux d'entrée et des signaux locaux, est directement utilisable, puisque ce n'est qu'une abréviation pour un automate à un état et une transition étiquetée par $b/x$, que l'on placerait en parallèle. On préfère la notation $x \leftarrow b$ à la notation $x = b$ de LUSTRE, pour
<figure><img src="image_33.png" /><figcaption>FIG. 6.2 – Expansion de la macro-notation de temporisation</figcaption></figure>

ne pas avoir à exiger qu’un signal ne soit défini que par une seule équation. Un programme peut
contenir deux équations $x \leftarrow b_1$ et $x \leftarrow b_2$, qu’on peut ou non remplacer par $x \leftarrow b_1 \lor b_2$.

6.2.3.3 Interruptions préemptives

Au chapitre 2 nous avons montré comment exprimer les interruptions préemptives grâce à
une construction qui utilise le raffinement et l'opération de définition d'horloge (figure 2.10). Si
l'on se donne un marquage des flèches de transitions pour repérer les transitions préemptives, il
est aisé de produire un programme ARGOS de base, en ajoutant un signal d'horloge.

En syntaxe graphique, nous proposons une extension de ce genre au chapitre 9. En syntaxe textuelle, il faudrait trouver un mot clé et décider de l'endroit où il apparaît.

## 6.3 Un mécanisme général de pragmas

Les pragmas sont des informations non structurées — ou plutôt dont l'éventuelle structure n'est pas connue du compilateur ARGOS — et que l'on attache à certaines structures syntaxiques d'ARGOS. L'extension du compilateur prévoit d'attacher des pragmas aux états, aux transitions, aux processus, à la structure globale du programme, etc. L'application de la méthode au cas des systèmes hybrides ne nécessite que des pragmas d'états et de transitions.

Le compilateur a la charge de construire l'automate global, en transmettant les pragmas. La figure 6.3 donne un programme ARGOS équipé de pragmas, et la structure de l'automate global, équipé de pragmas composés.

Les pragmas associés aux états globaux héritent de la structure du programme ARGOS : en-
semble de pragmas séparés par des virgules pour les compositions parallèles et un niveau de
hiérarchie préfixé par le pragma de l'état raffiné, dans le cas des raffinements. Ainsi l'état XAC
hérite-t-il du pragma composé : [χ [α,β]].

Les pragmas associés aux transitions héritent également de la structure du programme. Le pragma associé à la transition globale de XAC vers Y (obtenu par composition des transitions t1, t3 et t5, conformément à la sémantique d'ARGOS) est : [χ [τ₁,τ₃],τ₅].

Le compilateur transmet ainsi les pragmas en conservant l'information maximale sur la struc-
ture du programme, qui peut être nécessaire à l'utilisation desdits pragmas par un outil aval.
<figure><img src="image_34.png" /><figcaption>FIG. 6.3 – Transmission des pragmas par le compilateur ARGOS</figcaption></figure>
Dans le cas de POLKA (voir chapitre 11 la connexion de l'environnement ARGONAUTE à l'outil POLKA, pour l'analyse des systèmes hybrides), les pragmas attachés aux états raffinés peuvent par exemple servir de déclarations de variables, locales aux pragmas du processus raffinant. Conserver la structure du programme ARGOS permet alors de définir des variables avec un classique mécanisme de blocs imbriqués.

Le mécanisme général des pragmas permet d'implanter les extensions temporelles et hybrides ou d'utiliser des variables données.

## 6.4 Extensions

### 6.4.1 Variables de contrôle non booléennes

Les variables de contrôle sont introduites pour éviter d'avoir à coder par un automate un élément du contrôle qui peut prendre un nombre fini et relativement petit de valeurs, mais pour lequel les transitions sont faciles à exprimer par des calculs. Typiquement, les automates compteurs introduits pour l'expansion de la macro-notation de temporisation seraient décrits beaucoup plus simplement avec des variables de contrôle qu'avec un automate explicite. La figure 6.4 donne un automate compteur sur l'intervalle [0, 10], décrit en extension (a) et à l'aide d'une variable de contrôle notée $c$ (b).

Les variables de contrôle sont du type intervalle d'entiers fini (on pourrait également envisager des types énumérés, mais alors on retrouve les automates explicites, puisque les transitions ne peuvent être décrites qu'en donnant explicitement tous les triplets <état source, étiquette, état but>), sur lequel on peut réaliser des opérations évaluables statiquement.

Si les variables de contrôle sont attachées à un processus, chacune d'entre elles représente un composant parallèle réduit à un automate, dont les états sont les valeurs possibles de la variable. Les conditions et affectations portant sur des variables de contrôle peuvent être explicitement traduites en communications par diffusion synchrone, à l'aide de signaux auxiliaires, ou directement interprétées par le compilateur. Dans tous les cas, les valeurs de la variable sont traitées comme des états du contrôle.

### 6.4.2 Variables "données" non booléennes

On peut vouloir également manipuler des variables données, c'est-à-dire dont les valeurs ne doivent pas faire partie de la structure de contrôle du processus. On peut définir un sous-langage d'ARGOS pour la définition et la manipulation de telles variables, éventuellement en important les types et les opérations depuis un langage hôte, comme c'est fait pour LUSTRE et ESTEREL. On peut aussi cacher entièrement ces aspects dans les pragmas.

## 6.5 Une proposition de syntaxe textuelle

La syntaxe textuelle présentée ici intègre les extensions nécessaires à la manipulation de l'horloge de base, à l'introduction de variables de contrôle, à la définition de pragmas, etc.

### 6.5.1 Variables de contrôle

Les variables de contrôle sont de type intervalle d'entiers. Les définitions des types utilisés et la déclaration des variables de contrôle sont attachés à la définition d'un processus. Ces variables
<figure><img src="image_35.png" /><figcaption>FIG. 6.4 – *Variables de contrôle ou automates explicites*</figcaption></figure>
sont utilisables dans les transitions des automates de ce processus.

## 6.5.2 Etiquettes de transitions

Une étiquette de transition élémentaire comporte 4 champs :

- Une condition sur les variables de contrôle

- Une condition booléenne sur les signaux

- Un ensemble de signaux émis

- Une affectation aux variables de contrôle

Une étiquette est une suite d'étiquettes élémentaires séparées par des signes +. Cela permet de ne définir qu'une fois les états source et but de la transition, même si elle doit porter des quadruplets différents. Exemple : $(v = 5) \& (v > 3) \ u \ & \ x / z,t \ v := 2*3 + (v = 4) \ u/t$

## 6.5.3 Structure interne des processus

Les corps de processus sont décrits à l'aide des opérateurs suivants :

**Composition parallèle, notée $||$** La notation est infixée, l'opération est commutative et associative. $\mathit{toto}(x)(z) || \mathit{tutu}(y)(t) || \mathit{titi}(x)(z,t)$ représente la composition parallèle de trois appels de processus.

**Raffinement** Le raffinement est considéré comme une structure de contrôle paramétrée par l'automate. Cette structure a donc *n* places d'arguments si l'automate de contrôle a *n* états. On note : **controller { ... }**. Le corps de cette structure est composé de la déclaration de chacun des états, suivi de son ensemble de transitions sortantes. L'état lui-même définit un bloc dans lequel on peut décrire le processus raffinant, s'il existe.

**Encapsulation** La question se pose de savoir si tous les signaux locaux d'un processus sont attachés à la définition du processus, et donc en quelque sorte déclarés à la racine de son arbre abstrait. Introduire un opérateur d'encapsulation (la structure **signal ... in ... end d'ESTEREL**) permet de déclarer des signaux locaux à des sous-arbres. Inversement, le choix d'attacher les déclarations à la définition de processus est analogue à celui de **LUSTRE**. Les auteurs de **LUSTRE** aimaient maintenant en changer, il semble que ce soit parfois contraignant. Pour **ARGOS**, introduisons donc cet opérateur. La seule difficulté provient de la traduction en **DC** (cf. chapitre 5), dans laquelle on a décidé de construire un noeud **DC** par processus **ARGOS**. Or les signaux locaux des noeuds **DC** sont attachés à la définition du noeud. Il y a deux solutions : la première consiste à changer de méthode, et à produire un noeud **DC** par sous-arbre d'opérateur d'encapsulation ; la seconde consiste à "remonter" les déclarations de signaux locaux à la racine de l'arbre abstrait du processus, avec un éventuel renommage, mais il faut alors garantir que cela ne change pas la sémantique (voir les arguments dans ce sens, section 5.2.4 du chapitre 5).

**Condition d'activation** L'opération qui associe une condition d'activation à un processus est notée **when**. On écrit donc : **when B { P }**, où B est une condition booléenne et P un processus quelconque.
Notons que les automates sont des opérateurs. C'est une des raisons pour lesquelles les automates ne sont pas réutilisables comme les processus, par un mécanisme d'appel. Il faudrait plutôt un mécanisme d'instance de classe.

### 6.5.4 Contraintes sur l'environnement

Dans la syntaxe proposée ci-dessous les contraintes sur l'environnement sont attachées à la définition d'un processus, et ne portent que sur ses signaux d'entrée. On donne une formule booléenne quelconque de signaux d'entrée.

### 6.5.5 Temporisation des états

La borne de temporisation d'un état est optionnelle. Elle est associée à la définition d'un état: `state delay 4 ...`

### 6.5.6 Définition de processus, mécanisme d'appel et processus racine

**A FAIRE**

Le mécanisme d'étiquetage des appels de processus est introduit pour faciliter la remontée au source lors de l'expansion.

## 6.6 Exemple de programme

```s
 targos // this is just a keyword...
```

```c
/* Definition of the main process */
```

```c
main P (a,b,c)(d,e)
with (~a | b) & #(a,b,c) ;
```

```c
/* Process declarations */
```

```c
process P (x,y,z)(u,t) // declares the name of the process, and
                          // the lists of formal input and output
                          // parameters.
```

```c
[ this a pragma associated to process P ]
```

```c
internal v, w ; // local signals.
```

```c
types // types of control variables used in this process
```

```c
trois = 1..3 [ type pragma ] ;
```

```c
quatre = 1..4 ;
```

```c
cinq = 4..5 ;
```

```c
var // CONTROL variables, with type and initial value.
```

```c
trois v = 2 [ variable pragma ] ;
```

```c
truc w = 1 ;
```

```c
{
  // begin description of the process structure
```

```c
internal a,b {
```

```c
tag1:Q (u)(k) // tagged call of process Q
```

```c
|
```

```c
controller {
  init One // specifies the initial state
```
// State One has two transitions, to states Two and Three.

// and it is refined by a process made of Q, R and S.

One [ this is a pragma associated to state One]

{ when (x & ~y) {
    tag1:Q (x)(t) ||
    tag3:R (y)(t) ||
    tag4:S (x)(z,t)
}

}

-> Two with u & ~x / z,t + ~u & x / z ;

-> Three with y/t [ this a pragma for the transition ] ;

// State Two is not refined. It has only one transition.

// It has a delay attached to it.

Two delay 4 {} -> Two with { (v = 5) & (v > 3) } u/c { v := 2*3 } ;

// State Three is not refined. It has one transition.

Three {} -> One with y/;

} // end of "controller" structure

} // end of "internal" structure

} // end of process P

process Q (in)(out) { ... }

process R (in)(out) { ... }

process S (a)(b,c) { tag1:R (a)(b) || c <- a}

endtargos
# Deuxième partie

## Programmation multi-langages synchrone
<figure><img src="image_36.png" /></figure>
# Chapitre 7

## La programmation multi-langages : motivations et première étude dans le cadre synchrone

Sources: L'essentiel du travail sur le thème programmation multi-langages est décrit dans [JLMR94, JLMR93, Jou94]. On y trouve en particulier les motivations et le résumé d'une étude bibliographique débordant un peu du contexte des langages synchrones. Toutefois la première étude qui portait sur ARGOS et LUSTRE a soulevé de nouveaux problèmes, qui ont été traités indépendamment des aspects multi-langages. Nous reprenons ici l'énoncé des motivations, les propositions d'implantation décrites dans [JLMR93, Jou94], et les conclusions de ce travail, qui ont conduit à la proposition de mélanger les langages au niveau DC. La solution préconisée actuellement fait l'objet du chapitre suivant.

### 7.1 Motivations et travaux sur le sujet

Les premières idées de programmation multi-langages sont anciennes dans la communauté synchrone, et proviennent de quelques observations simples. Les styles impératif textuel, impératif à base d'automates, flot de données déclaratif, etc., représentés parmi les langages synchrones, correspondent à des cultures différentes dans l'industrie. LUSTRE, surtout sous sa forme graphique, paraît ainsi très naturel dans une communauté qui utilise les schémas-blocs ; un langage à base d'automates rappelle le Grafcet aux concepteurs d'automates programmables. Toutefois, la description de systèmes de taille conséquente montre souvent les limites d'une approche homogène, quelle qu'elle soit. Dans une description flot de données, on peut avoir envie de décrire une structure de contrôle globale sous forme d'automate ; dans une description purement impérative, les fonctionnements réguliers qui impliquent beaucoup de calculs sont souvent lourds à décrire. En quelque sorte, le style déclaratif flot de données se prête bien à la description des régimes permanents, alors que les styles impératifs conviennent mieux à la description des régimes transitoires ou des ruptures de phases de fonctionnement. Un cas typique est constitué par les systèmes de vision par ordinateur, dans lesquels des phases de traitement du signal sont contrôlées par des modes de fonctionnement. De manière générale, tout système réactif de taille importante comprend les deux aspects. Les différents styles de programmation sont donc complémentaires plutôt que concurrents, et on aimerait pouvoir les utiliser conjointement dans une description de
grande taille.

D'autre part, l'approche synchrone permet l'expression des propriétés à vérifier par des *ob-servateurs* [HLR93], un observateur de la propriété *P*, pour un programme *Q*, est un autre programme *O* — qui peut donc être écrit dans le même langage — qui observe les sorties et les entrées de *Q* et n'a qu'une sortie : un booléen *ok*. On exécute *Q* et *O* en parallèle, et on observe la sortie *ok*. L'observateur est conçu de telle manière que *ok* est vraie tant que le programme *Q* vérifie la propriété *P* ; elle devient fausse, et le reste, dès que *Q* viole *P*. La programmation multi-styles ou multi-langages peut être utilisée dans ce cadre : le programme à vérifier peut par exemple être écrit en LUSTRE et l'observateur en ARGOS. Pour des propriétés du genre *au moins un 'a' dans chaque intervalle défini par les occurrences de 'b' et 'c',* l'expression sous forme d'automate met clairement en évidence les cas limite, et peut-être plus lisible que la version LUSTRE. En suivant cette même idée, Pascal Raymond a proposé dans [Ray96] de décrire les propriétés de programmes synchrones par un langage à base d'expressions régulières, qui sont ensuite compilées en programmes LUSTRE grâce à l'outil REGLO.

Des préoccupations similaires apparaissent dans de nombreux contextes. Une étude bibli-
graphique du sujet est nécessairement très partielle ; l'étude des langages est au coeur de l'in-
formatique, et le thème de la programmation *multi-styles*<fnref n="1" /> est un thème transversal à tous les
domaines de l'informatique. Une recherche rapide dans la *Collection of Computer Science Bi-
bliographies*, pour le mot-clé *multiparadigm*, donne des références relatives aux langages visuels,
à la programmation concurrente orientée objet, à la spécification de systèmes téléphoniques, à
l'ordonnancement de tâches, à la construction de compilateurs, à la modélisation du processus
de développement et, bien sûr, à la recherche d'informations (!).

Toutefois nous n'avons pas trouvé de travaux sur le thème de la programmation multi-styles en
soi, indépendamment d'une d'application particulière. Les travaux les plus accessibles concernent
des langages généraux, et proposent de mêler les styles objet, logique, impératif, ... Voir par
exemple la définition de LEDA, un langage qui offre les styles impératif, fonctionnel, orienté objet
et relationnel [Shu91, PPST93], ou celle de Oz [Smo94b, Smo94a] (plus de détails à l'adresse :
http://ps-www.dfki.uni-sb.de/oz/). D'après ses auteurs, Oz est basé sur un nouveau modèle
de calcul qui permet d'intégrer simplement les styles fonctionnel d'ordre supérieur, logique avec
contraintes et orienté-objet concurrent. Oz est conçu comme le successeur de Lisp, Prolog et
Smalltalk. L'accent y est mis sur la définition d'un petit ensemble de constructions sémantiques,
à partir desquelles peuvent être dérivées des constructions usuelles des langages orienté objet,
par exemple.

7.2 Programmation multi-langages dans le cadre synchrone

Notre point de vue est moins général, puisque nous nous intéressons au problème relativement précis de la programmation *multi-langages*, à partir d'un petit ensemble de langages bien identifiés, qui disposent en outre d'une base sémantique commune. J'utilise l'adjectif "multi-langages" pour des approches qui consistent à considérer des programmes écrits dans des langages différents, et à définir une sémantique qui étend chacune des sémantiques d'origine. Une approche multi-langages est plus intéressante si elle porte sur des langages de styles différents.

Dans [JLMR94], nous proposons une approche de programmation multi-langages *au niveau source*, par opposition à l'utilisation d'une technique d'éditions de liens. Une réflexion plus appro-

<footnote n="1">1. L'approche est en général qualifiée de "multi-paradigmes". Bien que le terme semble consacré, il est fort peu approprié en français, et nous lui préférerons celui de "multi-styles".</footnote>
fondie montre que la différence entre ces deux approches n'est pas fondamentale ; ce n'est qu'une question de degré. L'approche de compilation d'un programme mixte ARGOS+LUSTRE via le format DC, que nous proposons au chapitre 8, suit exactement le même schéma que la compilation d'un programme écrit en C et PASCAL, via le format des fichiers binaires translatables.

### 7.2.1 Travaux de même nature

Dans la communauté synchrone ou à sa périphérie, on trouve le système PTOLEMY développé dans l'équipe d'Edward Lee à Berkeley. PTOLEMY est un environnement de programmation pour le développement, la simulation, et le prototypage de systèmes de traitement du signal et temps réel. PTOLEMY offre différents modèles d'exécution qui permettent de spécifier les interactions entre les calculs et leur ordonnancement. En outre, PTOLEMY permet de mélanger plusieurs modèles d'exécution dans une même application afin de choisir le modèle le mieux adapté à chaque sous-système. Parmi les modèles d'exécution on trouve un mode qualifié de "flot de données synchrone" et un mode "machine d'états finie". Les problèmes posés sont toutefois d'un autre ordre que ceux auxquels nous nous intéressons ici: PTOLEMY cherche à intégrer, non seulement des styles de programmation différents, mais aussi des modèles de calcul différents.

Le travail présenté ici s'apparente plus à [ZJ93], que P. Zave m'a signalé depuis à l'occasion d'un exposé sur la programmation ARGOS+LUSTRE via DC (objet du chapitre 8). On trouve également dans [CV89] une proposition de combinaison des statecharts et de la logique temporelle PTL pour la spécification des systèmes réactifs, où les Statecharts sont utilisés pour décrire des comportements trop généraux, qui sont ensuite restreints par des propriétés exprimées en PTL.

Une équipe des Bell Labs s'intéresse à la combinaison ESTEREL+ML.

Avec l'objectif de fournir en LUSTRE des structures de contrôle permettant par exemple de ré-initialiser un processus, Paul Caspi et Marc Pouzet ont proposé une extension de LUSTRE par ajout de structures récursives. [RM95] décrit d'autre part une proposition d'introduction de structures de contrôle dans SIGNAL, sous formes d'intervalle d'activation des processus. Cette extension a été utilisée pour décrire un système de vision.

### 7.2.2 Analogie avec C et PASCAL

Nous concluions dans [JLMR94] que la programmation multi-langages n'est envisageable que si l'on sait identifier, dans chacun des langages candidats, un niveau d'encapsulation adéquat, qui définit les blocs échangeables. Dans le cas de C et PASCAL, il s'agit des procédures ou fonctions. On peut appeler une fonction C depuis une procédure PASCAL, parce que la sémantique de ces blocs est comparable (suffisamment, en tout cas, pour que les deux objets soient compilés de la même façon, et que les fichiers objets soient fusionnables — les conventions d'utilisation de la pile ou des mécanismes de fenêtres de registres pour le passage de paramètres étant imposées par le système, et respectées par les différents compilateurs). On ne peut guère descendre plus bas que la structure de procédure ou fonction pour mêler C et PASCAL: dès que l'on imagine des imbrications de structures de contrôle, on rencontre des programmes comme :

```pascal
while x < y do (* c'est du pascal *)
  begin
    if ( f(x,y) ) break;      /* c'est du C */
  end;
```

où des instructions qui n'ont de sens que dans un contexte C apparaissent dans un contexte PASCAL.
La relation est évidente entre cette notion de bloc échangeable, et la notion de programme, par opposition aux termes, utilisée pour la formulation de la propriété de complète adéquation d'une sémantique (voir chapitre 2, section 2.5.2).

Le seul argument pertinent pour distinguer un mélange *au niveau source* concerne les aspects pratiques d'analyse des fichiers source: peut-on réellement mêler les constructions de deux langages dans un même fichier source, auquel cas on doit imaginer un analyseur syntaxique capable de comprendre un sur-ensemble des deux syntaxes ? Mais il y a de fortes chances pour que le niveau de bloc que l'on a identifié comme adéquat pour l'échange entre langages, soit également le niveau de bloc utilisé pour la programmation modulaire, dans chacun des deux langages pris séparément. On peut donc fournir les fragments de programmes dans des fichiers distincts, en confier l'analyse aux analyseurs mono-langages, et ne s'occuper que de la fusion des objets compilés.

### 7.2.3 Le cas ARGOS+LUSTRE

Dans le cas des langages synchrones, et en particulier de LUSTRE et ARGOS, le problème est à la fois beaucoup plus facile, un peu plus difficile et beaucoup plus intéressant, que dans le cas de C et PASCAL. Difficile et intéressant, parce que les structures d'ARGOS et de LUSTRE sont bien plus différentes que celles de C et PASCAL; facile parce que la base sémantique commune est beaucoup plus large (et formellement définie).

Comprendre comment les deux langages peuvent être mêlés, et estimer la richesse du mélange obtenu, suppose donc que l'on clarifie cette base sémantique commune. C'est ce que nous montrions dans [JLMR94], en présentant des abstractions de LUSTRE et ARGOS, nommées respectivement L et A. Ces abstractions permettent de comprendre comment l'on décrit des objets de base et comment l'on compose des objets, dans chacun des deux langages. On montre ensuite que les objets de base décrivent les mêmes objets sémantiques, puis on propose un langage mixte qui offre : les deux façons de décrire des objets de base, toutes les manières de composer des objets.

On peut en donner une vue encore plus abstraite, en oubliant momentanément le raffinement (la formulation qui suit est inspirée par des discussions avec Paul Caspi, et par ses présentations des fondements de l'approche synchrone).

Considérons un ensemble de signaux d'entrée *I* et un ensemble de signaux de sortie *O*. Un comportement réactif peut être décrit de deux manières : a) par un système de transitions fini — une machine de Mealy comme définie au chapitre 2 ; b) par une fonction *f* de $P(I)^*$ (les séquences d'entrée) vers $P(O)^*$ (les séquences de sortie), à mémoire bornée. Les deux modèles sont interchangeables. En effet, si *f* n'utilise qu'une abstraction bornée de la séquence d'entrées pour calculer la séquence de sorties, elle peut être représentée par un système de transitions dont les états correspondent aux valeurs possibles de la mémoire. Inversement, tout système de transitions fini représente une fonction des séquences d'entrées vers les séquences de sorties.

ARGOS peut être vu comme l'exemple type le plus simple d'un langage basé sur le point a) ci-dessus : les objets de base sont donnés par des systèmes de transitions et la composition repose sur le produit synchrone. Les programmes sont définis par :

$$ 
\begin{align*}
A &::= \mathit{BasicA} \mid A \parallel A \\
\mathit{BasicA} &::= \dots
\end{align*}
$$

En ARGOS on donne explicitement les ensembles d'états et de transitions des composants de base. C'est un héritage de la syntaxe graphique, mais on peut imaginer d'autres genres de descriptions
pour les BasicA. La sémantique est donnée par une fonction : $S_i : A \longrightarrow \mathcal{M}$ (où $\mathcal{M}$ est l'ensemble des machines de Mealy définies au chapitre 2), qui vérifie : $S_i(A_1 \| A_2) = S_i(A_1) \times S_i(A_2)$.

LUSTRE est l'exemple type d'un langage basé sur le point b). Les objets de base sont des fonctions décrites par des systèmes d'équations. Ces objets sont connectés par des "fils", pour former des réseaux flot de données, qui peuvent être décrits graphiquement ou textuellement, par des systèmes d'équations (on nomme les fils par des variables). Les programmes peuvent être décrits par :

$$ 
\begin{align*}
\text{DF} &::= \text{BasicDF} | \{\text{eq}\} \\
\text{eq} &::= o = \text{BasicDF}(i)
\end{align*}
$$

où $o$ et $i$ sont des n-uplets de noms de variables, et représentent les séquences de valeurs qui passent dans les fils. Les BasicDF sont les fonctions à mémoire bornée qui forment les "noeuds" du graphe flot de données. En LUSTRE on garantit que ces fonctions sont à mémoire bornée par des restrictions syntaxiques : les équations qui les définissent sont de la forme :

$$ \text{BasicDF} ::= \text{Inst} | \text{pre} $$

où Inst dénote des fonctions instantanées, ou combinatoires, et Pre est l'unique moyen de faire référence au passé. Les fonctions combinatoires sont obtenues comme des extensions aux séquences de fonctions point à point. Par exemple, $f(x) = 2 \times x$ est étendue en une fonction f telle que : $o = f(i) \iff \forall k \ge 0, o_k = 2 \times i_k$. La fonction pre est définie par : $\forall k > 0, o_k = i_{k-1}$. La fonction sémantique $S_{df}$ : DF $\longrightarrow \mathcal{M}$ vérifie :

$$ S_{df}(\{o = B(i), o' = B'(i'), \dots\}) = S_{df}(B) \times S_{df}(B') \times \dots $$

Dans le langage mixte, on autorise la description de comportements de base par des systèmes de transitions ou par des équations décrivant des fonctions à mémoire bornée; on permet la composition par le produit synchrone ou par la connexion en réseau d'opérateurs. D'où la grammaire :

$$ 
\begin{align*}
\text{Mixed} &::= \text{MixedBasic} | \text{Mixed} \| \text{Mixed} | \{\text{eq}\} \\
\text{MixedBasic} &::= \text{BasicA} | \text{BasicDF} \\
\text{eq} &::= o = \text{MixedBasic}(i)
\end{align*}
$$

On fusionne aisément les deux sémantiques.

### 7.2.4 Implantation

Lorsque l'on s'intéresse à une utilisation pratique de ces idées simples, il faut tout de même résoudre quelques petits problèmes. ARGOS, et surtout LUSTRE, ne sont pas aussi simples que cette présentation abstraite pourrait le faire croire. Nous proposions dans [JLMR94, JLMR93] un sous-ensemble raisonnable de LUSTRE qui se prête sans difficulté à l'implantation des idées exposées ci-dessus. Nous montrions comment compiler le langage mixte en deux étapes : une traduction des fragments ARGOS en LUSTRE, accompagnée d'une modification structurelle des fragments LUSTRE, suivies de la compilation LUSTRE usuelle.

La modification des fragments LUSTRE n'est pas mentionnée dans la présentation abstraite ci-dessus, pour les besoins de laquelle nous avions oublié le raffinement. Elle consiste à rendre les noeuds "ré-initialisables", pour pouvoir les utiliser dans un raffinement ARGOS. Cela consiste à rajouter à chaque noeud LUSTRE deux signaux d'entrée booléens qui déterminent l'état d'activité
du noeud pendant et après la réaction courante. Cette opération est décrite au chapitre 5 à propos
de la traduction du raffinement ARGOS en équations booléennes, je ne la détaille donc pas ici.

La traduction structurelle d'ARGOS en LUSTRE pose le problème de l'analyse de causalité des
fragments ARGOS, avant (ou pendant) la traduction en LUSTRE. Ce problème n'était toujours pas
réglé dans [Jou94]. L'étude d'une traduction d'ARGOS en équations booléennes sans contraintes
(c'est-à-dire autorisant des cycles de définitions), et l'utilisation de l'outil BAC (voir la section
*Analyse de causalité sur la forme équationnelle*, au chapitre 2) ont permis de mieux cerner
les problèmes. Le chapitre 8 expose les problèmes et montre comment intégrer une analyse de
causalité des fragments ARGOS dans un schéma d'implémentation où LUSTRE et ARGOS sont
traduits en DC. Nous envisageons maintenant une véritable programmation ARGOS+LUSTRE,
en utilisant LUSTRE sans restrictions et en garantissant aux fragments ARGOS une analyse de
causalité complète.

7.3 Conclusions

L'application idéale des idées exposées ici serait un environnement de programmation et vérification des systèmes réactifs dans lequel les programmes pourraient être décrits indifféremment en LUSTRE, ARGOS, ESTEREL, REGLO, etc.

En attendant qu’un tel objet soit effectivement réalisé, les études menées sur la programmation multi-langages dans des cas particuliers — mélange ARGOS+LUSTRE décrit au chapitre 8, mélange ARGOS+ESTEREL décrit au chapitre 9 — peuvent être utilisées pour imaginer l'enrichissement d'un langage par des structures issues d'un autre. La première idée de ce genre, issue de l'étude ARGOS+LUSTRE, est d'introduire des équations en ARGOS. La deuxième idée provient de l'étude ARGOS+ESTEREL, et consiste à offrir une notation pour les interruptions préemptives. Ces extensions sont présentées au chapitre 6.