Compositional Verification Through Learning And Assume-Guarantee Rules

Software reuse offers a solution to eliminate repeated work and improve efficiency and quality in the software development. Software reuse is generally classified into two catalogues:product reuse and process reuse. Reuse based on software components is the important form of product reuse and is the major area of software reuse research. Giving a finite model of a system composed by the compoents and a required property of the system.model checking can determine whether the system satisfy the property. However.model checking often faces a serious problem of state explosion, and compositional reasoning addresses the state-explosion problem by using a divede-and-conquer fashion.It's necessary to incorporate the environment in which each componet can be operated correctly. This is so called assume-guarantee reasoning.This paper studies on compositional verification of a system composed by n compoents based on assume-guarantee reasoning.My reserch includes the following sections:1. This paper proposes the basic concepts around the thesis,such as software reuse and compoent, the method of formalization, model checking, the LTS, assume-guarantee resoning and so on. In additon,this paper presentes detailedly the L learning algorithm and pointes out its characteristics.2. This paper researches two strategies of compositional verification:a framework based on assume-guarantee rule ASYM and the other based on assume-guarantee rule SYM-N. A approporiate assume is computed using the L* algorithm to determine whether the system satisfy the property in the two frameworks.The learning of assume is a iterative process,so it's an important issue of how to increase the iterative learning process.3. This paper proposes our own framework based on the rule S YM.and describes the algorithm according to the framework in detail, we also adopt the L* learning algorithm as the prior frameworks,while we suggest two optimizations to the framework.A more operation is introduced in our framework to reduce the redundant verification time,and the concept of equivalent counterexample and partial error FSM is used to improve the L* algorithm in our framework.and the experiment results also show that our framework is mor efficient. In addition,we analyse the correctness and termination of the framework,which meanes the framework will return the result of checking correctly in the end.