Performance analysis of symbolic reachability algorithms in model checking

[摘要] Simulation used to be the most common technique to test the correctness of a system. However, the complexity and size of digital systems has increased drastically during the last few years, which exposes increasingly intractable problems faced by simulation. In order to solve the problems, formal verification was introduced to provide a different approach to validate a system. Model checking has been proposed to make the verification procedure fully automatic. However, the state explosion problem restricts the application of model checking to small systems. Of the different techniques to solve this state explosion problem, one that provided a major breakthrough was that of using techniques to manipulate states symbolically with Binary Decision Diagrams (BDDs). First we use BDDs to represent sets of states that are randomly chosen from a state space. Then we study how the number of states affects the size of BDDs. Based on our research, we provide a formula to calculate the size of BDDs that representing states randomly chosen from a state space.Having a better understanding of BDDs, we are able to compare the main algorithms used in symbolic model checking. (Abstract shortened by UMI.)

[发布机构] Rice University

[效力级别] science