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 82
- Downloads 0
A Survey on Smartphones Systems for Emergency Management (SPSEM)
Emergency never runs with earlier intimations and indications. In the real world and practical life, detecting and perceiving such emergencies and reporting them are a genuine test and tough challenge. Smartphones System...
Evaluating a Cloud Service using Scheduling Security Model (SSM)
The development in technology makes cloud com-puting widely used in different sectors such as academic and business or for a private purposes. Also, it can provide a convenient services via the Internet allowing stakehol...
Comparison of Task Scheduling Algorithms in Cloud Environment
The enhanced form of client-server, cluster and grid computing is termed as Cloud Computing. The cloud users can virtually access the resources over the internet. Task submitted by cloud users are responsible for efficie...
Assessment and Comparison of Fuzzy Based Test Suite Prioritization Method for GUI Based Software
The testing of event driven software has significant role to improve overall quality of software. Due to event driven nature of GUI based software many test cases are generated and it is difficult to identify test cases...
Interest Reduction and PIT Minimization in Content Centric Networks
Content Centric Networking aspires to a more efficient use of the Internet through in-path caching, multi-homing, and provisions for state maintenance and intelligent forwarding at the CCN routers. However, these benefit...