模式语言与模式模板在运行时验证中的应用
发布时间：2018-09-08 18:38
【摘要】：运行时验证作为一种轻量级的形式化验证方法,已被应用到许多领域,如Java程序的运行时异常验证、硬件运行时行为验证、列车控制系统验证等。运行时验证中采用形式化规约描述性质,形式化规约最主要的优点在于可以准确描述被监控对象的一类错误。尽管优势明显,但现有形式化规约仍存在两点不足:其一,通常采用常量来描述事件,限制了规约的描述范围;其二,构造形式化规约需要具有较强的专业知识,影响了运行时验证的推广使用。因此,研究新的形式化规约,并提出相应的运行时验证算法,具有重要的理论意义与应用价值。本文针对利用模式语言和模式模板,解决运行时验证问题进行了研究,取得的创新研究成果如下:1.针对规约描述能力方面的不足,本文提出了模式以及模式语言的形式化定义,通过形式化定义将模式语言理论引入到运行时验证领域中,并在此基础上给出了模式语言在解决运行时验证匹配问题中的应用举例。2.针对推广使用形式化规约过程中存在的困难,本文提出了用于简化形式化规约构造的模式模板以及模板库。首先,针对离线监控下运行时验证问题,本文提出并实现了Brute Force扩展算法,Boyer-Moore扩展算法和Sunday扩展算法。针对在线监控下运行时验证问题,提出并实现了模式模板匹配问题的算法,上述算法在工程应用中达到了简化形式化规约构造过程的目的。然后,通过模拟运行时验证的实验,得出相比较其他算法Sunday扩展算法,带有HashMap结构的模式模板以及指定关系模式模板在匹配时效率更高。此外,为了增强模式模板的表达能力,提出了可接受状态自动机以及模式推导算法。3.在运行时验证工具Monitor Verification Control中,设计并实现了支持模式语言和模式模板的验证功能,进一步从工程上验证了本文所提出的模式语言相关概念以及算法的有效性。综上所述,使用模式语言可以增强规约的描述能力,通过调用模式库中的模式模板,可以快速将自然语言规约表示为相应的形式化规约,从而简化自然语言规约向形式化语言规约转化的过程,降低开发人员构造形式化规约描述性质的门槛。
[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.
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP311.53
本文编号：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.
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP311.53
【参考文献】
相关期刊论文 前2条
1 张硕;贺飞;;运行时验证技术的研究进展[J];计算机科学;2014年S2期
2 薛锐;冯登国;;安全协议的形式化分析技术与方法[J];计算机学报;2006年01期
，本文编号：2231357
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/2231357.html
