Modeling And Formal Verifying Automated Guided Vehicle

Thanks to the efficiency, accuracy and flexibility of automated guided vehicle, automated guided vehicles are widely used in manufacturing facilities, warehouses, distribution centers, transshipment terminals and so on. Automated guided vehicle requires high reliability, formal methods are the major techniques to ensure high reliability of a system, and formal modeling is the key step for formal methods, so this paper will research the formal modeling methods to model the automated guided vehicle, and prove the correctness of properties of automated guided vehicle by formal analysis. The related work is completed as follows:Firstly, this paper introduces formal methods briefly, including logics and formal verification. This paper mainly introduces propositional logic, first-order logic, temporal logic and higher-order logic. The introductions on formal verification including the basic principles and characteristics of equivalence checking, model checking and theorem proving.Then the paper deeply study hybrid system and modling a hybrid system. Two ways construct a hybrid system as follows:one is to add continuous phenomenons in the discrete model, and then combine with the control system. The other is to add discrete phenomentons in the continuous model, and then combine with control system.What is more, the automated guided vehicle is modeled using hybrid input and output automata. In order to simplify the proof of the properties of automated guided vehicle, an abstract model is builded from the hybrid input and output model of automated guided vehicle. In order to ensure the validity of the abstract model, this paper proves the existence of bisimulation relationship between original model and abstract models.Finally, some key properties are characterized for the correctness of the automated guided vehicle system. This paper designed some constraints to ensure the correctness of the desired properties. This paper also proved the validity of these constraints. This paper determine the extent of the interferences are allowed by analyzing the parameters of constraints of automated guided vehicle system.