模式语言与模式模板在运行时验证中的应用

作     者：李昕 

作者单位：南京航空航天大学 

学位级别：硕士

导师姓名：陈哲

授予年度：2016年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：模式语言 模式模板 运行时验证 匹配问题 模式推导问题 

摘      要：运行时验证作为一种轻量级的形式化验证方法,已被应用到许多领域,如Java程序的运行时异常验证、硬件运行时行为验证、列车控制系统验证等。运行时验证中采用形式化规约描述性质,形式化规约最主要的优点在于可以准确描述被监控对象的一类错误。尽管优势明显,但现有形式化规约仍存在两点不足:其一,通常采用常量来描述事件,限制了规约的描述范围;其二,构造形式化规约需要具有较强的专业知识,影响了运行时验证的推广使用。因此,研究新的形式化规约,并提出相应的运行时验证算法,具有重要的理论意义与应用价值。本文针对利用模式语言和模式模板,解决运行时验证问题进行了研究,取得的创新研究成果如下:1.针对规约描述能力方面的不足,本文提出了模式以及模式语言的形式化定义,通过形式化定义将模式语言理论引入到运行时验证领域中,并在此基础上给出了模式语言在解决运行时验证匹配问题中的应用举例。2.针对推广使用形式化规约过程中存在的困难,本文提出了用于简化形式化规约构造的模式模板以及模板库。首先,针对离线监控下运行时验证问题,本文提出并实现了Brute Force扩展算法,Boyer-Moore扩展算法和Sunday扩展算法。针对在线监控下运行时验证问题,提出并实现了模式模板匹配问题的算法,上述算法在工程应用中达到了简化形式化规约构造过程的目的。然后,通过模拟运行时验证的实验,得出相比较其他算法Sunday扩展算法,带有HashMap结构的模式模板以及指定关系模式模板在匹配时效率更高。此外,为了增强模式模板的表达能力,提出了可接受状态自动机以及模式推导算法。3.在运行时验证工具Monitor Verification Control中,设计并实现了支持模式语言和模式模板的验证功能,进一步从工程上验证了本文所提出的模式语言相关概念以及算法的有效性。综上所述,使用模式语言可以增强规约的描述能力,通过调用模式库中的模式模板,可以快速将自然语言规约表示为相应的形式化规约,从而简化自然语言规约向形式化语言规约转化的过程,降低开发人员构造形式化规约描述性质的门槛。