Formal Research Based On RT-middleware Data Transfer Protocol

The robot is a complex intelligent machine that combines various disciplines such as mechanics,electronics,computers,sensors,control technology,artificial intelligence and bionics.It has become one of the research hotspots in the world.In recent years,due to the development of robotics,more and more software frameworks for driving robots have been applied to commercial robots.The service groups of these products are often non-professionals,so the security of software and software frameworks for driving robots is also getting more and more important.RT-Middleware is a software framework for building robots,the data transmission protocol based on RT-middleware is the basis of the data transmission of the robot software framework.The former used the method of model checking to verify it.However,when describing the formal model defined by it,only three sets of data were used to explain that the formal model of its definition satisfies the formal specification of the protocol,and there is a problem of state space explosion,this paper uses the theorem proving method in the formal method to formally verify the protocol.Firstly,the formalization method is introduced.The three common method principles,advantages and disadvantages of formal verification are analyzed.The HOL4 system in the theorem proof is the main one.The history,logic,proof method,countermeasures and policies of the HOL system has been studied in depth,and then the general method of formalization using theorem proving is given.The implementation and specification of the protocol are formalized.Based on the implementation model of the protocol,a series of properties and lemmas are proposed to ensure the validity of the protocol implementation model,and finally complete the proof of deriving the specification model by the implementation model,prove the reliability of the data transmission protocol based on RT-middleware,and give some inspiration to the subsequent use of theorem proving to verify other applications based on RT-Middleware.