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 95
- Downloads 0
A Review on Parameters Identification Methods for Asynchronous Motor
The decoupling of excitation current and torque current is realized by Vector control so that the speed regulating performance of asynchronous motor is comparable with that of dc motor. The control precision is directly...
Modeling and FPGA Implementation of a Thermal Peak Detection Unit for Complex System Design
This paper, presents the modelization and the implementation of a thermal peak detection unit for complex system design. The modelization step starts with modeling the formula of the heat source using Simulink/Matlab too...
A Novel Assessment to Achieve Maximum Efficiency in Optimizing Software Failures
Software Reliability is a specialized area of software engineering which deals with the identification of failures while developing the software. Effective analysis of the reliability helps to signify the number of failu...
Cultural Dimensions of Behaviors Towards E-Commerce in a Developing Country Context
Customers prefer to shop online for various reasons such as saving time, better prices, convenience, selection, and availability of products and services. The accessibility and the ubiquitous nature of the Internet facil...
Evaluation for Feature Driven Development Paradigm in Context of Architecture Design Augmentation and Perspective Implications
Agile is a light weight software development methodology that is useful for rapid application development which is the need of current software industry. Since the focus of agile software development is the customer but...