Browsing by Author "金京"
Now showing 1 - 1 of 1
- Results Per Page
- Sort Options
Item 支援多種語言同步模擬驗證之框架設計(2010) 金京; Jin Ching並行機制(concurrency)的引進提供給軟體系統更多的效能,不幸的是,這使的原本就不易檢驗的系統正確性變的更加困難。通常關鍵性系統(critical systems)可能因為發生系統錯誤而造成無法承受的損失,故檢驗軟體的正確性對這一類系統是相當重要的。而在現行的驗證技術中,以模型驗證(model checking)為最常見。 這類技術多半是仰賴使用者先行將待檢驗的系統,依模型檢測工具制定的模型描述語言(modeling language)輸入後才能進行正式的驗證程序。這之間的轉換過程除了會造成錯誤,也會造成許多資訊的遺失,而這也解釋了為何主要的 model checking技術離實用還有很大的距離。 直接驗證高階語言直覺上會是最自然的選擇,不過直接以程式語言進行驗證的代價並不便宜,而且有許多待突破的技術困難,例如,每一種程式語言都有其獨特的特性,而且所支援的同步與通訊指令都不相同。因此本篇論文提出了一個彈性架構,在這個架構中,我們先將未來所選定的高階語言轉換成本論文所描述的control flow graph(CFG),目的在應付未來支援多語言輸入的支援。其目的是保留原始程式碼的資訊,讓後端模擬引擎可依 control flow graph 進行分析。此CFG 的制訂可以令後端的分析與模擬引擎,與前端語言的語法以及語意做到區隔,使模擬引擎可以支援多種程式語言的輸入。我們的目標是希望使用者在未來直接可以使用一般的程式語言建立模型,並且可以在程式開發階段就能進行初步的分析檢驗。 ArCats中的局部性分析模組,是使用CCS(Calculus of Communicating System)做為模型輸入。因此為了使修改後的 CFG 也能正確的轉換出 CCS,我們也重新實做了這個轉換的程式,並且解決新衍生的問題。