Validation Verification Of The Rules For Unmanned Vehicles' Decision System

With the development of information technology,the technology of unmanned vehicles has been one of the most heated areas in scientific research.Many countries have spent lots of money and time on it.Unmanned vehicles can free human drivers from their boring and dangerous work.It can also reduce the randomness of the vehicles' behavior and make it more predictable.So that it will improve the stability of the traffic.Moreover,unmanned vehicles can improve the vehicles' reaction speed to the environment thus strengthen the security of the traffic.At the same time,it can extremely shorten the distance between vehicles so that the transportation capacity of the road will be increased.In addition,it can improve the measuring precision of the environment.Also,it will put an end to the traffic accidents caused by the personal factors of human drivers.The central part of the technology of unmanned vehicles is the development of the decision system.However,this part of work is facing the following problems: The code directly written by the developers costs a lot and is hard to maintain;the decision rule and the application are mixed together;there may be errors and defects hidden in the designation;the process of software development and security checking are not synchronized.Aiming at these problems,this paper presents a development framework of verification-driven unmanned vehicle's decision system based on automatic code generation.The early work of our team include designing an inter-code language to describe the rules of unmanned vehicles and designing and implementing a tool for rule editing and code generation automatically.So that the first two problems has been solved.In order to solve the problems of security,in this paper,we introduce the technology of model checking based on the code generation automatically.We generate the modelling code of unmanned vehicles and model the environment of them.With the procedure of formal verification,we can find the errors and defects that hide in the designing process.With this method,the problems of insufficient security can be solved.This can also reduce the maintenance cost by synchronizing the process of software development with security checking.Based on this development framework,the tool named UNMANNED_RULE_EDIT(URE)equipped with model checking module is also implemented to support their work and assure their security.