论文部分内容阅读
随着软件系统的复杂化和大型化，保证软件可靠性变的越来越重要。运行时验证作为一种轻量级的的验证框架，它同时具备了形式化方法的准确性和测试的方便性，同时也避免了模型检测的“状态空间爆炸”问题。近些年来，它逐渐成为验证领域的研究热点。面向监控器的编程(Monitor Oriented Programming，简称MOP)是运行时验证中使用的比较多的框架，而其核心组件是一个监控器，在在线验证中，监控器会集成到目标程序中和程序一起运行。因此，对于监控器的开销控制也变的十分重要。 本文主要研究了MOP的一个实例：JavaMop，并重点研究了使用线性时态逻辑(LTL)描述的属性插件。该插件在处理LTL描述的属性时，LTL公式会先被转换成一个büchi自动机，然后该büchi自动机会被转换成为一个确定化的有穷状态自动机(DFA)。但是，在JavaMop中这个转换过程存在两个问题：第一，LTL公式生成的büchi自动机大小并不是最优的。第二，在后续的从非确定性的有穷状态自动机(NFA)到确定化的有穷状态自动机(DFA)的转换过程中，自动机的状态会成指数级增长。这些都会导致最后生成的监控器的大小过大，从而可能造成内存溢出等问题。本文通过在原有的转换过程中添加一个化简büchi自动机的步骤来解决这两个问题。主要工作总结如下： (1)本文研究了JavaMop中原有的从LTL公式到DFA的转换过程中所存在的缺陷。本文针对这个缺陷在其原有的转换算法中添加了一个化简的步骤，对原有的转换算法进行优化。 (2)本文结合运行时验证和模型检测的相似性，将模型检测中基于Fair simulation的büchi自动机化简算法用在了该化简步骤中，并针对该化简算法的运行时间慢的问题。在使用该算法前添加了一个预处理的过程对自动机进行初步的化简，进而可以加速该化简算法的运行，化简后本文可以减少得到的DFA的大小，最终减少的到的监控器的大小。 (3)通过使用本文工具对几个不同的程序进行验证，并对比实验结果和程序默认的结果，可知本文工具的设计是正确的。通过时间和内存的开销对比，可知，本文工具在内存开销上要少于JavaMOP。