formation par la recherche / formation doctorale / enseignement, stages / sujets de thèses

Méthodes de réalisation répartie de spécifications partielles de systèmes réactifs dans le langage BDL

Localisation :Irisa, Rennes

Equipe Pampa, Ep-Atr

Responsables : Benoît CAILLAUD (tél. direct : 02 99 84 74 07, email : Benoit.Caillaud@irisa.fr)
Albert BENVENISTE (tél. direct : 02 99 84 72 35, email : Albert.Benveniste@irisa.fr)

Sujet : Les phases initiales de la conception de logiciels répartis reposent à l'heure actuelle sur l'utilisation de spécifications partielles exprimées dans des notations telles que les diagrammes de séquences (abréviation MSC, pour message sequence charts), ou les contraintes OCL de la notation UML. Le langage BDL [1] permet également l'expression et la manipulation formelle de spécifications partielles. Chaque classe ou composant d'un modèle UML peut être muni d'une spécification BDL prenant la forme d'une famille de graphes orientés dont les sommets sont des événements valués pouvant être gardés par des conditions. Ces graphes spécifient des contraintes d'ordonnancement entre leurs événements sommets. BDL récupère en fait la technologie développée pour les langages synchrones (Esterel, Lustre, et en l'occurrence plus particulièrement Signal), tout en offrant une notion d'abstraction appropriée aux spécifications incomplètes. Le point nouveau, qui repose sur des résultats fondamentaux récents, est la possibilité d'interpréter un terme BDL indifféremment selon un mode synchrone ou asynchrone, en fonction de l'architecture du système modélisé et de la sémantique de communication entre objets.

Le travail de thèse portera sur l'élaboration de méthodes de synthèse de programmes répartis à partir de spécifications partielles BDL, qui prennent en compte l'environnement d'exécution des programmes. Il pourra s'inspirer à la fois des résultats récents sur la désynchronisation de systèmes de transitions synchrones [2] ainsi que de techniques classiques de synthèse de superviseurs de systèmes à événements discrets [3].

Bibliographie :

[1] Home Page of the BDL Project, http://www.irisa.fr/pampa/bdl/

[2] A. Benveniste, B. Caillaud, P. Le Guernic, FROM SYNCHRONY TO ASYNCHRONY, CONCUR'99, Lecture Notes in Computer Science, vol. 1664, pp. 162-177, August 1999.

[3] P.J.G. Ramadge, W.M. Wonham, The control of discrete event systems, Proceedings of the IEEE, vol.77, no.1 p. 81-98, 1988