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

Steffen Helke and Florian Kammuller, “Verification of Statecharts Using Data Abstraction” International Journal of Advanced Computer Science and Applications(IJACSA), 7(1), 2016. http://dx.doi.org/10.14569/IJACSA.2016.070179

@article{Helke2016,
title = {Verification of Statecharts Using Data Abstraction},
journal = {International Journal of Advanced Computer Science and Applications},
doi = {10.14569/IJACSA.2016.070179},
url = {http://dx.doi.org/10.14569/IJACSA.2016.070179},
year = {2016},
publisher = {The Science and Information Organization},
volume = {7},
number = {1},
author = {Steffen Helke and Florian Kammuller}
}