Compilation et vérification de programmes LOTOS / par Hubert Garavel ; sous la direction de Jacques Voiron

Bibliogr. p. 259-265

Thèse de doctorat informatique 1989 Grenoble 1

LOTOS (Language Of Temporal Ordering Specification) est un langage de description de systèmes parallèles communicants, normalisé par l'ISO et le CCITT afin de permettre la définition formelle des protocoles et des services de télécommunications. Le langage utilise des types abstraits algébriques pour spécifier les données et un calcul de processus proche de CSP et CCS pour exprimer le contrôle. Cette thèse propose une technique de compilation permettant de traduire un sous-ensemble significatif de LOTOS vers un modèle réseau de Petri interprète (pouvant servir a produire du code exécutable) puis vers un modèle automate d’états finis (permettant la vérification formelle de programmes LOTOS soit par réduction ou comparaison modulo des relations d’équivalence, soit par évaluation de formules de logiques temporelles). La méthode employée diffère des approches usuelles basées sur la réécriture de termes, qui construisent directement le graphe d'états correspondant à un programme LOTOS. Ici au contraire la traduction est effectuée en trois étapes successives (expansion, génération et simulation) s'appuyant sur des modèles sémantiques intermédiaires (le langage SUBLOTOS et le modèle réseau). Elle met en œuvre une analyse statique globale du comportement des programmes. Elle prend en compte les données, celles-ci devant être compilées au moyen d'algorithmes déjà existants. Ces principes de compilation ont été entièrement implémentés dans le logiciel CAESAR. Les performances obtenues confirment l'intérêt de la méthode