Modeling And Verification Of Unmanned Driving System Of Mine Locomotive Using Timed Automata

Mine locomotive unmanned driving is an effective way to improve the level of China’s mine production automation,to reduce the number of underground workers,thus reducing casualties in mine accident.As a safety critical system,it has high safety requirements,so it is necessary to use formal methods to verify design correctness in the system design stage.Based on the characteristics of unmanned driving system of mine locomotive,this dissertation proposes a method to model and verify the unmanned driving system of mine locomotive which is composed of several components and has fail-safe requirements.And autonomous driving and telecontrol driving process were modeled and verified using this method.The main work of this dissertation is as follows:(1)Through analyzing the unmanned driving process of mine locomotive in some typical operating scenarios,the data exchange scheme in the form of data table and the overall procedure of the unmanned locomotive control process are put forward according to the data characteristics of the system.(2)According to the characteristics of unmanned driving process of mine locomotive,this dissertation puts forward a method to model and verify its design correctness.The method is divided into five steps.First,specify the verification requirements.Second,define the fundamental data tables of the system.These data tables are crucial to drive the mine locomotive unmanned driving model;Third,model decomposition.For complex objects,decomposition can reduce the complexity of single model.Fourth,model construction,in the method a map from system design details to the grammatical elements of the model is introduced.Fifth,model checking.(3)Based on the method proposed in this dissertation,the autonomous driving and the telecontrol driving process are modeled and verified.The autonomous driving process model is mainly composed of data acquisition equipment models,actuator models,locomotive controller and train operating server model.Because of the complexity of locomotive controller’s function,it is divided into three parts: data acquisition,control decision making and control execution.After modeling process,the model is checked with Uppaal verifier,and the verification results prove the correctness of the system design.The modeling of the telecontrol driving process is divided into two parts: binding process and control process,in this dissertation the control process model are mainly analyzed.The telecontrol driving model involves the driver,locomotive controller,telecontrol operation platform as well as train operating server.And in modeling process,the equipment failure,network packet loss and delay factors are taken into account.Finally,correctness of the design for telecontrol driving process is verified.in telecontrol driving process model.