Browsing by Author "Cheng, Yung Pin"

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    使用Java實作局部性分析套件
    (2003) 黃吉元; Huang, Chi Yuan
    局部性分析技術對於某些系統可以有效的減緩組態爆炸，但是現有的軟體驗證工具皆少著墨於支援這部分的功能。其主要的問題在於某些系統，其架構卻不見得能組合出可分析的合成階層。其次，合成階層也難以自動化地獲得。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的語意，然後這些安全性質會被自動地加入合成階層中。經由局部性分析之後，若系統違反安全性質，則在最後的分析結果中會出現死結。