A compositional verification method from a high-level resource-management
standpoint is presented for dense-time concurrent systems and implemented in
the tool of SGM (State-Graph Manipulators) with graphical user interface.
SGM packages sophisticated verification technology into state-graph
manipulators and provides an user interface which views state-graphs
as basic data-objects. Hence users do not have to be verification theory
experts and do not have to trace inside state-graphs to analyze state and path
properties to make the best use of verification theory.
Instead users can construct their own verification strategies
based on observation on the state-graph complexity changes
after experitmenting with some combinations of manipulators.
Moreover, SGM allows users to control the complexity of state-graphs,
through iterative state-graphs merging and reductions,
before they become out of control. Reduction techniques specially designed
for the context of state-graph iteration composition
and shared variable manipulations are developed and used in SGM.
Experiments on different benchmarks to show SGM performance are reported.
An algorithm based on group theory to pick a
manipulator combination is presented.