Research Of Formal Method & Model Checking Technology On Service-oriented Robot Control System

In the domain of robot controlling,service-oriented control system can improve the reusability and scalability of robot control system.By using formal modeling method and model checking technology,it can improve the efficiency during development and guarantee the performance requirements of system.Formal modeling method unifies the design and implementation process,which can reduce repetitive coding workload in system developing.And using model checking technology in simulation and checking can verify the usability of robot control system.The main purpose of this thesis is researching the implementation of formal modeling method of MDA(Model Driven Architecture)and model checking technology of verification in robot control system.This thesis uses formal modeling method to specify robot control system,designs and build the modeling environment of robot control system;Uses model checking technology based on time automata and designs the checking model of robot control system;Designs the checking model based on SMC(Statistical Model Checking)technology to solve state explosion problem;Proposes componentization code generating technology,which can auto transforms the models and auto generates the code of robot control system.Finally,simulates and verifies the models of service-Oriented Robot Control System,which can guarantee the feasibility and reasonability of the auto componentization generating code,and experimental comparison results of codes show that the auto componentization generating code has more advantages in robot control system development.