Méthodes de vérification de spécifications comportementales : étude et mise en œuvre
Laurent Mounier · HAL (Le Centre pour la Communication Scientifique Directe) · 1992
This work deals with the verification of behavioural specifications for parallel programs, and, more precisely, with the design of efficient algorithms for the comparison of two labelled transition systems modulo a simulation or a bisimulation relation. First, we recall the principle of the classical decision procedures, based on partition refinement algorithms. This approach requires to previously build the transition relations of the two systems before the comparison phase, which constitutes a practical limitation. Consequently, we propose an original algorithm, based on a depth-first traversal of a synchronous product of the two systems, which allows to perform the comparison ``on the fly'', without explicitly building or storing the two transition relations. This ``on the fly'' comparison algorithm has been implemented within the Aldebaran verification tool with for various relations: strong bisimulation, observational equivalence, tau*a-bisimulation, delay bisimulation and branching bisimulation, as well as safety equivalence and preorder. Its application to the verification of several Lotos programs confirms the interest of this approach in comparison with the more classical ones. Finally, we are also concerned with diagnostic generation when the two labelled transitions systems are not equivalent: the decision procedures implemented within Aldebaran provide a set of discriminating execution sequences, which are minimal with respect to a given order relation.