UML and B Method Based Analysis and Refinement for Flight Control Software of Unmanned Aerial Vehicle

B is a formal method which enables the automatic generation of an executable code through successive refinements from an abstract specification. unified modeling language (UML) specifications can be formally verified by analyzing the corresponding B specification, and integration of UML specifications and B method can overcomes the drawbacks of UML. In this paper the class diagram of the flight control system is presented and each class operation is mapped to a B abstract machine. Statemate, one tool supporting the virtual prototype technology, is used, and the flight control software behaviors are presented in the form of statecharts The B method is adopted to translate the statecharts. into B specification of flight control software. Using UML and B method, flight control is refined and failure management is added. Finally the architecture of B specification derived from classes and statecharts diagram is built.