Conditioned slicing-Based Pre-Reduction Technique for efficient MDG Model-checker
Journal Title: International Journal on Computer Science and Engineering - Year 2011, Vol 3, Issue 3
Abstract
Integrating formal verification techniques into the hardware design process provides the means to rigorously prove critical properties. However, most automatic verification techniques, such as model checking, are only effectively applicable to designs of limited sizes due to the state explosion problem. The Multiway Decision Graphs (MDG) method is an efficient method to define hardware designs into more abstract environments; however, the MDG model checker (MDG-MC) still suffers from the state explosion problem. Furthermore, all the backward reduction algorithms cannot be used in MDG, due to the presence of abstract state variables. In this work, in order to alleviate the state explosion problem, we introduce an abstraction based property model checking approach for MDG-MC based on conditioned slicing. This reduction method is based on a static reduction technique that, before the actual verification begins, identifies cases where conditioned slicing reduction rules can safely be applied to reduce the MDG-based model component graphs and that results in reducing the verification complexity when the verification itself is performed. We handle property specifications of the form G(antecedent => consequent). Our method aims to build the conditioned slicing technique (CSPre-MDG) on the top of our previous static slicing reduction technique (SSPre-MDG) to improve the performance of the reduction.
Authors and Affiliations
Saad Elmansori
Keywords
Related Articles
- EP ID EP108091
- DOI -
- Views 101
- Downloads 0
FREQUENT DATA GENERATION USING RELATIVE DATA ANALYSIS
Traditional association rule mining method mines association rules only for the items bought by the customer. However an actual transaction consists of the items bought by the customer along with the quantity of items bo...
Devanagari Isolated Character Recognition by using Statistical features ( Foreground Pixels Distribution, Zone Density and Background Directional Distribution feature and SVM Classifier)
In this paper, we present a methodology for off-line Isolated handwritten Devanagari character recognition. The proposed methodology relies on a three feature extraction techniques. The first technique is based on recurs...
Comparison of variable learning rate and Levenberg-Marquardt back-propagation training algorithms for detecting attacks in Intrusion Detection Systems
This paper investigates the use of variable learning rate back-propagation algorithm and Levenberg-Marquardt back-propagation algorithm in Intrusion detection system for detecting attacks. In the present study, these 2 n...
Personal Cloud-based Learning Environment
In recent years, E-learning has grown into a widely accepted way of learning, and the usage of the global network is inevitable in every education process. Ubiquitous learning environments should integrate modern pedagog...
Novel Sorting Algorithm
Sorting has become a stand in need of prosaic life activities. Sorting in computer science alluded to as ordering deals with arranging elements of a list or a set of records of a file in ascending or descending order. We...