Automated Compositional Verification: Problems, Solutions, and Experiments
Date Issued
2009
Date
2009
Author(s)
Chen, Yu-Fang
Abstract
Compositional verification is a promising approach to scale up Model Checking (a fully automatic approach to hardware/software design verification) to large designs. The basic idea behind this approach is divide-and-conquer. It utilizes an assume-guarantee rule to break aask of verifying a system down to subtasks of verifying its components. The major difficulty in using an assume-guarantee rule is to search for appropriate contextual assumptions (the environments provided by other components); the search usually requires human intervention.n the past six years, several approaches based on machine learning techniques have been proposed to automate the assume-guarantee style of composition verification under aanguage theoretical framework. However, most of the currently proposed approaches do not really improve the efficiency of Model Checking and can only handle a restricted class of properties.n this thesis, we point out fundamental problems of the state-of-the-art automated compositional verification approaches and propose solutions to alleviate these problems.hree major problems of the previous approaches are identified in this thesis. First, most of the approaches are heuristics and cannot guarantee finding a minimal contextual assumption, even if there exists one. Second, all of the algorithms that have been proposedo far are explicit-state approaches; they explicitly construct the complete transition systemsf the intermediate assumptions. Third, all of the previous approaches cannot handle livenessroperties, which are essential to verify the correctness of a system.or the three problems, we suggest solutions and evaluate them via experiments. Contrastingo algorithms that are based on heuristics, we propose an algorithm that guarantees finding the minimal contextual assumption for assume-guarantee reasoning. The key techniquenvolved is a learning algorithm for minimal separating DFA''s. Our learning algorithmor minimal separating DFA''s has a quadratic query complexity. In contrast, the most recentlgorithm of Gupta et al. is exponential. Moreover, experimental results show that our learninglgorithm significantly outperforms all existing algorithms on a large number of exampleroblems.e develop the first fully implicit-state algorithm for automated compositional verification.his algorithm avoids using the L* learning algorithm, which explicitly enumeratesvery state of a conjecture DFA, to find contextual assumptions. Instead, it uses Bshouty''searning algorithm for boolean functions as the core. We evaluate the new algorithm viaxperiments and suggest directions for further improvements.oreover, we extend automated compositional verification to verify liveness propertiesy presenting an algorithm to learn an arbitrary regular set of infinite sequences (omega regularanguage) over an alphabet . The most important breakthrough involved in thisxtension is that we solved the problem of learning omega-regular languages using queriesnd counterexamples, which has been open since 1989.he problems we solved are important and fundamental because they are rooted from the algorithm, which is the foundation of the mainstream automated compositional verification approaches. There are still other problems that we have not addressed in this thesis. Althoughe do not cover all problems of the automated compositional verification approaches, weelieve that our results are important milestones on the way toward a complete solution toutomated compositional verification.
Subjects
Model Checking
Machine Learning
Regular Language
Omega Regular Language
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-D93725005-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):8e0607221cca1e5c9009d42025df1b0f