User-Friendly Verification

Pao-Ann Hsiung and Farn Wang
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
( Joint International Conference FORTE/PSTV'99 , Beijing, China, October 5-8, 1998.)


Model checking often faces the problem of reducing the large exponential sizes of state-space representations. Several reduction techniques such as bisimulation equivalence, partial-order semantics, and symmetry-based reduction have been proposed, but existing tools do not completely allow a user the flexibility in manipulating state spaces. We propose a new user-friendly verification environment where a user has full control on what techniques to apply and in what sequences to apply them. We have implemented the environment in a tool called State-Graph Manipulators (SGM). SGM packages verification techniques into efficient, reusable, modular manipulators, that act on high-level state-space representations called state-graphs. Further, we are also proposing four new state-space reduction techniques: variable shielding, read-write analysis, internal transitions bypassing, and sibling transition multiplicity reduction. They are implemented into SGM and experiments conducted to show their usefulness.

timed automata, TCTL, model-checking, state-space explosion, verification tool, concurrent real-time systems