Verifying invariants by approximate image computation. (English) Zbl 0907.68121
Moller, Faron (ed.), Verification of infinite state systems, Infinity ’97. Selected papers from the 2nd international workshop, Bologna, Italy, July 11--12, 1997. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 9, 13 p. (1997).
Summary: Automatic formal verification of safety properties typically requires computing reachable states of a system. A more efficient (and less automatic) alternative is to check whether a user suggested superset of reachable states is an invariant, i.e. whether it contains its image specified by the transition relation of the system. Still, this approach may be prohibitively expensive due to the complexity of image computation. To alleviate this problem we suggest to use approximate image computations, and we show that even though the approximation computes a superset of the image, it can, in certain cases, be used to answer categorically the question whether the suggested invariant contains its image. More precisely, we first establish sufficient conditions that the approximate image commutation and the suggested invariant need to satisfy in order to always reach a conclusive result of the verification process. Then, we use these results to show that the three approximate image computation methods proposed previously for approximate reachability analysis could be used for exact invariant verification. For the entire collection see [Zbl 0903.00065
|68Q60||Specification and verification of programs|
|68U10||Image processing (computing aspects)|