基于运行时验证的监控器生成技术研究

【摘要】：运行时验证是一种轻量级的验证技术,其验证过程伴随目标系统的实际运行。它是传统验证技术的有效补充,在许多领域逐渐受到人们的关注,并被具体运用到众多对系统安全性有着较高要求的行业。在运行时验证过程中,针对需求将待监控的性质采用某种时序逻辑进行描述,例如用线性时序逻辑(LTL)公式来描述,再根据性质公式构造监控器。由于运行过程只能观测到系统的有穷执行路径,因此传统的运行时验证技术多是把时序逻辑的语义改造成为基于有穷路径的二值语义,这使得使监控结果不能与时序逻辑性质的监控需求保持一致,并且在监控的预测性方面存在不足。本文根据已有的三值语义的监控方法,为了便于监控器的自动生成,基于交错Büchi自动机对该方法进行了改进。首先将具有三值语义的LTL公式转化为一个交错的Büchi自动机,该转换过程的时空开销均为线性;接下来,将所得交错Büchi自动机转换为非确定的Büchi自动机;最后将该自动机进行确定化,从而得到能够高效运行的监控器。本文提出了两种策略对Büchi自动机的优化:一是通过识别Büchi自动机中强连通图,并对其状态进行删除或合并;二是对Büchi自动机中每一个状态进行判空操作,去掉对应语言为空的状态。通过这样的优化,有效的降低了所生成监控器的规模。以上述方法为基础,本文对Java MOP监控工具进行扩展,使其能够支持三值LTL监控器的生成,并在美国航空航天局(NASA)的“火星车仿真软件Maestro”以及某“月球巡视器”系统中进行了实验,取得了良好效果,从而验证了上述方法的可行性以及原型工具的有效性。
【关键词】：运行时验证 软件监控器 线性时序逻辑 交错自动机 Büchi自动机
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP311.53