论文部分内容阅读
在国民经济与国防现代化建设中,计算机软件在日常生活中的应用越来越普及,软件可靠性问题日趋受到人们的重视,尤其对于一些安全关键领域,如载人航天、高速轨道交通等。应用于这些领域的系统通常是实时控制系统,这类系统不仅要求系统做出正确的响应,且要求系统的响应满足相应的时间约束。系统一旦发生失效,将会给国家安全乃至人员生命带来极大损失,因此如何提高这类系统的可靠性成为目前计算机领域的一个非常重要的研究内容。传统的测试方法由于存在测试用例不完备等问题无法满足系统的可靠性需求,模型检测能给出系统完备的正确性证明,但是对于复杂系统来说,这一技术面临着状态空间爆炸等问题。运行时验证作为测试和模型检测的有效补充,在系统运行过程中实施有效地监控与验证,尽早地发现软件失效,有助于提高实时系统的安全性和可靠性。为了提高实时系统的安全性和可靠性,本文提出一种基于度量区间时序逻辑(Metric Interval Temporal Logic, MITL)三值语义的运行时验证方法,主要工作如下：1、介绍了pointwise语义模型下MITL在有穷轨迹上的语法及语义,采用pointwise语义模型是因为MITL在该语义模型下是可判定的,定义了MITL在有穷轨迹上的三值语义,与LTL三值语义不同的是,它是在有穷时间字上进行解释的。2、本文定义了基于MITL三值语义的监控器的形式化描述,即基于迁移的扩展时间Buchi自动机(transition-based generalized timed Buchi automaton, TGTBA),它是在基于迁移的扩展Buchi自动机的基础上,通过增加时钟约束得到的。在此基础上,研究了一种构造预测监控器的方法,即采用逻辑重写的方法,根据给出的重写算法将公式重写为要求的形式,基于重写后的公式来构造TGTBA,将此TGTBA作为MITL公式的预测监控器,用于运行时验证过程中。3、在上述验证方法和MaC验证框架的基础上,将基于MITL的预测监控器应用于MaC框架中,实现了基于MITL三值语义的运行时验证原型工具MITL RV,并使用原型工具对铁路交叉路口控制系统进行运行时验证分析,且实验证表明,该方法是有效的。