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 96
- Downloads 0
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...
Optimizing Coverage of Churn Prediction in Telecommunication Industry
Companies are investing more in analytics to obtain a competitive edge in the market and decision makers are required better identification among their data to be able to interpret complex patterns more easily. Alluring...
English to Creole and Creole to English Rule Based Machine Translation System
Machine translation is the process of translating a text from one language to another, using computer software. A translation system is important to overcome language barriers, and help people communicate between differe...
Introducing Time based Competitive Advantage in IT Sector with Simulation
Incompletion of projects in time leads to project failure which is the major dilemma of the software industry. Different strategies are used to gain a competitive advantage over competitors in business. In software persp...
An Algorithm Research for Supply Chain Management Optimization Model
In this paper, we consider the extended linear complementarity problem on supply chain management optimization model. We first give a global error bound for the extended linear complementarity problem, and then propose a...