Visual verification of safety and liveness

Abstract

An exceptionally user-friendly approach to computer-aided validation / verification of concurrent and reactive systems is presented. In it, the user needs not express his verification questions formally in detail. Instead, he specifies a point of view to the system by choosing a subset of its externally observable actions. An automaton abstracts and reduces the behaviour of the system according to the choice, and shows the result graphically on a computer screen. The resulting picture represents all executions of the system, as seen from the chosen point of view. Thus the information in it is as comprehensive as that obtained by ordinary verification. On the other hand, like ordinary testing, the method makes it possible for a system designer to get rapid feedback with ease, to “just try the system and see how it behaves”. The article concentrates on practical and philosophical issues regarding the method and contains a detailed example.