Improving testing coverage for safety-critical system by mutated specification

Automation and high coverage are two essential industrial technical requirements of qualified testing method for safety-critical systems. The ioco-testing method is a sound and well-defined formal automation testing technique for labelled transition system. However, when we apply this method to a train control system developed by our industrial partner, we find that some testing requirements are not covered for certain testing objects. Further analysis has shown that the ioco-testing method only generates test cases based on explicit specified system behaviors which may result in low coverage when the implementation under test includes code branches used to deal with faults which can't be defined thoroughly in the specification in practices. Therefore, we propose a labelled transition system testing method based on specification mutation to improve safety-critical system testing coverage. We firstly define the mutation operators for the Input output symbolic transition system (IOSTS) modeling language, then we construct the corresponding test generation algorithm and translate the derived test cases into xml files which can be directly applied to the implementation under test in a simulation and test platform developed by our partner. Preliminary experiments on a safety-critical function named train position determination have shown about 28.5% improvement on the testing coverage.