Compte rendu de la réunion de l'ARC TOLÈRE

Participants :

• Gerard Berry (MEIJE)
• Robert de Simone (MEIJE)
• Annie Ressouche (MEIJE)
• Mihaela Sighireanu (SOSSO)

Ordre du jour :

• Présentation de l'outil DC2SDX pour la traduction du format DC vers SynDEx
• Discussion sur l'interconnexion des outils Esterel et SynDEx
• Présentation des outils MCL_EXPAND et EVALUATOR pour la vérification des formules de logique temporelle en ORCCAD et Esterel

Présentation de l'outil DC2SDX

Mihaela Sighireanu a présenté l'outil DC2SDX, le traducteur du format commun des langages synchrones DC vers le format d'entrée de SynDEx. Cet outil réalise l'interconnexion entre l'environnement ORCCAD (qui génère des programmes Esterel) et SynDEx.

La présentation a inclu une démonstration de cet outil sur un exemple Esterel classique. Cette démonstration a illustré deux des problèmes auxquels la traduction actuelle se confronte :

• La compilation d'Esterel vers DC (outil scdc) n'est pas toujours optimale. En effet, sur quelques exemples elle génère des équations DC ayant la forme "equ: F1 F2 at: $@1", ce qui correspond à un renommage de flots.

  Pour résoudre ce problème, la nouvelle version de DC2SDX (en cours de réalisation) optimise la traduction de ce type d'équations.

• Les automates de contrôle d'Esterel sont traduits en DC "aplati" (sans appels de noeuds) en utilisant comme opérations élémentaires les fonctions booléennes (and, or, ...). Or ceci représente une granularité trop fine pour SynDEx, qui est conçu pour la distribution d'opérations plus complexes.

  Pour résoudre le problème de la granularité trop fine des descriptions, des travaux sont en cours pour supporter la description modulaire (hiérarchique) en SynDEx. Toutefois, une autre solution (alternative et/ou complémentaire) pour ce problème est d'exploiter la modularité des descriptions Esterel ainsi que les outils de minimisation dédiés, afin d'obtenir des descriptions DC modulaires et/ou plus compactes. Par exemple, les descriptions DC obtenues à partir de programmes Esterel pourraient être minimisées en utilisant les outils BLIF et ensuite traduites en DC et SynDEx. Cette solution n'est pas réalisable à présent, car il n'existe pas encore d'outil de traduction du format BLIF vers le format DC.

Discussion sur l'interconnexion des outils Esterel et SynDEx

Suite à cette présentation, deux solutions concrètes ont été proposées par l'équipe MEIJE pour résoudre le problème de la granularité. Les deux solutions permettent de retrouver la modularité des descriptions Esterel au niveau du format DC.

• La première solution est applicable pour les descriptions Esterel pures (sans signaux valués). Elle utilise l'outil de compilation hiérarchique d'Esterel (esterel -hierarchy) dont la version beta sera très bientôt disponible.

  La figure ci-dessous indique les étapes de cette solution. A partir d'une description Esterel pure (spec.strl), la compilation en utilisant l'option "-hierarchy" permettra d'obtenir dans le format désiré (ici BLIF) une description pour chaque sous-module de la description initiale (spec_1.blif, spec_2.blif) et une description pour le module principal (spec_0_body.blif). Ces descriptions modulaires peuvent être éventuellement minimisées (en utilisant les outils BLIF, ici blifopt). Elles doivent être ensuite traduites vers Lustre (commande bliftrans -lustre) et puis en DC (commande lus2dc). On obtient ainsi plusieurs modules DC, à priori plus compactes que la description initiale, qui pourront ensuite être traduites vers SynDEx :

  

• La deuxième solution est applicable à toutes les descriptions Esterel, mais elle nécessite la modification de la version actuelle du compilateur d'Esterel vers DC (scdc) afin de supporter la hiérarchie. La future version de ce compilateur devrait générer des appels de noeuds correspondant aux modules Esterel.

Présentation des outils MCL_EXPAND et EVALUATOR

Mihaela Sighireanu a présenté un travail effectué en collaboration avec Radu Mateescu, sur la vérification des formules de logique temporelle pour les applications robotiques. Les transparents de cette présentation sont disponibles ici.

Ce travail s'inscrit dans l'objectif (voir [1]) d'interconnexion entre l'environnement dédié applications robotiques ORCCAD et la boîte à outils de vérification CADP. Le schéma suivant résume la manière dont cette interconnexion est réalisée :

Ainsi, les propriétés des applications robotiques sont décrites à l'aide de macro-propriétés ("patterns") simples, qui peuvent être ensuite combinées en utilisant les connecteurs logiques usuels (and, or, ...). Les macro-propriétés permettent aux utilisateurs d'ORCCAD, qui ne sont pas forcement des spécialistes de la logique temporelle, d'écrire des propriétés logiques d'une manière très simple.

En utilisant un macro-expanseur, ces propriétés sont traduites vers des formules de mu-calcul modal régulier (une variante de PDL). Un exemple de macro-expansion vers ACTL est donné ici.

Le mu-calcul régulier est ensuite traduit par l'outil MCL_EXPAND (de la boîte à outils CADP) vers un système d'équations modales (SEM). En partant du SEM et de l'automate généré à partir de l'application robotique (par ORCCAD, puis Esterel), l'outil EVALUATOR (de la boîte à outils CADP) vérifie la formule donnée. Le résultat de cette vérification est un booléen (oui ou non la formule est vérifiée) et un diagnostic (la partie de l'automate vérifiant la formule).

Comme le schéma ci-dessus le montre, les outils MCL_EXPAND et EVALUATOR peuvent être également utilisés pour la vérification des propriétés de logique temporelle pour les programmes Esterel, en alternative aux outils FC2Tools.

L'exposé a été accompagné d'une démonstration de la vérification des propriétés de logique temporelle en utilisant CADP pour l'exemple de l'arbitre à quatre noeuds fourni dans la distribution de Xeve (outil de FC2Tools). Cette démonstration a souligné les différences entre les approches utilisées respectivement par CADP et par Xeve :

• Xeve considère la logique temporelle linéaire, tandis que EVALUATOR supporte la logique temporelle branchue.

• Xeve utilise les automates observateurs pour la vérification des propriétés logique, tandis que EVALUATOR utilise les systèmes d'équations booléennes.

• EVALUATOR accompagne sa réponse par un diagnostic, ce qui n'est pas le cas de Xeve.

Les discussions qui ont suivi l'exposé ont permis de fixer un point technique dans la sémantique des automates fc2 obtenus à partir de programmes Esterel. En effet, pour traduire la macro-propriété "le signal a est présent dans la transition courante", il faut utiliser l'expression régulière

not ('.*#a.*')

'.*?a.*' ou '.*!a.*'

'.*#a.*'

Références

[1] Compte rendu de la réunion TOLÈRE du 26 octobre 1998.

Envoyez vos commentaires à Mihaela Sighireanu à Mihaela.Sighireanu@inria.fr.