Publications 1992

L. Besnard.
Compilation de Signal: horloges, dépendances, environnements. Phd thesis, Université de Rennes I, IFSIC, September 1992.
Abstract : Le travail décrit dans ce document s'inscrit dans le cadre du développement d'un contexte de programmation d'applications temps-réel. Il présente d'une part, la mise en oeuvre du langage synchrone SIGNAL orienté flot de données et la structure de l'environnement SIGNAL, d'autre part. Le point important dans la compilation de SIGNAL est d'assurer le respect de la synchronisation des calculs exprimée par le langage. Ceci conduit l'intégration dans le compilateur d'un système formel de preuves de propriétés de programmes ; c'est-à-dire un outil automatique d'analyse et de synthèse de contraintes temporelles et de dépendances de calculs. Dans les travaux présentés, on s'intéresse à l'ensemble des propriétés invariantes dans le temps. La vérification partielle de la correction du processus vis-à-vis de ses synchronisations est effectuée en utilisant une technique de réécriture ; la synthèse partielle d'expressions explicites du contrôle se traduit par une forêt d'arbres dont les racines sont éventuellement arguments de contraintes non résolues et les noeuds internes des expressions explicites. L'ordonnancement des calculs est explicité dans un graphe structuré conformément à la hiérarchie définie. La structure de l'environnement SIGNAL ainsi que la méthodologie de développement utilisée sont ensuite présentées. Nous décrivons la double structuration (fonctionnelle et hiérarchique) de la réalisation et l'environnement de développement du compilateur qui a été construit sous le système MENTOR (éditeur dirigé par la syntaxe). Cette méthodologie de développement permet d'atteindre un bon degré de portabilité de l'application.

B. Dutertre.
Spécification et preuve de systèmes dynamiques. Phd thesis, Université de Rennes I, IFSIC, December 1992.
Abstract : SIGNAL est un langage synchrone, à flots de données, destiné à la spécification de systèmes réactifs et temps-réel. Certains domaines d'application envisagés exigent une grande fiabilité et une grande sûreté de fonctionnement. Pour répondre à ces exigences, il est nécessaire de pouvoir prouver des propriétés critiques des programmes. Cette thèse a pour objet l'étude de méthodes et d'outils de validation et de preuve des systèmes réactifs décrits en SIGNAL. La vérification de propriétés repose sur une représentation équationnelle de la synchronisation et de la logique des programmes, sous la forme de systèmes dynamiques dans le corps des entiers modulo trois. L'approche retenue consiste à traduire les propriétés des systèmes réactifs en propriétés algébriques équivalentes qui peuvent être vérifiées par des outils de calcul formel. Cette approche permet notamment la vérification de propriétés exprimées soit par des formules de logique temporelle soit par d'autres systèmes dynamiques. Nous montrons comment les graphes de décision binaires utilisés dans le cadre des algèbres booléennes peuvent être étendus aux fonctions polynômiales sur un corps finis et comment cette représentation permet une mise en oeuvre performante des calculs algébriques.

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors and by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Webmaster : epatr_webmaster@irisa.fr
Ces pages sont créées automatiquement par le
programme bib2html du projet Vista de l'IRISA-INRIA Rennes