T. Amagbegnon. Forme canonique arborescente deshorloges de Signal. Thèse de l'université de Rennes 1, Novembre 1995.
Charger l'article :
Gziped Postscript
Copyright : Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.
Cette thèse traite des techniques de calcul booléen mises en oeuvre dans la compilation du langage SIGNALC'est un langage synchrone destiné à la programmation de systèmes réactifs. La compilation d'un programme SIGNAL repose sur la résolution d'un système d'équations booléennes qui représente son contrôle. La résolution mise en oeuvre dans le compilateur tire parti de la spécificité des équations issues des programmes SIGNAL et un système d'équations résolu est représenté par un arbre dont chaque noeud est un BDD\ (Diagramme Binaire de Décision). Nous décrivons en détail la forme des systèmes d'équations booléennes de SIGNAL et motivons le choix d'une représentation arborescente. Nous montrons à l'aide d'une factorisation à supports disjoints que cette représentation arborescente est une forme canonique des systèmes d'équations résolus de SIGNAL. Ensuite, nous développons sur cette structure de données des algorithmes de minimisation logique pour générer du code efficace. Enfin, nous développons des algorithmes de projection de systèmes d'équations en vue d'une évolution vers de la compilation séparée et de la preuve de propriétés de sûreté. Tous ces nouveaux algorithmes ont été mis en oeuvre et comparés avec les algorithmes préexistants.
Keywords:
@PhdThesis{amagbegnon95c,
Author = {Amagbegnon, T.},
Title = {Forme canonique arborescente deshorloges de Signal},
School = {université de Rennes 1},
Month = {November},
Year = {1995}
}
Charger la référence EndNote (.ref)
This page is part the Espresso project web site.
It has been automatically generated using the bib2html program.