Cette these contribue a l'etude des semantiques pour la specification et la verification des systemes reactifs. Plus precisement, nous comparons des semantiques comportementales, basees sur la bisimulation avec celles induites par des logiques modales du temps arborescent. Dans la premiere partie, nous considerons les modeles d'entrelacement pour les systemes sequentiels non-deterministes. Plusieurs travaux recents ont montre que dans le cadre des systemes a branchement infini (c-a-d. non-determinisme infini), l'equivalence de bisimulation (forte), reconnue comme l'equivalence semantique de base pour le temps arborescent, est strictement plus fine que celles induites par les logiques du temps arborescent (nous savons depuis longtemps qu'elles coincident sous l'hypothese de branchement fini). Nous utilisons les Processus Ordinaux de Klop, et, en derivant une notion de pouvoir de distinction d'une equivalence semantique, nous montrons dans un cadre parfaitement unifie que la bisimulation est plus fine que les logiques du temps arborescent, mais aussi que pour une large classe de combinateurs, les congruences engendrees par les logiques restent strictement plus faibles que la bisimulation. Dans la deuxieme partie de la these, nous considerons les modeles d'ordre partiel pour les systemes paralleles, dans lesquels on dispose d'une definition satisfaisante de l'operation de raffinement de programme (cette notion est liee a la methode classique de conception hierarchique des programmes). Parmi les equivalences semantiques de la litterature, la history preserving bisimulation est particulierement interessante car c'est une congruence pour l'operation de raffinement quand les systemes n'ont pas d'action invisible. En utilisant une caracterisation de cette equivalence en termes d'une bisimulation avant-arriere, nous exhibons deux caracterisations logiques, ainsi qu'un algorithme de traduction entre ces deux logiques. Nous etudions aussi plusieurs variantes de cette bisimulation avant-arriere. Enfin, nous elargissons le champ de travail en considerant les modeles d'ordre partiel avec actions invisibles. Nous montrons que la bisimulation avant-arriere susmentionnee, adaptee a ce cadre, coincide avec la branching bisimulation sur les arbres causaux, mais aussi avec deux nouvelles equivalences~: l'equivalence de mixed-ordering branching et la history preserving branching bisimulation, que nous etudions.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00005141 |
| Date | 08 January 1993 |
| Creators | Pinchinat, Sophie |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0021 seconds