Techniques for reducing the computational requirements of symbolic reachability analysis.

Format:

Book

Thesis/Dissertation

Author/Creator:

Yang, Zijiang.

Contributor:

Alur, Rajeev, 1966- advisor.

University of Pennsylvania.

Language:

English

Subjects (All):

Computer science.

0984.

Penn dissertations--Operations and information management.

Operations and information management--Penn dissertations.

Penn dissertations--Managerial science and applied economics.

Managerial science and applied economics--Penn dissertations.

Local Subjects:

Penn dissertations--Operations and information management.

Operations and information management--Penn dissertations.

Penn dissertations--Managerial science and applied economics.

Managerial science and applied economics--Penn dissertations.

0984.

Physical Description:

167 pages

Contained In:

Dissertation Abstracts International 64-10B.

System Details:

Mode of access: World Wide Web.

text file

Summary:

Verification techniques using symbolic state space traversal rely on efficient algorithms based on Binary Decision Diagrams (BDDs) for reachability computation. Unfortunately, BDD size is very sensitive to the number of variables, variable ordering, and the nature of the logic expressions being represented. In spite of a large body of work, the current purely BDD-based approach has been unreliable for designs of realistic size and functionality because of the state-space explosion problem.

In this thesis, we propose three approaches to cope with the problem. The first approach combines Boolean Satisfiability (SAT) techniques with BDD-based techniques in a single integrated framework. It can be regarded as SAT providing a disjunctive decomposition of the image computation into many subproblems, each of which is handled in the standard way using BDDs. Various novel heuristics such as BDD bounding, partition-based decision and dynamic detection and removal of inactive clauses have been proposed to improve the performance further. The second approach is motivated by the fact that the number of variables is a critical parameter that affects the performance of BDD packages. We propose a technique called variable reuse to reduce the variable usage. It works synergetically with conjunctive partitioning and early quantification, leading to further savings in reachability analysis. The third approach explores behavioral hierarchy of the designs. It is most useful in modern software design languages that promote hierarchy as one of the key constructs for structuring complex specifications.

Notes:

Thesis (Ph.D. in Operations and Information Management) -- University of Pennsylvania, 2003.

Source: Dissertation Abstracts International, Volume: 64-10, Section: B, page: 5053.

Supervisor: Rajeev Alur.

Local Notes:

School code: 0175.

ISBN:

9780496567799

Access Restriction:

Restricted for use by site license.