參數(shù)化運行時驗證研究與工具實現(xiàn).pdf

1、隨著軟件規(guī)模的不斷增大，如何保證軟件可靠性和安全性成為學(xué)術(shù)界和工業(yè)界越來越關(guān)注的問題。目前，軟件測試、靜態(tài)分析和模型檢測是保證軟件質(zhì)量的常用方法，但它們都存在一定缺陷。靜態(tài)分析容易產(chǎn)生對錯誤的漏報和誤報，且很難處理指針和復(fù)雜數(shù)據(jù)結(jié)構(gòu)。模型檢測則可能導(dǎo)致狀態(tài)空間爆炸問題。而軟件測試需要手動生成測試用例，且無法驗證形式化規(guī)約。
　　運行時驗證是一種新型的程序自動驗證技術(shù)，它是一種在程序運行過程中驗證系統(tǒng)是否滿足或違背給定性質(zhì)的方法。在

2、運行時驗證中，使用監(jiān)控器來對系統(tǒng)進行驗證。監(jiān)控器從給定性質(zhì)中產(chǎn)生。在程序執(zhí)行時，監(jiān)控器通過不斷檢測程序的執(zhí)行情況來判斷它是否滿足給定的性質(zhì)。C語言是一種重要的編程語言，使用C語言編寫的程序具有執(zhí)行效率高、可移植性強等優(yōu)點。當前針對C程序的運行時驗證工具較少。JavaMOP(Monitoring-Oriented Programming)是一個針對Java程序的運行時驗證工具，但它無法對C程序進行驗證。
　　本文設(shè)計了一種針對C程序

3、的監(jiān)控器規(guī)約語言，用于描述針對C程序的形式化規(guī)約。該語言借鑒了面對方面編程的思想，可以支持基于有限狀態(tài)自動機、正則表達式和線性時序邏輯的參數(shù)化運行時驗證。本文設(shè)計了支持該語言的參數(shù)化運行時驗證方法。為了對運行時產(chǎn)生的大量監(jiān)控器進行索引，我們提出并實現(xiàn)了一種層次哈希森林的數(shù)據(jù)結(jié)構(gòu)。在此基礎(chǔ)上，本文利用C++語言和開源工具flex、bison實現(xiàn)了原型工具MOVEC(MOnitoring,VErification and Control)。