Automated Verification of Refinements of
Concurrent and Distributed Systems

Peter Herrmann, Thomas Kraatz,
Heiko Krumm, Miriam Stange

    Dept. of Computer Science, Dortmund University, D-44221 Dortmund, Germany
    Phone +49 231 755-4836, Fax -4730, herrmann@ls4.informatik.uni-dortmund.de

Research Report 541/1994
March 28, 1994


Abstract

In order to support the practical application of formal verification,
a fully-automated verification tool has been developed which is used
for the design of communication systems and distributed applications.
The tool refers to the concept of Refinement Mappings, which state
correspondences between specifications of more abstract and more de-
tailed systems. It checks the correctness of the refinements of finite-
state transition systems with respect to safety and liveness properties.
The liveness properties of refinements are described in terms of the
strong-fairness and weak-fairness of transitions. The liveness proper-
ties to be checked are described in terms of weak-fair transitions. To
tackle the problem of `state explosion' the tool performs on-the-fly
model checking by structuring the reachability graph of the refine-
ment into strongly-connected components.  We report on the basic
algorithm, its implementation, and some performance characteristics
yielded from the verification of data transfer protocols.