Abstract FR:

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 modele reseau de Petri interprete (pouvant servir a produire du code executable) puis vers un modèle automate d'etats finis (permettant la vérification formelle de programmes LOTOS soit par réduction ou comparaison modulo des relations d'equivalence, 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 reseau). Elle met en oeuvre 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