模式語(yǔ)言與模式模板在運(yùn)行時(shí)驗(yàn)證中的應(yīng)用
發(fā)布時(shí)間：2018-09-08 18:38
【摘要】：運(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)的運(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)造的模式模板以及模板庫(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)模式模板的表達(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)發(fā)人員構(gòu)造形式化規(guī)約描述性質(zhì)的門(mén)檻。
[Abstract]:As a lightweight formal verification method, runtime verification has been applied to many fields, such as runtime exception verification of Java programs, hardware runtime behavior verification, train control system verification and so on. Formal specification is used in runtime verification. The main advantage of formal specification is that it can accurately describe a class of errors of monitored object. Although the advantages are obvious, the existing formal protocols still have two shortcomings: first, they usually use constant to describe events, which limits the scope of specification; second, the construction of formal protocols requires strong expertise. It affects the popularization of runtime verification. Therefore, it is of great theoretical significance and practical value to study the new formal specification and propose the corresponding runtime verification algorithm. In this paper, we study how to use pattern language and pattern template to solve the problem of run-time verification. The innovative research results are as follows: 1. In this paper, the formal definition of schema and schema language is proposed, and the theory of schema language is introduced into the field of runtime verification through formal definition. On this basis, the application of pattern language in solving the problem of runtime verification matching is given. 2. 2. Aiming at the difficulties in the process of popularizing formal specification, this paper puts forward the pattern template and template library to simplify the construction of formal specification. Firstly, aiming at the problem of running time verification under off-line monitoring, this paper proposes and implements the Brute Force extension algorithm and the Sunday extension algorithm. An algorithm for pattern template matching is proposed and implemented to solve the problem of runtime verification under on-line monitoring. The above algorithms can simplify the construction process of formal specification in engineering applications. Then, by simulating the experiment of runtime verification, it is concluded that compared with other algorithms, Sunday extension algorithm, pattern template with HashMap structure and specified relational pattern template are more efficient in matching. In addition, in order to enhance the expression ability of pattern templates, an acceptable state automaton and a pattern derivation algorithm .3are proposed. In the runtime verification tool Monitor Verification Control, we design and implement the verification function of supporting pattern language and pattern template, and further verify the concept of schema language and the validity of the algorithm proposed in this paper. To sum up, using pattern language can enhance the description ability of the specification. By calling the pattern template in the pattern library, the natural language specification can be quickly represented as the corresponding formal specification. Therefore, the process of transforming natural language specification into formal language specification is simplified, and the threshold for developers to construct formal specification description is lowered.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：TP311.53
本文編號(hào)：2231357
[Abstract]:As a lightweight formal verification method, runtime verification has been applied to many fields, such as runtime exception verification of Java programs, hardware runtime behavior verification, train control system verification and so on. Formal specification is used in runtime verification. The main advantage of formal specification is that it can accurately describe a class of errors of monitored object. Although the advantages are obvious, the existing formal protocols still have two shortcomings: first, they usually use constant to describe events, which limits the scope of specification; second, the construction of formal protocols requires strong expertise. It affects the popularization of runtime verification. Therefore, it is of great theoretical significance and practical value to study the new formal specification and propose the corresponding runtime verification algorithm. In this paper, we study how to use pattern language and pattern template to solve the problem of run-time verification. The innovative research results are as follows: 1. In this paper, the formal definition of schema and schema language is proposed, and the theory of schema language is introduced into the field of runtime verification through formal definition. On this basis, the application of pattern language in solving the problem of runtime verification matching is given. 2. 2. Aiming at the difficulties in the process of popularizing formal specification, this paper puts forward the pattern template and template library to simplify the construction of formal specification. Firstly, aiming at the problem of running time verification under off-line monitoring, this paper proposes and implements the Brute Force extension algorithm and the Sunday extension algorithm. An algorithm for pattern template matching is proposed and implemented to solve the problem of runtime verification under on-line monitoring. The above algorithms can simplify the construction process of formal specification in engineering applications. Then, by simulating the experiment of runtime verification, it is concluded that compared with other algorithms, Sunday extension algorithm, pattern template with HashMap structure and specified relational pattern template are more efficient in matching. In addition, in order to enhance the expression ability of pattern templates, an acceptable state automaton and a pattern derivation algorithm .3are proposed. In the runtime verification tool Monitor Verification Control, we design and implement the verification function of supporting pattern language and pattern template, and further verify the concept of schema language and the validity of the algorithm proposed in this paper. To sum up, using pattern language can enhance the description ability of the specification. By calling the pattern template in the pattern library, the natural language specification can be quickly represented as the corresponding formal specification. Therefore, the process of transforming natural language specification into formal language specification is simplified, and the threshold for developers to construct formal specification description is lowered.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：TP311.53
【參考文獻(xiàn)】
相關(guān)期刊論文 前2條
1 張碩;賀飛;;運(yùn)行時(shí)驗(yàn)證技術(shù)的研究進(jìn)展[J];計(jì)算機(jī)科學(xué);2014年S2期
2 薛銳;馮登國(guó);;安全協(xié)議的形式化分析技術(shù)與方法[J];計(jì)算機(jī)學(xué)報(bào);2006年01期
，本文編號(hào)：2231357
本文鏈接：http://sikaile.net/kejilunwen/ruanjiangongchenglunwen/2231357.html
最近更新
教材專(zhuān)著
