Modeling and Analyzing Flight Control Software of Unmanned Aerial Vehicle Using UML and B Method
作者： Jiufu Liu , Jianyong Zhou , Chunsheng Liu , Zhong Yang , Zhisheng Wang
关键词:
摘要: B is a formal method which enables the automatic generation of an executable code through successive refinements from abstract specification. Unified Modeling Language (UML) specifications can be formally verified by analyzing corresponding specification, and integration UML overcomes drawbacks UML. In this paper Class diagram flight control system presented each class operation mapped to machine. The software behaviors are in form statecharts adopted translate into specification software.Using method, refined failure management added. Finally proof obligations ensure safety for ertical artificial navigation UAV.
jsoftware.us
sci-hub.st 参考文章(12)
Hung Ledang, Jeanine Souquières, Integrating UML and B Specification Techniques The Informatik 2001 Workshop on Integrating Diagrammatic and Formal Specification Techniques. pp. 641- 648 ,(2001)
Colin Snook, Marina Waldén, Refinement of statemachines using event b semantics Lecture Notes in Computer Science. pp. 171- 185 ,(2007) , 10.1007/11955757_15
Xiao Liang, Jundong Zhang, Yu Qin, Hongrui Yang, Dynamic Modeling and Computer Simulation for Autonomous Underwater Vehicles with Fins Journal of Computers. ,vol. 8, pp. 1058- 1064 ,(2013) , 10.4304/JCP.8.4.1058-1064
Chunyu Miao, Dynamic Slicing Research of UML Statechart Specifications Journal of Computers. ,vol. 6, pp. 792- 798 ,(2011) , 10.4304/JCP.6.4.792-798
Akram Idani, Yves Ledru, Dynamic graphical UML views from formal B specifications Information & Software Technology. ,vol. 48, pp. 154- 169 ,(2006) , 10.1016/J.INFSOF.2005.03.008
Amel Mammar, Régine Laleau, From a B formal specification to an executable code: application to the relational database domain Information & Software Technology. ,vol. 48, pp. 253- 279 ,(2006) , 10.1016/J.INFSOF.2005.05.002
Manoranjan Satpathy, Michael Leuschel, Michael Butler, ProTest: An Automatic Test Environment for B Specifications Electronic Notes in Theoretical Computer Science. ,vol. 111, pp. 113- 136 ,(2005) , 10.1016/J.ENTCS.2004.12.009
Liu Jiufu, Integration of statechart and B method based analysis and verification for flight control software of unmanned aerial vehicle ACM SIGSOFT Software Engineering Notes. ,vol. 32, pp. 1- 4 ,(2007) , 10.1145/1234741.1234759
Lina Chen, Automatic Test Cases Generation for Statechart Specifications from Semantics to Algorithm Journal of Computers. ,vol. 6, pp. 769- 775 ,(2011) , 10.4304/JCP.6.4.769-775
H. Ledang, J. Souquieres, Modeling class operations in B: Application to UML behavioral diagrams automated software engineering. pp. 289- 296 ,(2001) , 10.1109/ASE.2001.989815