© 1995 Benoit Girard. Toute reproduction interdite sans consentement écrit de l'auteur
Cette page a comme but la présentation d'une partie de ma thèse de maîtrise. Celle-ci porte sur l'analyse de systèmes répartis et de l'implantation de logiciels permettant cette analyse. Le modèle présenté est celui des systèmes de transitions d'Arnold-Nivat. L'objectif ici visé est de permettre la validation formelle d'applications concurentes.
Nous vous suggérons tout d'abord de lire l'introduction au modèle d'Arnold-Nivat qui résume rapidement comment on peut l'utiliser pour modéliser des systèmes répartis.
Un modèle qui ne serait que descriptif ne servirait à rien. Il existe donc une logique formelle permettant d'exprimer des propriétés sur les systèmes de transitions qui servent à effectuer la validation des modélisations proposées. Nous avons dressé une liste des propriétés générales les plus utilisées, tel qu'elles sont exprimées dans la syntaxe de cette logique.