基于活性順序圖的形式化驗證方法及工具研究

張　坤，葉俊民，王　嬙，趙麗嫻，陳　曙

（華中師范大學　　計算機學院，武漢　430079）

基于活性順序圖的形式化驗證方法及工具研究

張坤，葉俊民，王嬙，趙麗嫻，陳曙

（華中師范大學計算機學院，武漢430079）

近年來，形式化驗證方法在軟件開發過程的作用越來越大；如何充分利用形式化驗證方法提高軟件系統的可靠性已成為軟件開發者及使用者主要關注的問題；總結了近年來基于活性順序圖的形式化驗證方法的研究進展，首先介紹活性順序圖的語言及其表達能力與復雜性，然后深入分析現有的基于活性順序圖的形式化驗證的關鍵技術及其典型應用，最后實現一種基于活性順序圖的運行時驗證工具，實驗證明使用本驗證工具進行形式化驗證的可行性。

活性順序圖；形式化驗證；軟件開發過程

0　引言

隨著計算機技術的發展，軟件系統已經滲透到人們的生活之中，軟件系統關系著人民的信息安全、財產安全乃至生命安全。形式化驗證方法在軟件開發過程中的作用越來越受到軟件開發者的重視，確保軟件系統在任何時候都與需求規約一致，已經成為軟件開發者及使用者關注的重要問題，利用場景對系統進行建模和分析已成為軟件開發過程中形式化驗證的重要技術和方法［1］。目前形式化驗證方法主要包括模型驗證［2］與運行時驗證［3］等。

基于場景的形式化驗證經常使用順序圖對系統進行建模和分析，順序圖是一種基于場景的語言，能夠圖形化地表示系統實例間交互的時序關系。……