自動化組合式驗證：問題、解答、實驗

Abstract

自動化組合式驗證被普遍認為是增進模型驗證效率及可處理規模的重要方法。在這方法背後的基本想法是各個擊破。他運用一個假設-保證式推論規則來把驗證一個系統的工作拆解成數個驗證其組成元件的子工作。使用這個方法最困難的地方，在於如何找到一個適用的環境假設。這個尋找的工作通常需要靠人工完成。在過去六年中，在透過機器學習的方式來自動化假設-保證式的組合式自動驗證這個主題上，有非常多的研究發表。然而，大部分目前發表的結果並不能真的增進模型驗證方法的效率，而且能檢查的性質也很有侷限。在這篇論文中，我們指出了現今自動化組合式驗證方法的根本問題，並且提出解決方案。 我們找出了三個主要的問題。其一、大部分的成果是啟發式的方法。他們不能保證找到最小(佳)的環境假設。其二、他們全部是顯性-狀態的方法；他們列舉出環境假設的所有可能狀態。其三、所有之前提出的方法都不能檢驗liveness性質。檢查這類性質的對於完整的檢查一個系統是否正確是不可或缺的。 針對這三個問題，我們提出了建議的解答並透過實驗來評估他們的效果。相對於啟發式的方法，我們提出了能保證找到最小環境假設的演算法。這個方法的關鍵技術是一個最小分隔DFA的機器學習演算法。我們的演算法的查詢複雜度僅有平方次數，相對的，目前最近的演算法(由Gupta等提出的)是指數次數的。此外，實驗結果也顯現了我們的方法明顯的優於所有之前提出的作法。 我們發展了第一個完全隱含狀態的自動化組合式驗證演算法。這個方法避免掉使用L*機器學習演算法。他利用Bshouty提出的對於布林函式的機器學習方法作為核心。我們也透過實驗來評出這個方法並提出了很多可能的改良方向。 此外，我們把自動化組合式驗證擴充至能處理Liveness性質。關鍵的技術是一個對於任意無限長度規則語言(Omega規則語言)的機器學習演算法。Omega規則語言的機器學習是一個從1989開始的開放問題。 我們解決的問題對於自動化組合式驗證技術而言是根本而重要的。因為這些問題都跟源自L*演算法，這演算法被大多數的自動化組合式驗證方法採用。在這篇論文中，我們並沒有解決自動化組合式驗證所有的問題。但是我們相信我們的成果會是自動化組合式驗證技術的一個重要里程碑。

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 a task 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. In the past six years, several approaches based on machine learning techniques have been proposed to automate the assume-guarantee style of composition verification under a language 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. In this thesis, we point out fundamental problems of the state-of-the-art automated compositional verification approaches and propose solutions to alleviate these problems. Three 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 proposed so far are explicit-state approaches; they explicitly construct the complete transition systems of the intermediate assumptions. Third, all of the previous approaches cannot handle liveness properties, which are essential to verify the correctness of a system. For the three problems, we suggest solutions and evaluate them via experiments. Contrasting to algorithms that are based on heuristics, we propose an algorithm that guarantees finding the minimal contextual assumption for assume-guarantee reasoning. The key technique involved is a learning algorithm for minimal separating DFA's. Our learning algorithm for minimal separating DFA's has a quadratic query complexity. In contrast, the most recent algorithm of Gupta et al. is exponential. Moreover, experimental results show that our learning algorithm significantly outperforms all existing algorithms on a large number of example problems. We develop the first fully implicit-state algorithm for automated compositional verification. This algorithm avoids using the L* learning algorithm, which explicitly enumerates every state of a conjecture DFA, to find contextual assumptions. Instead, it uses Bshouty's learning algorithm for boolean functions as the core. We evaluate the new algorithm via experiments and suggest directions for further improvements. Moreover, we extend automated compositional verification to verify liveness properties by presenting an algorithm to learn an arbitrary regular set of infinite sequences (omega regular language) over an alphabet . The most important breakthrough involved in this extension is that we solved the problem of learning omega-regular languages using queries and counterexamples, which has been open since 1989. The problems we solved are important and fundamental because they are rooted from the L 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. Although we do not cover all problems of the automated compositional verification approaches, we believe that our results are important milestones on the way toward a complete solution to automated compositional verification.