使用Java實作局部性分析套件

Abstract

局部性分析技術對於某些系統可以有效的減緩組態爆炸，但是現有的軟體驗證工具皆少著墨於支援這部分的功能。其主要的問題在於某些系統，其架構卻不見得能組合出可分析的合成階層。其次，合成階層也難以自動化地獲得。Cheng& Young在[15]中提出一套方法稱refactoring。此方法利用CCS[12]中的weak bisimulation，將原本無法被分析的系統透過分割與轉換後，轉變為另一個行為相等的新系統。這個新系統的模組間的關係因為較為鬆散(loosely coupled)，利用誤試(trial & error)的方式可從中找出一個可分析的合成階層。這使得局部性分析的應用範圍有極大的改善。 我們配合此技術實作出局部性分析的電腦輔助驗證的工具套件。因為Java眾多的優點，如豐富的類別函式庫、記憶體的自動管理、及跨平台的特性，我們選擇以Java作為實作的語言。在這工具套件中的主要功能包含了合成階層的編輯環境(hierarchy editor)、並行合成(parallel composition)、本文限制(context constraint)[11]、分支雙模擬(branch bisimulation)[18]、安全性質的檢驗(safety property verification)[13]。這些功能當中，合成階層對於局部性分析的成敗扮演著關鍵性的作用，而且難以自動化產生。在實際的應用中，經常需要嘗試許多種階層。因此，我們在合成階層編輯環境中提供一個可以迅速地組合階層的功能。這種功能可為局部性分析的使用者帶來相當的便利。另外，局部性分析通常配合本文限制會有更大的效果。我們以Cheung& Kramer[11]中所提出的方法加以修改成以CCS語意為基礎的本文限制套件。再者，分支雙模擬套件考量其可移植性，我們重新以Java實作。最後，我們以Cheung & Kramer〔13〕中的方法，用局部性分析來檢驗安全性質，其中安全性質的檢測被轉換成一個死結偵測(deadlock detection)的問題。我們修改了該方法，使其符合CCS的語意，然後這些安全性質會被自動地加入合成階層中。經由局部性分析之後，若系統違反安全性質，則在最後的分析結果中會出現死結。Compositional analysis can alleviate the well-known state explosion problem for some systems. However, existing computer-aided verification tools which facilitate this approach are rare. The main problem of the approach is analyzable composition hierarchy can be difficult to find in many systems. Besides, composition hierarchy is difficult to be obtained automatically. Cheng& Young in [15] overcome the problem by refactoring a system, which decomposes and transforms a system into another one with behavior equivalence preserved using weak bisimulation of CCS [12]. Refactoring often transform a system into one with loosely coupled components, which are more amenable to compositional analysis. By trial and error, we can find an analyzable composition hierarchy from the refactored architecture. It increases sociability of the compositional analysis for practical applications.

In this thesis, to aid re-factoring, we implement a compositional analysis tool suite, which adopts CCS semantics. We implement the tool suite by Java, because Java has a lot of benefits, such as rich class library, memory management automatically, and portability. The tool suite includes hierarchy editor, parallel composition, context-constraint [11], branch bisimulation [18], and safety property verification [13]. First, because the composition hierarchy often has great impact on compositional analysis, we build a hierarchy editor to allow tool users editing hierarchies easily and conveniently. Second, compositional analysis can be effective with the context-constraint. We adopt Cheung& Kramer’s approach [11], and modify it to fit CCS semantics. Third, we re-implement branch bisimulation in Java. At last, we adopt Cheung & Kramer’s approach in [13] to verify safety property with CCS semantics. Their approach translates the verification problem of safety property to a deadlock detection problem. We automatically add the safety property in the composition hierarchy. A violation of safety property will be manifested as a deadlock in the result of compositional analysis.