Research On Test Case Generation Technology Based On NuSMV Model And ANTLR

Under the background of complex structure and diversified functions of the safety-critical system,the probability of software accidents is increasing.A testing software system can reduce the risk of accidents and improve system security.However,the adequacy of the tests needs to be evaluated by performing many test cases.It is very urgent and necessary to research the generating method of test cases to improve the quality and efficiency of test cases.Therefore,from the requirement and source code two points of view,this thesis describes the route and method of obtaining test cases and is committed to improving the quality of test cases and generati on efficiency.The main research work of this thesis is as follows:1.From the perspective of the requirement,on the route of obtaining test cases,the level switching scenario from China Train Control System 2(CTCS-2)to China Train Control System 3(CTCS-3)in the train control system is selected as a case.The agent theory is introduced to describe and analyze the complex scenario.The relationship among multiple agents is established based on the level switching process,and the attributes such as safety,environment and function are extracted.According to the abstract information interaction relationship between individual and multiple agents,Nu SMV is used for formal modelling.The model checking technology is used to verify the specification in Computation Tree Logic(CTL)form to obtain the counterexample path and modify the counterexample path to obtain the function test case set.2.From the source code perspective,on obtaining test cases,select the code in the form of C language as the research object,and introduce Another Tool for Language Recognition(ANTLR)as the analysis plug-in to analyze and process the source code.The constraint rules for selecting branch statements are proposed,the nodes of all types of program statements are analyzed,the program execution order is expressed using the data structure in the form of a graph,and the key logic information is obtained simultaneously.It lays the foundation for the test case generation.3.Based on Modified Condition/Decision Condition(MC/DC)coverage criterion,this thesis expounds on the concept of a minimum complete test case set of logical operators,uses a binary tree to represent Boolean expression,and puts forward MC/DC test case generation algorithm of a Boolean expression.In addition,this thesis also makes the corresponding MC/DC analysis of various types of program structures and uses Satisfiability Modulo Theorie(SMT)solver to calculate the binarization test sequence.Then,the causes of redundant test cases are described,and the redundancy filtering method of the test case set is proposed.Finally,the theory in this thesis is tested and analyzed.It is concluded that the method in this thesis can produce a test case set that meets the MC/DC standard,which shows the feasibility of the method in this thesis.This thesis constructs a test case generation model from different requirements and source code angles.It obtains the test case set that automatically meets the high coverage standard to a certain extent,which is of great significance to the automatic generation of test cases.