论文部分内容阅读
随着信息技术的发展，计算机技术已经融入了现代社会各个领域，得到极其广泛的应用。然而在这样的背景下，计算机系统的异常可能会造成灾难性后果。 测试和仿真通常被用来保障这类安全关键系统的可靠性，但是这类方法针对的是实际运行前的系统，只能检测到系统的错误，而不能证明系统的正确。模型验证是完备的，但是它针对的是系统的抽象模型，难以证明系统的抽象模型和实际系统的等价性，同时这种方法需要遍历系统的所有执行路径，对于复杂系统来说，容易产生组合爆炸问题。 与传统的测试和模型验证技术不同，运行时验证针对的是正在运行的实际系统。运行时验证一般采用时态逻辑来描述要验证的需求规约，并根据需求规约构造监控器。利用UML序列图来描述要验证的需求规约，克服了时态逻辑等形式化方法使用复杂的问题，使得普通的软件工程师也能方便正确的描述要验证的需求规约或性质。研究基于时间属性序列图(TPSD，Timed Property Sequence Diagram)自动生成监控器来进行运行时验证就显得十分有意义。 本文提出了基于UML2.0时间属性序列图的运行时验证方法，其具体思想是使用时间属性序列图来描述要验证的需求规约，然后为序列图中的每个对象构造时间对象自动机，将整个序列图转换为时间自动机网络，以构造出运行时验证中所需的监控器，监控器监控目标系统的执行轨迹，判断目标系统的当前执行是否满足需求规约。本文先给出了满足本文验证需求的时间属性序列图形式化定义，接着提出了时间对象自动机及其形式化定义，然后提出了基于时间属性序列图的运行时验证方法的基本原理，进而提出了将时间属性序列图转化为时间自动机网络来构造预测监控器的算法。在此基础上，本文利用上述原理构造了一个基于时间属性序列图的运行时验证工具TPSD_monitor，构造了一个列控系统CTCS-2向CTCS-3级间切换仿真程序作为要验证的目标系统，利用该工具对构造的目标系统进行运行时验证，说明了本文中方法对安全关键系统进行运行时验证的可行性。进而进行了性能对比试验，实验表明，本文的监控器构造方法所产生的监控器运行开销较小，且能在一定程度上缓解监控器生成过程中的组合爆炸问题。