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

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

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

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