Charles André— Robert De Simone
Les formalismes impératifs synchrones (Esterel et SyncCharts) permettent d’exprimer des comportements réactifs complexes. La connaissance de la sémantique de ces modèles est indispensable si on veut exploiter pleinement leur richesse expressive et éviter les “cycles de causalité”. La première partie de ce papier rappelle les grandes lignes de la sémantique constructive. Cette sémantique est utilisée dans la seconde partie pour analyser des propriétés dans l’instant portant sur les ordres partiels d’exécutions d’actions simultanées. Il est montré comment les fonctionnalités du compilateur, issues de la sémantique constructive, permettent une telle analyse. La technique est illustrée par un exemple de zFIFO (0 fall-through time FIFO queue) un système qui présente de nombreuses actions simultanées dont l’ordonnancement est critique.
systèmes réactifs, synchrone, ESTEREL, SYNCCHARTS, sémantique constructive, vérification de modèle.
@INPROCEEDINGS{sp:msr2001,
AUTHOR = "C. Andr\'e and R. {De Simone}",
TITLE = "Programmation synchrone : Propriétés dans une réaction",
sorte= "colna" ,
BOOKTITLE = {MSR'2001},
PUBLISHER= {Hermès Science Publications},
PAGES = {547--561},
YEAR = {2001},
ADDRESS = {Toulouse (F)},
MONTH = {17-19 octobre}
}