Efficient and User-Friendly Verification

Farn Wang
Pao-Ann Hsiung
Institute of Information Science,
Academia Sinica,
Taipei, Taiwan.
Department of Computer Science and Information Engineering,
National Chung Cheng University,
Chiayi, Taiwan.
( IEEE Transactions on Computers , Vol. 51, No. 1, pp. 61-83, January 2002.)


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.