Automated Verification Of The Completeness Of CTCS-3 Test Cases

As the key to ensure the efficiency and the safety of high speed railway system, the CTCS-3(Chinese Train Control System Level 3) is firmly required to have excellent safety and reliability performance. In order to guarantee that the system behaviors of CTCS-3 are in accordance with the requirements specified in "CTCS-3 System Requirements Specification(SRS) (v1.0)", a comprehensive test to verify the functions of CTCS-3 is necessary to be taken. Moreover, the basis and the standard of the test are formed by "Test Cases for CTCS-3(v3.0)". The completeness of the test cases is the key to assure the integrality of the test. Thus, to ensure the completeness of the test cases, a completeness verification approach for test cases of CTCS-3 is proposed in this paper.The main works of this thesis are as follows.(1) On the basis of analyzing the features of the test method and the test cases of CTCS-3, the main requirements and the key issues which must be addressed in the process of verifying the completeness of CTCS-3 test cases are determined.(2) A verification process based on Event-B and Cause-Effect Graph method is presented. The formal model of SRS is established rigorously with Event-B and transformed into cause-effect graph. The decision table of SRS is generated according to the cause-effect graph of SRS. Then, the cause-effect graph of test cases is established and transformed into test cases decision table to unify the description schemes of SRS and test cases. Finally, the basis for measuring the completeness of test cases is obtained based on the SRS decision table, and the verification result is acquired through the comparisons between the SRS decision table and the decision table of test cases.(3) In order to implement the verification process mentioned above, several methods are proposed. The rewriting and mapping rules of Event-B model are determined to realize the model transformation from Event-B model to cause-effect graph. To clarify the corresponding relations between SRS and test cases, a method that establishing the test cases cause-effect graph based on the events in SRS cause-effect graph is proposed. Moreover, the test adequacy criterion and the test coverage domain are designed according to the SRS decision table. Furthermore, a comparison process is designed to acquire the verification result which can be easily used by the test designers.(4) Based on the verification method proposed previously, a tool is designed and developed to automatically verify the completeness of test cases in collaboration with the Rodin platform. Taking mode transition functions under SB mode and RBC switching functions as examples, the completeness of relevant test cases is verified. The result indicates that the method and the tool presented in this paper are suitable for verifying the completeness of CTCS-3 test cases and finding out the possible problems in the existing test cases.