Automatic Test Case Generation from Formal Requirement Model for Avionics Software

The scale and complexity of software in modern avionics systems are growing fast. It becomes a challenge to develop such kind of software systems satisfying both high safety and reliability requirements. This paper presents a framework of automatic test case generation for avionics software form formal requirement models. We introduced a specific formal model of VRM (Variable Relation Model), which is used for modeling the requirements of avionics software, from which control tree structures are established. Different model test coverage criteria are defined according to the DO-178C standard to simplified the control tree structure, and test path constraint selection methods are proposed based on those criteria. Through performing domain error test case selection, test cases are generated for each path constraint selected, which makes up a test case set for the requirement. At last, to demonstrate how we generate test cases form a requirement model, a case study is given.