目錄
“零信任：群體智能可信決策與安全控制叢書”序
前言
第1章 緒論 1
1.1 引言 1
1.2 車聯(lián)網(wǎng)信息系統(tǒng)建模研究現(xiàn)狀 3
1.3 零信任環(huán)境下車聯(lián)網(wǎng)信息系統(tǒng)建模的需求分析 5
1.4 形式化方法應(yīng)用前景 7
1.5 本章小結(jié) 9
參考文獻(xiàn) 10
第2章 前期預(yù)備知識介紹 15
2.1 基于零信任架構(gòu)的車聯(lián)網(wǎng)系統(tǒng)機(jī)制分析 15
2.2 基于Petri 網(wǎng)的零信任車聯(lián)網(wǎng)系統(tǒng)建模 17
2.3 零信任車聯(lián)網(wǎng)系統(tǒng)的擴(kuò)展Petri 網(wǎng) 22
2.3.1 時(shí)間Petri網(wǎng) 22
2.3.2 隨機(jī)Petri網(wǎng) 25
2.4 零信任車聯(lián)網(wǎng)系統(tǒng)建模的Z 語言表征 26
2.5 零信任車聯(lián)網(wǎng)系統(tǒng)形式化模型的PZN 表征 30
2.6 基于Actor-Critic 算法的強(qiáng)化學(xué)習(xí) 37
2.7 形式化建模工具介紹 39
2.8 本章小結(jié) 41
參考文獻(xiàn) 41
第3章 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求模型的形式化建模 44
3.1 基于零信任的車聯(lián)網(wǎng)系統(tǒng)需求目標(biāo)模型的形式化建模與分析 44
3.1.1 基于超協(xié)調(diào)邏輯思想的需求預(yù)處理 44
3.1.2 目標(biāo)層的形式化建模 58
3.1.3 目標(biāo)層的形式化分析與驗(yàn)證 63
3.1.4 零信任環(huán)境下目標(biāo)層模型的演化 70
3.1.5 性能比較分析 76
3.1.6 項(xiàng)目應(yīng)用的實(shí)例分析 77
3.2 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求過程模型的形式化建模與分析 79
3.2.1 過程層的形式化建模 79
3.2.2 形式化分析與驗(yàn)證 85
3.2.3 動態(tài)環(huán)境下過程層模型的演化 89
3.2.4 性能比較分析 94
3.2.5 項(xiàng)目應(yīng)用的實(shí)例分析 95
3.3 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求目標(biāo)與過程模型的一致性驗(yàn)證 98
3.3.1 目標(biāo)與過程的映射關(guān)系 98
3.3.2 一致性分析 99
3.3.3 一致性驗(yàn)證 104
3.3.4 項(xiàng)目應(yīng)用的實(shí)例分析 107
3.4 本章小結(jié) 109
參考文獻(xiàn) 110
第4章 面向零信任車聯(lián)網(wǎng)信息安全傳輸機(jī)制的形式化分析 114
4.1 基于TPZN的形式化建模 114
4.1.1 TPZN 114
4.1.2 TPZN的建模與精煉 116
4.1.3 TPZN建模工具介紹 118
4.2 基于TPZN的形式化驗(yàn)證 120
4.2.1 完整性分析 120
4.2.2 可達(dá)性分析 121
4.2.3 活性分析 123
4.3 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)中特殊車輛的優(yōu)先級處理方法 124
4.3.1 基于零信任的車聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型的形式化建模 124
4.3.2 零信任車聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型的形式化驗(yàn)證 129
4.3.3 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型仿真與結(jié)果分析 131
4.4 車聯(lián)網(wǎng)系統(tǒng)中緊急車輛讓行處理方法 136
4.4.1 緊急車輛讓行信息傳輸模型的形式化建模 136
4.4.2 零信任環(huán)境下緊急車輛讓行信息傳輸模型的形式化驗(yàn)證 144
4.4.3 零信任環(huán)境下緊急車輛讓行信息傳輸模型仿真與結(jié)果分析 150
4.5 本章小結(jié) 154
參考文獻(xiàn) 154
第5章 離散動態(tài)環(huán)境下零信任車聯(lián)網(wǎng)系統(tǒng)性能的形式化優(yōu)化方法 158
5.1 基于SPZN的零信任智能網(wǎng)聯(lián)汽車的形式化建模 158
5.1.1 集成隨機(jī)Petri網(wǎng)與Z 語言的形式化方法 158
5.1.2 SPZN的形式化建模 162
5.1.3 SPZN的優(yōu)勢 164
5.2 基于SPZN的智能網(wǎng)聯(lián)汽車的精煉和抽象方法 165
5.2.1 隨機(jī)Petri網(wǎng)的可達(dá)標(biāo)識空間爆炸問題 165
5.2.2 對單個(gè)庫所和變遷的精煉抽象方法 166
5.2.3 對多個(gè)庫所和變遷的精煉抽象方法 168
5.2.4 混合庫所和變遷的精煉抽象方法 169
5.3 基于SPZN的車聯(lián)網(wǎng)系統(tǒng)的形式化驗(yàn)證與分析 170
5.3.1 SPZN的動態(tài)性質(zhì)分析 172
5.3.2 基于SPZN的零信任車路云系統(tǒng)的形式化建模 174
5.3.3 基于SPZN的零信任“車-路-云”系統(tǒng)的精煉與抽象 179
5.3.4 基于SPZN的零信任“車-路-云”系統(tǒng)的形式化驗(yàn)證與分析 186
5.4 本章小結(jié) 198
參考文獻(xiàn) 199
第6章 零信任車聯(lián)網(wǎng)信息系統(tǒng)形式化方法的研究趨勢分析 202
6.1 零信任車聯(lián)網(wǎng)數(shù)據(jù)傳輸?shù)男问交�建模與驗(yàn)證研究趨勢 202
6.2 形式化方法在零信任車聯(lián)網(wǎng)的應(yīng)用 204
6.3 形式化驗(yàn)證工具和研究成果 205
6.4 本章小結(jié) 208
參考文獻(xiàn) 208