Verifying Statecharts with State Invariants

Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating "many small" verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.