零信任環(huán)境下車聯(lián)網(wǎng)信息安全傳輸?shù)男问交Ｅc分析方法

目錄
“零信任：群體智能可信決策與安全控制叢書”序
前言
第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
參考文獻 10
第2章 前期預備知識介紹 15
2.1 基于零信任架構(gòu)的車聯(lián)網(wǎng)系統(tǒng)機制分析 15
2.2 基于Petri 網(wǎng)的零信任車聯(lián)網(wǎng)系統(tǒng)建模 17
2.3 零信任車聯(lián)網(wǎng)系統(tǒng)的擴展Petri 網(wǎng) 22
2.3.1 時間Petri網(wǎng) 22
2.3.2 隨機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 算法的強化學習 37
2.7 形式化建模工具介紹 39
2.8 本章小結(jié) 41
參考文獻 41
第3章 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求模型的形式化建模 44
3.1 基于零信任的車聯(lián)網(wǎng)系統(tǒng)需求目標模型的形式化建模與分析 44
3.1.1 基于超協(xié)調(diào)邏輯思想的需求預處理 44
3.1.2 目標層的形式化建模 58
3.1.3 目標層的形式化分析與驗證 63
3.1.4 零信任環(huán)境下目標層模型的演化 70
3.1.5 性能比較分析 76
3.1.6 項目應(yīng)用的實例分析 77
3.2 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求過程模型的形式化建模與分析 79
3.2.1 過程層的形式化建模 79
3.2.2 形式化分析與驗證 85
3.2.3 動態(tài)環(huán)境下過程層模型的演化 89
3.2.4 性能比較分析 94
3.2.5 項目應(yīng)用的實例分析 95
3.3 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)需求目標與過程模型的一致性驗證 98
3.3.1 目標與過程的映射關(guān)系 98
3.3.2 一致性分析 99
3.3.3 一致性驗證 104
3.3.4 項目應(yīng)用的實例分析 107
3.4 本章小結(jié) 109
參考文獻 110
第4章 面向零信任車聯(lián)網(wǎng)信息安全傳輸機制的形式化分析 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 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)中特殊車輛的優(yōu)先級處理方法 124
4.3.1 基于零信任的車聯(lián)網(wǎng)系統(tǒng)信息傳輸機制模型的形式化建模 124
4.3.2 零信任車聯(lián)網(wǎng)系統(tǒng)信息傳輸機制模型的形式化驗證 129
4.3.3 零信任環(huán)境下車聯(lián)網(wǎng)系統(tǒng)信息傳輸機制模型仿真與結(jié)果分析 131
4.4 車聯(lián)網(wǎng)系統(tǒng)中緊急車輛讓行處理方法 136
4.4.1 緊急車輛讓行信息傳輸模型的形式化建模 136
4.4.2 零信任環(huán)境下緊急車輛讓行信息傳輸模型的形式化驗證 144
4.4.3 零信任環(huán)境下緊急車輛讓行信息傳輸模型仿真與結(jié)果分析 150
4.5 本章小結(jié) 154
參考文獻 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 集成隨機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 隨機Petri網(wǎng)的可達標識空間爆炸問題 165
5.2.2 對單個庫所和變遷的精煉抽象方法 166
5.2.3 對多個庫所和變遷的精煉抽象方法 168
5.2.4 混合庫所和變遷的精煉抽象方法 169
5.3 基于SPZN的車聯(lián)網(wǎng)系統(tǒng)的形式化驗證與分析 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)的形式化驗證與分析 186
5.4 本章小結(jié) 198
參考文獻 199
第6章 零信任車聯(lián)網(wǎng)信息系統(tǒng)形式化方法的研究趨勢分析 202
6.1 零信任車聯(lián)網(wǎng)數(shù)據(jù)傳輸?shù)男问交Ｅc驗證研究趨勢 202
6.2 形式化方法在零信任車聯(lián)網(wǎng)的應(yīng)用 204
6.3 形式化驗證工具和研究成果 205
6.4 本章小結(jié) 208
參考文獻 208