Test Generation from StateChart and B method for flight control software of unmanned aerial vehicle

摘要

The growing complexity of flight control software of unmanned aerial vehicle led up to more and more difficulty in testing such systems. B is a formal method which enables the automatic generation of an executable code through s succession of refinements from an abstract specification. UML specifications can be formally verified by analyzing the corresponding B specification. Integration of UML specifications and B method can overcomes the drawback of UML. We adopt the tool Statemate which support the virtual prototype technology. The detailed description of flight control software behaviors is presented based on statecharts. Then we adopt the B method to translate the statecharts into B specification of flight control software. According to software testing criteria MC/DC, we are easy to obtain the test cases based on StateChart and B method.