The SH-Verification Tool — Abstraction-Based Verification of Co-operating Systems
Peter Ochsenschläger, Jürgen Repp, Roland Rieke, Ulrich Ultes‐Nitsche · Formal Aspects of Computing · 1998
Abstract. The sh-verification tool comprises computing abstractions of finite-state behaviour representations as well as automata and temporal logic based verification approaches. To be suitable for the verification of so called co-operating systems, a modified type of satisfaction relation (approximate satisfaction) is considered. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. The well known state space explosion problem is tackled by a compositional method combined with a partial order method.