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 111
- Downloads 0
A Realistic Approach: RTST to Reduce Cost & Time
Regression testing is the most expensive technique, but this technique gives confidence that whatever changes has been incorporated they are not making any adverse affect to the output. In Regression Test Selection Techn...
FEATURE BASED IMAGE OPTIMIZATION TECHIQUE
The motivation behind the production of high resolution images is to increase the quality and the visual presentation of a digital image. The erstwhile analogue images captured by the silver Bromide film was having infin...
Road Recognition for Vision Navigation of Robot by Using Computer Vision
This paper presents a method for vision navigation of robot by road recognition based on image processing. By taking advantages of the unique structure in road images, the square images on road can be scanned while the r...
A New Method to Improve the Simulation Of Piezoelectric Transducer Using PSPICE And Genetic Algorithms
Piezoelectric transducer (SAW devices) is a very important device in industry but it is very difficult to simulate it using any circuit-simulation program. This paper proposes a practical method to simulate the Mason’s m...
Effective Term Based Text Clustering Algorithms
Text clustering methods can be used to group large sets of text documents. Most of the text clustering methods do not address the problems of text clustering such as very high dimensionality of the data and understandabi...