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

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

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

3、板以及模板庫(kù)。首先，針對(duì)離線(xiàn)監(jiān)控下運(yùn)行時(shí)驗(yàn)證問(wèn)題，本文提出并實(shí)現(xiàn)了Brute Force擴(kuò)展算法，Boyer-Moore擴(kuò)展算法和Sunday擴(kuò)展算法。針對(duì)在線(xiàn)監(jiān)控下運(yùn)行時(shí)驗(yàn)證問(wèn)題，提出并實(shí)現(xiàn)了模式模板匹配問(wèn)題的算法，上述算法在工程應(yīng)用中達(dá)到了簡(jiǎn)化形式化規(guī)約構(gòu)造過(guò)程的目的。然后，通過(guò)模擬運(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ǔ)言和模式模板的驗(yàn)證功能，進(jìn)一步從工程上驗(yàn)證了本文所提出的模式語(yǔ)言相關(guān)概念以及算法的有效性。
　　綜上所述，使用模式語(yǔ)言可以增強(qiáng)規(guī)約的描述能力，通過(guò)調(diào)用模式庫(kù)中的模式模板，可以快速將自然語(yǔ)言規(guī)約表示為相應(yīng)的形式化規(guī)約，從而簡(jiǎn)化自然語(yǔ)言規(guī)約向形式化語(yǔ)言規(guī)約轉(zhuǎn)化的過(guò)程，降低開(kāi)