Conditioned slicing-Based Pre-Reduction Technique for efficient MDG Model-checker

Apply

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

EP ID EP108091
DOI -
Views 76
Downloads 0