支援多種語言同步模擬驗證之框架設計

Abstract

並行機制(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，我們也重新實做了這個轉換的程式，並且解決新衍生的問題。

Multi-threading and multi-core technology introduce more computing power to software system, but unfortunately, concurrency makes system correctness more difficult to verify. To many critical systems, failures could cost lives and large amount of money, so the correctness plays a vital role in the development of such systems. In recent years, model checking is the most popular approach to address the problem. Model checking often requires users to abstract a model from a target system. But the abstraction process between source code and model often drives programmers away from such technique. This explains why verification tools are still far from practical usage. Having users write model with high-level programming language is the most straightforward idea to ease the use of verification tools. Nevertheless, the cost of building and maintaining a programming language parser and its related components is high. In this thesis, we propose an intermediate data structure based on control flow graph. In the future, we expect the input program will be translated into such control flow graph. The control flow graph serves as the standard representation for our backend analysis engine. ArCats (Architecture Refactoring and Concurrency Analysis Tool Suite) is a research prototype this work is built from. It runs in the two different graph-like data structure, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), by polymorphism technique in OOP. In the compositional analysis module, we use CCS as model input. In this thesis, the component that translates the revised CFG to CCS is also described.