Abstraction and Verification of Cooperating Systems
The Simple Homomorphism Verification Tool

Methods and tools where developed in the research group Cyber-Physical Systems.

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 cooperating 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. This paper gives an overview of our concepts presented in more detail in [13,11,10,9]. A tutorial [12] and a manual [1] are available.





© 2008
Fraunhofer-Gesellschaft
feedback to CSS Home Page | Imprint | Privacy Statement