Research On Automatic Generation Method Of Test Case For Aviation Software

Software testing occupies very important position in the development process of software.It is a critical step to ensure software quality.Because of aviation software with the characteristics of real-time, embedded and high reliability etal,to carry out rigorous software testing is essential.Test case generation is the core issue in software testing.The research of automatic generation method of test case for aviation software has important theoretical significance and practical value to improve the reliability of aviation software.In this paper, taking aviation software --satellite navigation systems as the project background, first,make a in-depth analysis of all kinds of methods and research results of automatic generation of test cases at home and abroad.On the basis of above mentioned study,research a based on model checking method of automatic generation of test cases. Combined with Gray box test process which applied for aviation software, put forward a test process of automatically generating test cases which based on software requirment and taking use of model checking.The process involves the abstraction of software requirements,establishing formal system model according to software requirements, sequential logic transformation based on testing criteria, consistency verification between software requirements formal models and temporal logic and the refining of test cases and so on.Secondly, according to aviation software testing standard DO-178B,this paper presents a Boolean operator replacement algorithm to construct the sequential logic, the test cases which generated by inputing the converted temporal logic to model checker can meet MC/DC coverage criterion.In the end the paper aimed to the process of automatically generating test cases,design and develop an automatic generation of test cases based on the model checking tool.In terms of satellite navigation system software testing process, verify availability of the proposed method of automatic generation of test cases by using the tool as auxiliary tool to design test cases and designing test-driven template and making structural coverage analysis.