Normal view MARC view ISBD view

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

Auteur principal : Garavel, Hubert, 1963-, AuteurAuteur secondaire : Voiron, Jacques, Directeur de thèseAuteur secondaire collectivité : Université Joseph Fourier, Grenoble, Etablissement de soutenanceType de document : ThèseLangue : français.Pays : France.Éditeur : [S.l.] : [s.n.], 1989Description : 1 vol. (XVI-265 p.) ; 30 cmISBN : 2726106218.Bibliographie : Bibliogr. p. 259-265.Sujet MSC : 68M12, Network protocols, Computer science -- Computer system organization
68Q60, Specification and verification (program logics, model checking, etc.), Computer science -- Theory of computing
97A70, Theses and postdoctoral theses, Mathematics education - General, mathematics and education
Note de thèse: Thèse de doctorat, informatique, 1989, Grenoble 1
Tags from this library: No tags from this library for this title. Log in to add tags.
Current location Call number Status Date due Barcode
CMI
Salle S
Thèses GAR (Browse shelf) Available 10490-02
CMI
Salle S
Thèses GAR (Browse shelf) Available 10490-01

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

There are no comments for this item.

Log in to your account to post a comment.