Research On Safety Software Testing Based On Multiform Clocks Input Output Transition System

The lack of systematic and scientific testing theoretical foundation is the primary problem that has always affected the credibility of safety-critical software testing.As a result,the actual system safety status may be worried about during its operation.And moreover,the problem is becoming more and more serious under the continuous increased demand,responsibility scope,complexity and scale of safety software.In the dissertation,we propose a safety testing theoretical framework and the corre-sponding test sequences generation method based on formal testing.Our method takes the views from the analysis and design phases rather than testing phase itself and proves that testing can also guarantee the correctness of safety-critical software.We begin our research with the construction of a new modeling language satisfying safety-critical soft-ware characteristics and then construct the integration testing theoretical framework of safety verification and safety testing.The main contributions of the dissertation includes:1.We define the multiform clocks based time model,propose a new safety-critical soft-ware modeling language named multiform clocks input output symbolic transition system(MCIOSTS),define its corresponding formal syntax and semantics and put for-ward the modeling method which separates time modeling from behavior modeling;2.We construct the integrated theoretical testing framework of safety verification and safety conformance testing,prove that if the implementation can pass test sequences that generate from the specification model satisfying the expected safety properties,the implementation also satisfies these safety properties;3.We develop the safety testing method for MCIOSTS based on our proposed testing framework,define the multiform clocks input output conformance relation and design the corresponding symbolic testing algorithms.Moreover,in order to satisfy with the fault testing requirements,we propose a fault test sequences generation method based on mutated MCIOSTS specifications.We design the related mutation operators and their weakly-killing guidance rules.To cover expected faults as soon as possible,the k-cycled guided testing algorithm is also developed.The application of our method is demonstrated with a real on-board automatic train control software which is one of the highest safety level systems in a train control system.