Verification of statecharts using data abstraction
Article
Helke, S. and Kammueller, F. 2016. Verification of statecharts using data abstraction. International Journal of Advanced Computer Science and Applications. 7 (1), pp. 571-583. https://doi.org/10.14569/IJACSA.2016.070179
Type | Article |
---|---|
Title | Verification of statecharts using data abstraction |
Authors | Helke, S. and Kammueller, F. |
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. |
Publisher | SAI Organization |
Journal | International Journal of Advanced Computer Science and Applications |
ISSN | 2158-107X |
Publication dates | |
15 Jan 2016 | |
Publication process dates | |
Deposited | 04 May 2016 |
Accepted | 01 Jan 2016 |
Output status | Published |
Digital Object Identifier (DOI) | https://doi.org/10.14569/IJACSA.2016.070179 |
Language | English |
https://repository.mdx.ac.uk/item/865v2
57
total views0
total downloads0
views this month0
downloads this month