基于形式化测试的实时系统变更后安全性验证
摘要
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 veri cation are the popular applied automatic safety veri cation 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 veri cation 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.