Modular Model Checking of SA/RT Models Using Assoiation Rules

(File Last Modified Wed, May 29, 2002.)

• Review: Modular Model Checking of SA/RT Models Using Assoiation Rules
• Problem Addressed
• Approach Proposed
• Validation
• Contribution
• Comments

Review: Modular Model Checking of SA/RT Models Using Assoiation Rules

Problem Addressed

When validating complex systems model checkers are used to do a exhausitive search over the state-space of the system. Due to state-explosion problem, the formal verification of complex reactive systems require the use of compositional/modular techniques. However, many of them need user guidance in order to specify an abstract environment of the componect to verify. The problem is how to make this process automatic.

Approach Proposed

This paper present a method to automatically construct abstract environments of components in from of association rules in large databases to obtain context constraints. Then, they use those behaviour rules to verify the component by a model checker.

Validation

The proposed method is applied on one model. They baseline the results against a previous approach. Experimental result are reported and performace is compared between the two. The authors evaluated their contribution by discussing some related work, although very briefly.

Contribution

The paper mentioned that the problem addressed has been researched previously in the domain and there are different techniques invented. The authors claim that their approach is novel compared to others: they use association rule mining to extract all the rules that serve as context constraints in the component to verify. Their technique is fully automatic and is able to decrease the user guidance as well as computational resource.

Comments

The authors describe the standard association rule mining technique and provide their reasons and steps to optimize the algorithm for their domain. Technical details are presented with some examples and Inputs and outputs are given. The method is later illustrated on one case study to support their conclusion. The method is shown in a systematic manner.

This paper is organized in a sound order. But there are so many grammatical mistakes which should not appear in such an academic paper.

Note:Check the rule construction procedure: support=0, confidence=100