模式語言與模式模板在運(yùn)行時(shí)驗(yàn)證中的應(yīng)用.pdf

1、運(yùn)行時(shí)驗(yàn)證作為一種輕量級的形式化驗(yàn)證方法，已被應(yīng)用到許多領(lǐng)域，如 Java程序的運(yùn)行時(shí)異常驗(yàn)證、硬件運(yùn)行時(shí)行為驗(yàn)證、列車控制系統(tǒng)驗(yàn)證等。運(yùn)行時(shí)驗(yàn)證中采用形式化規(guī)約描述性質(zhì)，形式化規(guī)約最主要的優(yōu)點(diǎn)在于可以準(zhǔn)確描述被監(jiān)控對象的一類錯(cuò)誤。盡管優(yōu)勢明顯，但現(xiàn)有形式化規(guī)約仍存在兩點(diǎn)不足：其一，通常采用常量來描述事件，限制了規(guī)約的描述范圍；其二，構(gòu)造形式化規(guī)約需要具有較強(qiáng)的專業(yè)知識，影響了運(yùn)行時(shí)驗(yàn)證的推廣使用。因此，研究新的形式化規(guī)約，并提出相應(yīng)的

2、運(yùn)行時(shí)驗(yàn)證算法，具有重要的理論意義與應(yīng)用價(jià)值。
　　本文針對利用模式語言和模式模板，解決運(yùn)行時(shí)驗(yàn)證問題進(jìn)行了研究，取得的創(chuàng)新研究成果如下：
　　1.針對規(guī)約描述能力方面的不足，本文提出了模式以及模式語言的形式化定義，通過形式化定義將模式語言理論引入到運(yùn)行時(shí)驗(yàn)證領(lǐng)域中，并在此基礎(chǔ)上給出了模式語言在解決運(yùn)行時(shí)驗(yàn)證匹配問題中的應(yīng)用舉例。
　　2.針對推廣使用形式化規(guī)約過程中存在的困難，本文提出了用于簡化形式化規(guī)約構(gòu)造的模式模

3、板以及模板庫。首先，針對離線監(jiān)控下運(yùn)行時(shí)驗(yàn)證問題，本文提出并實(shí)現(xiàn)了Brute Force擴(kuò)展算法，Boyer-Moore擴(kuò)展算法和Sunday擴(kuò)展算法。針對在線監(jiān)控下運(yùn)行時(shí)驗(yàn)證問題，提出并實(shí)現(xiàn)了模式模板匹配問題的算法，上述算法在工程應(yīng)用中達(dá)到了簡化形式化規(guī)約構(gòu)造過程的目的。然后，通過模擬運(yùn)行時(shí)驗(yàn)證的實(shí)驗(yàn)，得出相比較其他算法Sunday擴(kuò)展算法，帶有HashMap結(jié)構(gòu)的模式模板以及指定關(guān)系模式模板在匹配時(shí)效率更高。此外，為了增強(qiáng)模式模板的

4、表達(dá)能力，提出了可接受狀態(tài)自動(dòng)機(jī)以及模式推導(dǎo)算法。
　　3.在運(yùn)行時(shí)驗(yàn)證工具M(jìn)onitor Verification Control中，設(shè)計(jì)并實(shí)現(xiàn)了支持模式語言和模式模板的驗(yàn)證功能，進(jìn)一步從工程上驗(yàn)證了本文所提出的模式語言相關(guān)概念以及算法的有效性。
　　綜上所述，使用模式語言可以增強(qiáng)規(guī)約的描述能力，通過調(diào)用模式庫中的模式模板，可以快速將自然語言規(guī)約表示為相應(yīng)的形式化規(guī)約，從而簡化自然語言規(guī)約向形式化語言規(guī)約轉(zhuǎn)化的過程，降低開