accueil

 carte
 

    Publications 1992


    L. Besnard.
    Compilation de Signal: horloges, dépendances, environnements.  Thèse de l'Université de Rennes I, IFSIC, Septembre 1992.
    Résumé : 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.  Thèse de l'Université de Rennes I, IFSIC, Décembre 1992.
    Résumé : 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.

    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.

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