车联网多源异构信息协同容错传输机制的形式化验证方法

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.

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

本项目在时间Petri网和随机Petri网理论基础上，结合框架描述语言-Z的特点，开展了动态Petri网融合规约语言的相关研究，提出了TPZN（时间Petri网融合Z语言）和SPZN（随机Petri网融合Z语言）的概念，进一步完善和提炼了动态Petri网理论，研究了复杂动态环境下车联网环境中数据传输的形式化建模和分析方法。为了解决车联网系统中节点模式异构性强、运行环境复杂多变、随机事件发生的多样性等问题，引入超协调逻辑规则扩展Z语言中二值问题，并融合时间Petri网和随机Petri网描述车联网汽车系统中设备信息的时间约束条件、动态演化规则、随机事件发生概率等，进一步分析车联网系统数据信息的可达性、正确性和完整性。具体研究内容包括：（1）采用TPZN-TPN描述车联网汽车系统中设备信息的时间约束条件和动态演化规则，采用TPZN-Z刻画车联网汽车系统中设备节点的状态信息、功能性信息和非功能性信息，在此基础上对车联网汽车系统进行形式化建模，以更精准的描述运行环境中的实时性问题，并对模型的可达性、正确性和完整性进行形式化分析验证；（2）采用SPZN-SPN描述车联网运行环境中的随机事件发生状态变化，采用SPZN-Z刻画车联网系统中设备节点的状态信息、功能性信息和非功能性信息，在此基础上对车联网运行环境中随机事件进行形式化建模和分析，将Petri Net对应的可达标识图转化为同构的马尔科夫链，模拟预测分析车辆后续行为，通过模型的抽象避免了Petri网中的状态爆炸问题，采用强化学习中的Actor-Critic算法对SPZN模型参数进行优化，以提高系统的稳定性和安全性。本项目的研究成果不仅丰富了动态形式化建模语言的理论基础，同时为车联网工程的故障诊断和行为预测建模和分析领域提供了一定的理论支撑，带来了新的思维方式。