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, Computer system organization, Network protocols
68Q60, Computer science - Theory of computing, Specification and verification
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique, 1989, Grenoble 1 Item type: Thèse
Tags from this library: No tags from this library for this title. Log in to add tags.
Holdings
Current library Call number Status Date due Barcode
CMI
Salle S
Thèses GAR (Browse shelf(Opens below)) Available 10490-02
CMI
Salle S
Thèses GAR (Browse shelf(Opens below)) 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 on this title.

to post a comment.