Verification of Statecharts Using Data Abstraction

摘要: We present an approach for verifying Statecharts including infinite data spaces. devise a technique checking that formula of the universal fragment CTL is satisfied by specification written as Statechart. The based on property-preserving abstraction additionally preserves structure. It prototypically implemented in logic-based framework using theorem prover and model checker. This paper reports following results. (1) proof infra-structure Isabelle/HOL, which constitutes basis defining mechanised process. formalisation Hierar-chical Automata (HA) allow structural decomposition into Sequential Automata. (2) Based this theory we introduce technique, can be used to abstract space HA given function. constructing over-approximations. structure-preserving designed compositional way. (3) For reasons practicability, finally two tactics supporting have Isabelle/HOL. To make proofs more efficient, these use checker SMV models automatically.