An improvement in formal verification

Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usually implemented as a depth-first search of the product state-space of all components in the system, with each (finite state) component modeling the behavior of one asynchronously executing process. Formal verification is achieved by coupling the depth-first search with a method for identifying those states or sequences of states that violate the correctness requirements. It is well known, however, that an exhaustive depth-first search of this type performs redundant work. The redundancy is caused by the many possible interleavings of independent actions in a concurrent system. Few of these interleavings can alter the truth or falsity of the correctness properties being studied. The standard depth-first search algorithm can be modified to track additional information about the interleavings that have already be...

• Type: Conference
• Year: 1994
• Where: FORTE
• Authors: Gerard J. Holzmann, Doron Peled
• Keywords: Concurrent System, Depth-first Search, Finite State, FORTE 1994, FORTE 2007