论文部分内容阅读
随着计算机技术的发展,软件系统的可靠性问题越来越受到人们的重视。尤其对于安全关键系统,如何提高此类软件系统的可靠性已成为一个非常重要的研究方向。测试方法可以提高系统的可靠性,但其存在不完备性问题。模型检测具有完备性,但是需要建立系统的抽象模型,而且对于复杂系统来说,模型检测容易产生“状态空间爆炸”等问题。运行时验证技术是传统验证方法的有效补充,能够尽早地发现软件系统故障,有助于提高软件系统的可靠性。运行时验证关注的是软件系统的实际执行是否满足待验证的需求规约,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点,目前基于可视化需求规约场景的运行时验证技术还存在以下不足：(1)已有的验证方法容易产生冗余性质,验证开销较大,且二值语义的验证结果是不准确的。(2)已有的基于Maude工具引擎的重写逻辑运行时验证算法的效率较低,不利于快速的发现系统故障。针对现有的运行时验证技术存在的不足之处,本文的主要工作有：(1)分析已有的验证方法的不足,提出一种基于活性顺序图的运行时验证的改进方法。该方法使用代码插装获取系统执行轨迹,使用活性顺序图描述需求规约场景,为了支持现有的运行时验证技术,基于活性顺序图到LTL公式的基本转换过程,利用图中性质的传递性化简转换所得的LTL公式的规模,然后基于有穷轨迹上LTL三值可执行语义,实现针对系统执行轨迹的离线方式的运行时验证。(2)针对基于Maude工具引擎的重写逻辑运行时验证算法的效率较低问题,使用轨迹状态消耗的思想,根据Maude工具引擎的特点,引入操作符的缓存机制,提高公式重写的效率,以便快速的发现系统故障。(3)设计验证工具和完整的实验实例,为了证明本文提出的改进方法的可行性,本文设计并实现了运行时验证工具RVT4LSC,并使用该工具验证ETCS-2级列车运行控制系统中RBC/RBC切换场景,实验结果证明了本文改进方法的可行性。然后进行了对比性实验,实验结果表明,本文采用的转换方法将产生更小规模的LTL公式,能有效降低运行时验证的开销。