目錄
“零信任：群體智能可信決策與安全控制叢書(shū)”序
前言
第1章 緒論 1
1.1 引言 1
1.2 車(chē)聯(lián)網(wǎng)信息系統(tǒng)建模研究現(xiàn)狀 3
1.3 零信任環(huán)境下車(chē)聯(lián)網(wǎng)信息系統(tǒng)建模的需求分析 5
1.4 形式化方法應(yīng)用前景 7
1.5 本章小結(jié) 9
參考文獻(xiàn) 10
第2章 前期預(yù)備知識(shí)介紹 15
2.1 基于零信任架構(gòu)的車(chē)聯(lián)網(wǎng)系統(tǒng)機(jī)制分析 15
2.2 基于Petri 網(wǎng)的零信任車(chē)聯(lián)網(wǎng)系統(tǒng)建模 17
2.3 零信任車(chē)聯(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 零信任車(chē)聯(lián)網(wǎng)系統(tǒng)建模的Z 語(yǔ)言表征 26
2.5 零信任車(chē)聯(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)境下車(chē)聯(lián)網(wǎng)系統(tǒng)需求模型的形式化建模 44
3.1 基于零信任的車(chē)聯(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)境下車(chē)聯(lián)網(wǎng)系統(tǒng)需求過(guò)程模型的形式化建模與分析 79
3.2.1 過(guò)程層的形式化建模 79
3.2.2 形式化分析與驗(yàn)證 85
3.2.3 動(dòng)態(tài)環(huán)境下過(guò)程層模型的演化 89
3.2.4 性能比較分析 94
3.2.5 項(xiàng)目應(yīng)用的實(shí)例分析 95
3.3 零信任環(huán)境下車(chē)聯(lián)網(wǎng)系統(tǒng)需求目標(biāo)與過(guò)程模型的一致性驗(yàn)證 98
3.3.1 目標(biāo)與過(guò)程的映射關(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章 面向零信任車(chē)聯(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)境下車(chē)聯(lián)網(wǎng)系統(tǒng)中特殊車(chē)輛的優(yōu)先級(jí)處理方法 124
4.3.1 基于零信任的車(chē)聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型的形式化建模 124
4.3.2 零信任車(chē)聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型的形式化驗(yàn)證 129
4.3.3 零信任環(huán)境下車(chē)聯(lián)網(wǎng)系統(tǒng)信息傳輸機(jī)制模型仿真與結(jié)果分析 131
4.4 車(chē)聯(lián)網(wǎng)系統(tǒng)中緊急車(chē)輛讓行處理方法 136
4.4.1 緊急車(chē)輛讓行信息傳輸模型的形式化建模 136
4.4.2 零信任環(huán)境下緊急車(chē)輛讓行信息傳輸模型的形式化驗(yàn)證 144
4.4.3 零信任環(huán)境下緊急車(chē)輛讓行信息傳輸模型仿真與結(jié)果分析 150
4.5 本章小結(jié) 154
參考文獻(xiàn) 154
第5章 離散動(dòng)態(tài)環(huán)境下零信任車(chē)聯(lián)網(wǎng)系統(tǒng)性能的形式化優(yōu)化方法 158
5.1 基于SPZN的零信任智能網(wǎng)聯(lián)汽車(chē)的形式化建模 158
5.1.1 集成隨機(jī)Petri網(wǎng)與Z 語(yǔ)言的形式化方法 158
5.1.2 SPZN的形式化建模 162
5.1.3 SPZN的優(yōu)勢(shì) 164
5.2 基于SPZN的智能網(wǎng)聯(lián)汽車(chē)的精煉和抽象方法 165
5.2.1 隨機(jī)Petri網(wǎng)的可達(dá)標(biāo)識(shí)空間爆炸問(wèn)題 165
5.2.2 對(duì)單個(gè)庫(kù)所和變遷的精煉抽象方法 166
5.2.3 對(duì)多個(gè)庫(kù)所和變遷的精煉抽象方法 168
5.2.4 混合庫(kù)所和變遷的精煉抽象方法 169
5.3 基于SPZN的車(chē)聯(lián)網(wǎng)系統(tǒng)的形式化驗(yàn)證與分析 170
5.3.1 SPZN的動(dòng)態(tài)性質(zhì)分析 172
5.3.2 基于SPZN的零信任車(chē)路云系統(tǒng)的形式化建模 174
5.3.3 基于SPZN的零信任“車(chē)-路-云”系統(tǒng)的精煉與抽象 179
5.3.4 基于SPZN的零信任“車(chē)-路-云”系統(tǒng)的形式化驗(yàn)證與分析 186
5.4 本章小結(jié) 198
參考文獻(xiàn) 199
第6章 零信任車(chē)聯(lián)網(wǎng)信息系統(tǒng)形式化方法的研究趨勢(shì)分析 202
6.1 零信任車(chē)聯(lián)網(wǎng)數(shù)據(jù)傳輸?shù)男问交�建模與驗(yàn)證研究趨勢(shì) 202
6.2 形式化方法在零信任車(chē)聯(lián)網(wǎng)的應(yīng)用 204
6.3 形式化驗(yàn)證工具和研究成果 205
6.4 本章小結(jié) 208
參考文獻(xiàn) 208