Conference
Verifying Statecharts with State Invariants
Abstract
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 …
Authors
Sekerinski E
Pagination
pp. 7-14
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Publication Date
March 1, 2008
DOI
10.1109/iceccs.2008.40
Name of conference
13th IEEE International Conference on Engineering of Complex Computer Systems (iceccs 2008)