Interprétation abstraite des systèmes de transitions
synchrones
Localisation : IRISA
Equipe(s) : EP-ATR
Responsable(s) : Jean-Pierre Talpin (poste 7436)
Paul Le Guernic (poste 7242)
Mots-clés : Systèmes de transitions, programmation
synchrone, analyse de programmes.
La spécification et la mise en oeuvre de systèmes
réactifs nécéssite une analyse comportementale
précise
afin d’assurer la sureté de fonctionnement et de garantir
l’exécution efficace. L’utilisation de langages
de
programmation synchrone facilitent la réalisation de systèmes
critiques remplissant ces critères.
Dans ce processus d’analyse, une représentation symbolique
du système, par exemple sous forme d’arbres
de décision binaires, ou bien sous forme de systèmes
de transitions hiérarchiques, joue un rôle primordial
afin d’en analyser, d’en vérifier et d’en
optimiser la structure.
L’objectif est ici de définir une interprétation
abstraite des systemes de transition synchrones permettant
d’assurer le déploiement correct de spécifications
synchrones sur des architectures distribuées. Il s’agit
du
probleme de désynchronisation, que nous aborderons dans le
cas de systemes de transitions dits infinis. Nous
pourrons ensuite envisager le probleme de bon-déploiement
comme un cas particulier de model-checking et
définir plus généralement un model-checking
abstrait des systemes de transition synchrones.
Références :
"Timed polyhedra analysis for synchronous languages".
Besson, F., Jensen, T., Talpin, J.-P. Static Analysis
Symposium. Springer Verlag, September 1999.
"Hierarchic normal forms for desynchronization". Talpin,
J.-P., Benveniste, A., Caillaud, B., Le Guernic,
P.Research Report No. 3822. INRIA, December 1999.
|
