本站原创摘 要 ：本文结合作者课题内容,介绍了一种运行时验证技术中的监控器构造方法.该方法完整涵盖了从性质规约到监控器模型再到监控程序的全过程,过程中使用了相关开源的第三方软件使得该方法的自动化程度较高.同时由于该监控器的构造是基于三值语义,使得该监控器在一定意义上具有预测性.
关 键 词 ：运行时验证；监控器模型；监控程序；三值语义
中图分类号：TP311.52 文献标识码：A 文章编号：1007-9599 （2012） 20-0000-02
1.引言
运行时验证[1]是一种新兴的轻量级程序验证技术.在运行时验证中,通常从系统需求中产生监控器,监控器通过观测程序的执行来检查程序运行过程是否满足系统需求,是传统的软件验证和确认技术,比如测试[2]和模型验证[3]的有效补充.它不但可以有效的检测系统运行中的异常行为,而且也使得在检测到正确性背离时有效地修复系统成为可能.
本文结合作者课题中的相关工作,介绍了一种运行时验证监控器构造方法,该方法结合LTL3 Tools监控器模型生成工具以及JaMOP软件开发工具支持和分析框架,其完整的流程图如图1所示.
论文的组织如下：第二节结合案例介绍如何使用LTL3 Tools工具生成监控器模型即F（finite-state machine, 有限状态机）,第三节结合案例介绍如何将监控器模型经过相应处理后,通过JaMOP生成成为监控程序.最后进行总结.
2.监控模型的生成
在运行时验证领域,LTL[4]（Linear Temporal Logic,线性时序逻辑）被广泛的应用,相应的监控性质要通过LTL公式进行描述.LTL公式的预测语义,也称三值语义[5]（简称LTL3）.相较典型的已经被定义而且使用于运行时验证工具的有穷轨迹上的两值语义（true/false）监控器,基于三值语义的监控器非常适合于运行时验证.一方面,三值语义的公平性使得监控器的裁决始终是正确的,另一方面,三值语义的预测性使得监控器有发现一条无穷运行轨迹的最小好[6]（坏）前缀的能力,即监控器能尽可能早的作出裁决,因此在一定意义上具有预测性.所以本文的监控器构造也将使用三值语义.三值语义监控器的理论构造过程请参照文献[7].
LTL3 Tools是一个将给定LTL公式φ转换为F（finite-state machine, 有限状态机）表示Mφ的工具集.该工具集为免费使用,在网上可以下载.F可以看作是一个基于三值语义的监控器模型,输入有穷字u,它会判断出是否公式成立.
这里结合一个案例,进行介绍：
对一个软件监测以下需求：直到init后才进行spawn,即只有初始化以后才能调用spawn操作.对应的LTL规约为： !spawn U init
通过ltl2mon（该程序为LTL3 Tools输入规约的入口）程序输入以下命令：$./ltl2mon "（! spawn） U init" | dot -Tps > graph.ps得到对应的F格式的监控器.得到监控器自动机的图形化表示为：
其中,是起始状态,绿色是安全状态,红色是不安全状态.
生成监控器的结果也可以通过如下命令 $ ./ltl2mon "（! spawn） U init" -itest.f > test.txt输出到txt文档中,形成一个文本格式的自动机描述如图3所示：
3.监控程序的实现
我们的最终目的是对定义的LTL规约,生成相应的监控程序.这里我们将使用到JaMOP,它是一个基于Ja的面向对象编程（MOP）软件开发工具支持和分析框架,它支持将F等逻辑转化为Ja程序的监控器,支持面向方面编程的编织模式,是一个自动化程度较高的运行时验证框架.JaMOP有相应的逻辑处理层,用于处理各种逻辑,将其转换成Ja语言的表达方式,并且有相应的处理层根据目标Ja文件输出相应面向方面的监控器表达.
在之前的案例中得到监控器模型的基础上,通过JaMOP生成监控程序的过程如下.
1）对test.txt中描述的的监控器,去除重复和空的迁移条件,例如”label等于
2）按如下命令jamop test.mop执行,得到对应的面向方面文件TestMonitorAspect.aj.
由于作者课题中所考虑的领域基本上都是由C或C++实现,因此没有使用JaMOP的植入功能,即在相应节点中插装一些程序段用于获取监控所关注的系统信息,而主要利用其生成监控程序的功能,这使得作者课题中还为了获取相应的程序信息做了大量的相关工作.如果针对的是由Ja实现的程序,直接利用JaMOP的植入功能将使从目标程序中获取信息环节的工作可以由程序自动完成.作者主要使用其中生成的监控器代码,它位于TestMonitor类中,是一个监控器类,完成自动机的功能.图4是案例中最终生成的监控程序中的一段实现监控器监控过程（即根据观察到的事件发生迁移）的代码,其中利用数组表示不同事件在不同状态时发生的迁移.
图4.案例监控程序中实现监控器监控过程的代码
4.总结和下一步工作
本文结合作者课题中相关内容,介绍了了一种运行时验证监控器的构造方法,该方法结合使用了开源的第三方软件LTL3 Tools和JaMOP,使得其自动化程度较高. 在下一步工作中作者将结合其他课题的工作将该方法整理成一个类似于已经成熟应用的运行时验证工具集Ja-MaC[8]一样的工具,只通过输入相应的监控性质就能完全自动的生成相应的监控器程序.