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 64
- Downloads 0
An improved Approach for Document Retrieval Using Suffix Trees
Huge collection of documents is available at few mouse clicks. The current World Wide Web is a web of pages. Users have to guess possible keywords that might lead through search engines to the pages that contain informat...
BITRU: Binary Version of the NTRU Public Key Cryptosystem via Binary Algebra
New terms such as closest vector problem (CVP) and the shortest vector problem (SVP), which have been illustrated as NP-hard problem, emerged, leading to a new hope for designing public key cryptosystem based on certain...
Dynamic Bandwidth Allocation in LAN using Dynamic Excess Rate Sensing
Today human and information processing system both need rapid access to anything they want on the internet. To fulfill these needs more and more internet service providers with a large amount of bandwidth are introducing...
An Efficient Algorithm for Enumerating all Minimal Paths of a Graph
The enumeration of all minimal paths between a terminal pair of a given graph is widely used in a lot of applications such as network reliability assessment. In this paper, we present a new and efficient algorithm to gen...
Quantifying the Relationship between Hit Count Estimates and Wikipedia Article Traffic
This paper analyzes the relationship between search engine hit counts and Wikipedia article views by evaluating the cross correlation between them. We observe the hit count estimates of three popular search engines over...