Un langage d'horloge pour spécifier et analyser les réactions
synchrones
-
Résumé :
Les langages synchrones, dédiés à la spécification
des systèmes réactifs, considèrent un temps discret
: une échelle de temps est appelée horloge. L'approche dite
multi-horloge polychrone (représentée par le langage flot
de données Signal) est la plus générale : indissociable
des horloges, elle permet de décrire un système ouvert à
tous les stades de sa conception, de la spécification incomplète
et non déterministe au programme exécutable. Dans cette approche
une variable possède à tout instant un statut de présence/absence
et uniquement en cas de présence une valeur significative. Les outils
de vérification existants dénotent l'absence des variables
par une valeur additionnelle qui étend leur domaine et est difficile
à traiter. On attaque ce problème en proposant un langage
d'horloge qui peut exprimer toute assertion combinatoire flot de données
(par exemple spécifications Signal ou Lustre, propriétés
de sûreté sans état) et permet de mener les analyses
sans valeur additionnelle.
-
Bibtex entry:
@InProceedings{nebutAFADL03,
author = {M. Nebut},
title = {Un langage d'horloge pour analyser et spécifier
les réactions synchrones},
booktitle = {Approches Formelles pour l'Assistance au
Développement de Logiciels, AFADL'03},
note = {In french}
}
Pdf
file (225Ko)
Mirabelle Nebut
Last
modified: Mon Dec 30 12:37:46 /etc/localtime 2002