ArCats局部性模型分析安全性質和活化性質

Abstract

近年來，局部性模型分析在自動化軟體驗證領域中佔有一席角色。局部性模型分析能夠成功的關鍵在於檢驗的系統模型具有良好的階層架構，同時盡量利用最小化的技術減化子系統的內部行為，達到減緩組態爆炸的發生。透過模型架構重構可以解決不良的模型架構，這增強局部性分析的效能。當利用局部性分析檢驗系統性質時，因為保留過多的系統性質到全域系統中，造成子系統無法最小化的結果，這將大幅消減局部性分析在模型驗證中的效能。

在本篇論文中，我們根據ArCats和其在局部性分析中所提供的良好功能，開發出能夠檢測系統安全性質(safety)和活化性質(liveness)的功能，同時並能夠維持局部性分析的減緩狀態爆炸的優勢。在檢驗安全性質時，我們利用一種類似死結狀態的π狀態，讓違反安全性的系統行為能夠被偵測出來。而在檢驗活化性質時我們使用一種特殊的接受轉移（accept transition）來代表系統符合檢驗性質。這兩種在局部性分析中檢測性質，主要參考Cheung[28][29][30]的研究。但是由於ArCats是以CCS為基礎來提供模型架構重構的功能而Cheung的研究採用的是CSP，本篇論文將針對如何利用以CSP為基礎的驗證技術實做到以CCS為基礎的驗證工具中，同時探討與解決所面臨的困難。

In recent years, compositional model checking is known as a promising approach to combat state explosion problem in the automatic verification techniques. However, the success of such technique relies on a good hierarchy in system architectures so that the states in subsystemscan be minimized and hidden to alleviate state explosion problem. ARCATS is a tool designed for compositional analysis. It provides a technique called model architecture refactoring to address systems which do not possess good compositional hierarchies in their as-built architecture.

In the past, ARCATS can detect deadlocks only. In this thesis, we would like to improve ARCATS to allow safety and liveness properties to be verified in a compositional fashion. To check safety properties, a violation of safety properties is caught as a π state in the system behavior. A π state is very similar to a deadlock state. To check liveness properties, a special global transition called accept transition is added to Buchi automata which represents the liveness properties. These approaches have been proposed in Cheung[28][29][30], which is based on CSP, but we need to implement these approaches in to ARCATS, which is based on CCS. There are several issues to be addressed in this implementation. These issues will be discussed in this thesis.