随着无线通信技术、定位技术、人工智能技术等不断发展，世界经济加速向网络信息技术产业转变，车联网的地位显得越来越重要。美国、日本、欧洲等国都提出了自己的智能交通系统（ITS）战略计划，本课题针对车联网多源异构环境下海量终端设备节点拓扑结构的多变性、需求融合的复杂性、数据传输的实时性等特点，采用形式化方法研究车联网多源异构环境下信息协同容错传输机制的正确性和可靠性。主要包括：（1）车联网多源异构信息协同容错传输的规约语言机制：借鉴超协调逻辑思想扩展Z语言，结合动态建模语言Time Petri net，建立协同容错规约语言TPZN；（2）基于TPZN建立车联网多源异构信息协同容错传输机制的形式化模型；（3）针对形式化模型进行分析验证。本项目的实施将为车联网信息协同容错传输机制建立一套新的模型设计和分析方法，为我国车联网的安全发展提供新的理论保障。

With the development of wireless communication technology, location technology, artificial intelligence technology, and so on, the world economy depends on network and information technology more and more heavily. In particular, the Internet of Vehicles turns to be more and more important. The United States, Japan, Europe and many other countries have put forward their own Intelligent Transportation Systems (ITS) plan. Aiming at characterizing features of the internet of vehicles, including the multi-source heterogeneous environment, the variability of the node topology, the complexity of requirement, and the real-time of data transmission, etc, this project study on how to use formal methods to verify the correctness and reliability of the collaborative fault-tolerant transmission mechanism under the multi-source heterogeneous environment of the Internet of Vehicles. Concretely, it includes: (1) the specific language of collaborative fault-tolerant transmission of the Internet of Vehicles: extending the Z language based on the paraconsistent logic, combing it with dynamic modeling language Time Petri net, and establishing the cooperative fault-tolerant language TPZN; (2) modeling the collaborative fault-tolerant transmission mechanism of the multi-source heterogeneous information based on TPZN; (3) analyzing and verifying the formalized model. This project will hopefully lead to a new way for modeling and analyzing the collaborative fault-tolerant transmission mechanism of the information in the Internet of Vehicle, and supply a new theoretical guarantee for the safety of the Internet of Vehicle.