本书以零信任环境下车联网信息传输过程中的安全机制为主题，在近几年课题组的研究基础之上，针对车联网运行环境复杂、多变，以及传感器设备数量庞大等特征导致的人、设备、应用等不存在任何潜在信任的问题，基于“永不信任、持续验证”的实际需求进行了详细的问题分析，以零信任环境为具体特性，对车联网信息系统的需求模型、车联网数据信息的传输过程、离散环境下车联网系统的安全性传输机制进行形式化建模与分析，并进行模型抽象与重组。

更多科学出版社服务，请扫码获取。

2003.09-2006.07 重庆大学，控制理论与控制工程，博士 2000.09-2003.07 辽宁大学，应用数学，硕士 1996.09-2000.07 湖北民族学院，数学及应用数学，学士，本科2011.11－2018.12， 重庆交通大学信息科学与工程学院，教授（电子信息工程系主任） 2019.01-2021.12， 重庆交通大学信息科学与工程学院副院长，教授，博士生导师 2021.01-2022.10，重庆交通大学信息科学与工程学院，教授，博士生导师 2022.10-至 今，安徽大学人工智能学院，教授，博士生导师（自主无人系统技术教育部工程中心副主任）中国自动化学会数据驱动控制、学习与优化专业委员会副秘书长 中国自动化学会技术过程的故障诊断及安全性专业委员会委员 中国自动化学会过程控制专业委员会委员

目录
“零信任：群体智能可信决策与安全控制丛书”序
前言
第1章 绪论 1
1.1 引言 1
1.2 车联网信息系统建模研究现状 3
1.3 零信任环境下车联网信息系统建模的需求分析 5
1.4 形式化方法应用前景 7
1.5 本章小结 9
参考文献 10
第2章 前期预备知识介绍 15
2.1 基于零信任架构的车联网系统机制分析 15
2.2 基于Petri 网的零信任车联网系统建模 17
2.3 零信任车联网系统的扩展Petri 网 22
2.3.1 时间Petri网 22
2.3.2 随机Petri网 25
2.4 零信任车联网系统建模的Z 语言表征 26
2.5 零信任车联网系统形式化模型的PZN 表征 30
2.6 基于Actor-Critic 算法的强化学习 37
2.7 形式化建模工具介绍 39
2.8 本章小结 41
参考文献 41
第3章 零信任环境下车联网系统需求模型的形式化建模 44
3.1 基于零信任的车联网系统需求目标模型的形式化建模与分析 44
3.1.1 基于超协调逻辑思想的需求预处理 44
3.1.2 目标层的形式化建模 58
3.1.3 目标层的形式化分析与验证 63
3.1.4 零信任环境下目标层模型的演化 70
3.1.5 性能比较分析 76
3.1.6 项目应用的实例分析 77
3.2 零信任环境下车联网系统需求过程模型的形式化建模与分析 79
3.2.1 过程层的形式化建模 79
3.2.2 形式化分析与验证 85
3.2.3 动态环境下过程层模型的演化 89
3.2.4 性能比较分析 94
3.2.5 项目应用的实例分析 95
3.3 零信任环境下车联网系统需求目标与过程模型的一致性验证 98
3.3.1 目标与过程的映射关系 98
3.3.2 一致性分析 99
3.3.3 一致性验证 104
3.3.4 项目应用的实例分析 107
3.4 本章小结 109
参考文献 110
第4章 面向零信任车联网信息安全传输机制的形式化分析 114
4.1 基于TPZN的形式化建模 114
4.1.1 TPZN 114
4.1.2 TPZN的建模与精炼 116
4.1.3 TPZN建模工具介绍 118
4.2 基于TPZN的形式化验证 120
4.2.1 完整性分析 120
4.2.2 可达性分析 121
4.2.3 活性分析 123
4.3 零信任环境下车联网系统中特殊车辆的优先级处理方法 124
4.3.1 基于零信任的车联网系统信息传输机制模型的形式化建模 124
4.3.2 零信任车联网系统信息传输机制模型的形式化验证 129
4.3.3 零信任环境下车联网系统信息传输机制模型仿真与结果分析 131
4.4 车联网系统中紧急车辆让行处理方法 136
4.4.1 紧急车辆让行信息传输模型的形式化建模 136
4.4.2 零信任环境下紧急车辆让行信息传输模型的形式化验证 144
4.4.3 零信任环境下紧急车辆让行信息传输模型仿真与结果分析 150
4.5 本章小结 154
参考文献 154
第5章 离散动态环境下零信任车联网系统性能的形式化优化方法 158
5.1 基于SPZN的零信任智能网联汽车的形式化建模 158
5.1.1 集成随机Petri网与Z 语言的形式化方法 158
5.1.2 SPZN的形式化建模 162
5.1.3 SPZN的优势 164
5.2 基于SPZN的智能网联汽车的精炼和抽象方法 165
5.2.1 随机Petri网的可达标识空间爆炸问题 165
5.2.2 对单个库所和变迁的精炼抽象方法 166
5.2.3 对多个库所和变迁的精炼抽象方法 168
5.2.4 混合库所和变迁的精炼抽象方法 169
5.3 基于SPZN的车联网系统的形式化验证与分析 170
5.3.1 SPZN的动态性质分析 172
5.3.2 基于SPZN的零信任车路云系统的形式化建模 174
5.3.3 基于SPZN的零信任“车-路-云”系统的精炼与抽象 179
5.3.4 基于SPZN的零信任“车-路-云”系统的形式化验证与分析 186
5.4 本章小结 198
参考文献 199
第6章 零信任车联网信息系统形式化方法的研究趋势分析 202
6.1 零信任车联网数据传输的形式化建模与验证研究趋势 202
6.2 形式化方法在零信任车联网的应用 204
6.3 形式化验证工具和研究成果 205
6.4 本章小结 208
参考文献 208