Aldebaran: A Tool for Verification of Communicating Processes

Jean-Claude Fernandez

Rapport SPECTRE, C14, Laboratoire de Génie Informatique - Institut IMAG, Grenoble, September 1989

Abstract:

Aldebaran is a tool for verifying communicating systems represented as labeled transition systems. Verification techniques are based on the comparison of two labeled transition systems according to an equivalence relation. Strong bisimulation, weak bisimulation, acceptance model equivalence and safety equivalence are supported by Aldebaran. Communicating systems are described hierarchically by parallel composition of processes. Synchronization (or communications) between labeled transition systems set in parallel are determined by a synchronization algebra. To allow partial synchrony, a restriction operator is defined. To verify external specification, an abstract mechanism is used. A major goal of the tool is to provide different equivalence relations and efficient algorithms implementing these.

28 pages

PDF

PostScript