Formal Modeling And Verification Of Communication Mechanisms In ROS

With the continuous development and transformation of artificial intelligence and robotic technology,robots are gradually entering various fields of human production and life.Therefore,the Robot Operating System(ROS)has been widely used and it has attracted the attention of academia and industry.For example,ROS security testing and verification have become one of the hot issues in this field.As the most basic function of ROS,the communication mechanisms play an irreplaceable role in ensuring the correctness and safety of the system.Furthermore,ROS security should not only be verified from simulation and testing,but also formal methods must be used to ensure the completeness of security verification.Therefore,this paper analyzes the source code of the ROS from the perspective of formal verification and extract the relevant communication mechanism,that is,the implementation scheme based on the three communication mechanisms of topic,service,and action.Then establishes the corresponding formal model,and verify the safety and reliability of related communication mechanisms in UPPAAL.The main works and contributions of this paper are as follows:First of all,we analyze summarily all the source codes of ROS,extract and establish the core source codes scope of ROS to achieve the above three communication mechanisms.On this basis,the research gives a class diagram of each communication mechanism.For the topic-type communication mechanism,we discuss and analyze specifically the respective functions implementation of the publisher class and the subscriber class,the relationship between each other,and the(publisher)message publishing process and(subscriber)message subscription process;for the service-type communication mechanism,we discuss and analyze specifically the realization of the functions of the server class and the client class,the relationship between each other,and the(client)request message flow and the(server)response message flow;for the actiontype communication mechanism,we discuss and analyze specifically the server class and the client class implementation of their respective functions,task state machine,(server)simple scheduling strategy and(client)task cancellation strategy.Then,on the basis of studying the UPPAAL model construction patterns and principles of abstraction from source codes,For ROS communication mechanisms,we come up with the formal modeling and verification technical route.According to the analysis results of the three ROS communication mechanisms based on the source codes,the corresponding UPPAAL formal models are established.For the topic-based communication mechanism,formal verification is carried out on the security attributes of publishers and subscribers such as queue overflow and deadlock;for service-based communication mechanism,the security attributes such as the reachability and liveness are respectively verified in formal;for action-type communication mechanism,the deadlock of the task state machine of the client and the server,the scheduling,preemption,and the uniqueness of task execution of the server's simple scheduling strategy,and the task cancellation strategy reachability of the client have been formally verified one by one.All the above verification results show that the corresponding communication mechanism satisfies the corresponding security attributes,thereby verifying the security and reliability of the ROS existing communication mechanisms.In addition,test cases for reliability on the above three communication mechanisms has been designed and the corresponding application programs are implemented.The results lend further support the feasibility of the technical route of the formal verification in this paper and the credibility of the former verification conclusion.In this paper,the main innovative contributions include the proposal of formal modeling and security verification technical route of ROS communication mechanisms based on source codes analysis,and formal verification of security attributes related to them.In the future,further research can be carried out on the design and implementation of formal verification tools and the automatic construction of formal models based on source codes.