User-Friendly Verification
Abstract
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.
KEYWORDS:
timed automata, TCTL, model-checking, state-space explosion,
verification tool, concurrent real-time systems