Model checking using interface abstraction

Abstract

This thesis presents a methodology of formal verification using model checking tool. Model checking is used to determine the validity of formulas written in temporal logic to respect the behavioral model of a system. One of the serious limitations of the model checking approach comes from its reliance on the explicit state transition graph representation of the hardware system to be verified. Typically, the number of states increases exponentially with the number of elements in the system, resulting in what is popularly called the state explosion problem. Although many researchers have tried to verified solved this problem using the abstraction and reduction of the environment and target system, no general and explicit methodology for the abstraction of the environment has been presented yet. The proposed method in this thesis tries to solve the state explosion problem in the model checking is based on ‘design separation’ and ‘interface abstraction’. Design separation is a process separating the whole design into small designs to be verifiable while the interface abstraction is a process for modeling the interface behavior between separated designs. By means of this method the complex design having a state explosion problem can be verified successfully and the memory usage and computing time for model checking also can be improved about 100 times than no use of the proposed method.