Sciweavers

FORTE
1994

An improvement in formal verification

13 years 5 months ago
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...
Gerard J. Holzmann, Doron Peled
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1994
Where FORTE
Authors Gerard J. Holzmann, Doron Peled
Comments (0)