基于形式化测试的实时系统变更后安全性验证

变更后系统实现的安全性验证是安全攸关系统维护过程中必不可少的环节,也是其面临的主要挑战之一.软件模型检测和程序验证是目前常用的作用于代码层面的自动化安全性验证技术.本文站在系统行为角度,基于形式化方法,提出了一种将变更后系统实现的安全性验证问题归结为一致性测试的方法,尝试通过自动生成的一致性测试用例在系统行为级别上判定系统实现是否安全.为此,首先以时间输入输出自动机及其语义模型为基础,构建了该方法的证明体系,证明了该方法的正确性;其次,建立了变更后系统实现安全性验证的回归测试生成框架.相对于其它实时系统测试方法,这种测试方法不仅可以发现实时系统中常规的不一致性缺陷,而且为变更后系统实现在运行时是否满足指定的安全性属性提供了依据.最后,以轨道交通系统中的列车自动防护功能的变更情景为案例研究,说明了方法的具体应用.

A safety verification approach for changed real time implementation based on formal testing

It is necessary and competitive to verify the desired safety properties on the changed implementation during the maintenance phase of a safety critical system. Software model checking and program verification are the popular applied automatic safety verification techniques on the program level. In the paper,we propose a formal testing method for the system behaviors which tries to verify the desired safety properties for the changed implementation by means of conformance testing. Firstly,we prove the correctness of our method based on timed input/output automata and its semantics model. Secondly,we present a regression testing generation framework of safety verification for the changed implementation. Compared with other real time testing methods,our method can not only detect the common non-conformance defects but also conclude the satisfaction with the desired safety properties. The method is illustrated with a changing requirement of the automatic train protection function in the train control system.