Verification of Statecharts Using Data Abstraction
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2016, Vol 7, Issue 1
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.
Authors and Affiliations
Steffen Helke, Florian Kammuller
Keywords
Related Articles
- EP ID EP148944
- DOI 10.14569/IJACSA.2016.070179
- Views 99
- Downloads 0
QRS Detection Based on an Advanced Multilevel Algorithm
This paper presents an advanced multilevel algorithm used for the QRS complex detection. This method is based on three levels. The first permits the extraction of higher peaks using an adaptive thresholding technique. Th...
Solving Word Tile Puzzle using Bee Colony Algorithm
In this paper, an attempt has been made to solve the word tile puzzle with the help of Bee Colony Algorithm, in order to find maximum number of words by moving a tile up, down, right or left. Bee Colony Algorithm is a ty...
A Generic Methodology for Clustering to Maximises Inter-Cluster Inertia
This paper proposes a novel clustering methodology which undeniably manages to offer results with a higher inter-cluster inertia for a better clustering. The advantage obtained with this methodology is due to an algorith...
OFDM System Analysis for reduction of Inter symbol Interference Using the AWGN Channel Platform
Orthogonal Frequency Division Multiplexing (OFDM) transmissions are emerging as important modulation technique because of its capacity of ensuring high level of robustness against any interferences. This proj...
An Energy-Efficient User-Centric Approach High-Capacity 5G Heterogeneous Cellular Networks
Today’s cellular networks (3G/4G) do not scale well in heterogeneous networks (HetNets) of multiple technologies that employ network-centric (NC) model. This destabilization is due to the need for coordination and manage...