Event-B建模 系統(tǒng)和軟件工程

第 1章　引言 1
1．1　動機(jī) 1
1．2　各章概覽 2
1．3　如何用這本書 6
1．4　形式化方法 8
1．5　一個小迂回：藍(lán)圖 9
1．6　需求文檔 10
1．6．1　生命周期 10
1．6．2　需求文檔的困難 10
1．6．3　一種有用的比較 11
1．7　本書中使用的“形式化方法”的定義 12
1．7．1　復(fù)雜系統(tǒng) 12
1．7．2　離散系統(tǒng) 13
1．7．3　測試推理與模型（藍(lán)圖）推理 13
1．8　有關(guān)離散模型的非形式化概覽 14
1．8．1　狀態(tài)和遷移 14
1．8．2　操作性解釋 14
1．8．3　形式化推理 15
1．8．4　管理閉模型的復(fù)雜性 15
1．8．5　精化 15
1．8．6　分解 16
1．8．7　泛型開發(fā) 16
1．9 參考資料 17
第 2章　控制橋上的汽車 18
2．1　引言 18
2．2　需求文檔 18
2．3　精化策略 20
2．4　初始模型：限制汽車的數(shù)量 20
2．4．1　引言 20
2．4．2　狀態(tài)的形式化 21
2．4．3　事件的形式化 22
2．4．4　前-后謂詞 23
2．4．5　證明不變式的保持性質(zhì) 23
2．4．6　相繼式 25
2．4．7　應(yīng)用不變式保持性的規(guī)則 25
2．4．8　證明義務(wù)的證明 26
2．4．9　推理規(guī)則 27
2．4．10　元變量 29
2．4．11　證明 29
2．4．12　更多推理規(guī)則 30
2．4．13　改造兩個事件：引進(jìn)衛(wèi) 31
2．4．14　改造的不變式保持規(guī)則 31
2．4．15　重新證明不變式的保持性 32
2．4．16　初始化 33
2．4．17　初始化事件init的不變式建立規(guī)則 33
2．4．18　應(yīng)用不變式建立規(guī)則 34
2．4．19　證明初始化的證明義務(wù)：更多推理規(guī)則 34
2．4．20　無死鎖 35
2．4．21　無死鎖規(guī)則 35
2．4．22　應(yīng)用無死鎖證明義務(wù)規(guī)則 35
2．4．23　更多推理規(guī)則 36
2．4．24　證明無死鎖的證明義務(wù) 37
2．4．25　對初始模型的總結(jié) 38
2．5　第 一次精化：引入單行橋 38
2．5．1　引言 38
2．5．2　狀態(tài)的精化 39
2．5．3　精化抽象事件 40
2．5．4　重溫前-后謂詞 40
2．5．5　精化的非形式化證明 41
2．5．6　證明抽象事件的正確精化 42
2．5．7　應(yīng)用精化規(guī)則 43
2．5．8　精化初始化事件init 45
2．5．9　初始化事件init精化正確性的證明義務(wù)規(guī)則 46
2．5．10　應(yīng)用初始化精化的證明義務(wù)規(guī)則 46
2．5．11　引入新事件 46
2．5．12　空動作skip 47
2．5．13　證明兩個新事件的正確性 47
2．5．14　證明新事件的收斂性 49
2．5．15　應(yīng)用非收斂證明義務(wù)規(guī)則 50
2．5．16　相對無死鎖 51
2．5．17　應(yīng)用相對無死鎖證明義務(wù)規(guī)則 51
2．5．18　更多推理規(guī)則 52
2．5．19　第 一個精化的總結(jié) 54
2．6　第二次精化：引入交通燈 55
2．6．1　精化狀態(tài) 55
2．6．2　精化抽象事件 56
2．6．3　引進(jìn)新事件 56
2．6．4　疊加：調(diào)整精化規(guī)則 57
2．6．5　證明事件的正確性 58
2．6．6　更多邏輯推理規(guī)則 58
2．6．7　試探性的證明和解 58
2．6．8　新事件的收斂性 64
2．6．9　相對無死鎖 67
2．6．10　第二個精化的總結(jié) 68
2．7　第三次精化：引入車輛傳感器 70
2．7．1　引言 70
2．7．2　精化狀態(tài) 72
2．7．3　精化控制器里的抽象事件 75
2．7．4　在環(huán)境里增加新事件 77
2．7．5　新事件的收斂性 78
2．7．6　無死鎖 78
第3章　沖壓機(jī)控制器 79
3．1　非形式描述 79
3．1．1　基本設(shè)備 79
3．1．2　基本命令和按鈕 80
3．1．3　基本用戶動作 80
3．1．4　用戶工作期 80
3．1．5　危險：控制器的必要性 80
3．1．6　安全門 81
3．2　設(shè)計模式 81
3．2．1　動作和反應(yīng) 82
3．2．2　第 一種情況：一個簡單的動作反應(yīng)模式，無反作用 83
3．2．3　第二種情況：一個簡單的動作模式，一次重復(fù)動作和反應(yīng) 86
3．3　沖壓機(jī)的需求 90
3．4　精化策略 91
3．5　初始模型：連接控制器和電動機(jī) 92
3．5．1　引言 92
3．5．2　建模 92
3．5．3　事件的總結(jié) 94
3．6　第 一次精化：把電動機(jī)按鈕連接到控制器 94
3．6．1　引言 94
3．6．2　建模 95
3．6．3　加入“假”事件 99
3．6．4　事件的總結(jié) 100
3．7　第二次精化：連接控制器到離合器 100
3．8　另一個設(shè)計模式：兩個強(qiáng)反應(yīng)的弱同步 101
3．8．1　引言 101
3．8．2　建模 103
3．9　第三次精化：約束離合器和電動機(jī) 108
3．10　第四次精化：連接控制器到安全門 110
3．10．1　拷貝 110
3．10．2　事件的總結(jié) 110
3．11　第五次精化：約束離合器和安全門 110
3．12　另一設(shè)計模式：兩個強(qiáng)反應(yīng)的強(qiáng)同步 111
3．12．1　引言 111
3．12．2　建模 112
3．13　第六次精化：離合器和安全門之間的更多約束 117
3．14　第七次精化：把控制器連接到離合器按鈕 118
3．14．1　拷貝 118
3．14．2　事件的總結(jié) 118
第4章　簡單文件傳輸協(xié)議 120
4．1　需求 120
4．2　精化策略 120
4．3　協(xié)議的初始模型 121
4．3．1　狀態(tài) 122
4．3．2　一些數(shù)學(xué)表示法 122
4．3．3　事件 125
4．3．4　證明 125
4．4　協(xié)議的第 一次精化 127
4．4．1　非形式化的說明 127
4．4．2　狀態(tài) 128
4．4．3　更多數(shù)學(xué)符號 128
4．4．4　事件 130
4．4．5　精化證明 131
4．4．6　事件receive的收斂性證明 134
4．4．7　相對無死鎖證明 135
4．5　協(xié)議的第二次精化 135
4．5．1　狀態(tài)和事件 135
4．5．2　證明 137
4．6　協(xié)議的第三次精化 137
4．6．1　狀態(tài) 137
4．6．2　事件 138
4．6．3　全稱量化謂詞的推理規(guī)則 138
4．7　對開發(fā)的回顧 139
4．7．1　動機(jī)和預(yù)期事件的引入 139
4．7．2　初始模型 140
4．7．3　第 一次精化 140
4．7．4　第二次精化 141
4．7．5　第三次精化 141
4．8　參考資料 142
第5章　Event-B建模語言和證明義務(wù)規(guī)則 143
5．1　Event-B表示法 143
5．1．1　引言：機(jī)器和上下文 143
5．1．2　機(jī)器和上下文的關(guān)系 143
5．1．3　上下文的結(jié)構(gòu) 144
5．1．4　上下文的例子 145
5．1．5　機(jī)器的結(jié)構(gòu) 145
5．1．6　機(jī)器的例子 146
5．1．7　事件 147
5．1．8　動作 147
5．1．9　事件的例子 149
5．2　證明義務(wù)規(guī)則 150
5．2．1　引言 150
5．2．2　不變式保持證明義務(wù)規(guī)則：INV 151
5．2．3　可行性證明義務(wù)規(guī)則：FIS 153
5．2．4　衛(wèi)加強(qiáng)證明義務(wù)規(guī)則：GRD 153
5．2．5　衛(wèi)歸并證明義務(wù)規(guī)則：MRG 154
5．2．6　模擬證明義務(wù)規(guī)則：SIM 155
5．2．7　數(shù)值變動式證明義務(wù)規(guī)則：NAT 158
5．2．8　有窮集變動式證明義務(wù)規(guī)則：FIN 158
5．2．9　變動量證明義務(wù)規(guī)則：VAR 159
5．2．10　非確定性見證證明義務(wù)規(guī)則：WFIS 161
5．2．11　定理證明義務(wù)規(guī)則：THM 162
5．2．12　良好定義證明義務(wù)規(guī)則：WD 162
第6章　有界重傳協(xié)議 163
6．1　有界重傳協(xié)議的非形式說明 163
6．1．1　正常行為 163
6．1．2　不可靠的通信 163
6．1．3　協(xié)議流產(chǎn) 164
6．1．4　交替位 164
6．1．5　協(xié)議的最后情況 164
6．1．6　BRP的偽代碼描述 165
6．1．7　有關(guān)偽代碼的說明 167
6．2　需求文檔 167
6．3　精化策略 168
6．4　初始模型 169
6．4．1　狀態(tài) 169
6．4．2　事件 169
6．5　第 一次和第二次精化 170
6．5．1　狀態(tài) 170
6．5．2　第 一次精化的事件 170
6．5．3　第二次精化的事件 171
6．6　第三次精化 171
6．6．1　狀態(tài) 172
6．6．2　事件 172
6．6．3　事件之間的同步 173
6．7　第四次精化 173
6．7．1　狀態(tài) 173
6．7．2　事件 174
6．7．3　事件的同步 175
6．8　第五次精化 176
6．8．1　狀態(tài) 176
6．8．2　事件 177
6．8．3　事件的同步 180
6．9　第六次精化 181
6．10　參考資料 181
第7章　一個并發(fā)程序的開發(fā)1 182
7．1　分布式和并發(fā)程序的比較 182
7．1．1　分布式程序 182
7．1．2　并發(fā)程序 182
7．2　提出的實(shí)例 183
7．2．1　非形式的說明 183
7．2．2　非并發(fā)的場景展示 185
7．2．3　定義原子性 186
7．3　交錯 187
7．3．1　問題 187
7．3．2　計算不同交錯的數(shù)目 188
7．3．3　結(jié)果 189
7．4　并發(fā)程序的規(guī)范描述 190
7．4．1　寫和讀的軌跡 190
7．4．2　軌跡之間的關(guān)系 190
7．4．3　不變式的總結(jié) 193
7．4．4　事件 193
7．5　精化策略 194
7．5．1　最終精化的梗概 194
7．5．2　精化的目標(biāo) 196
7．6　第 一次精化 196
7．6．1　讀者狀態(tài) 196
7．6．2　讀事件 197
7．6．3　寫者狀態(tài) 198
7．6．4　寫事件 198
7．7　第二次精化 200
7．7．1　狀態(tài) 200
7．7．2　事件和新增的不變式 200
7．8　第三次精化 203
7．8．1　狀態(tài) 203
7．8．2　事件 203
7．9　第四次精化 204
7．9．1　狀態(tài) 204
7．9．2　事件 205
7．10　參考資料 206
第8章　電路的開發(fā) 207
8．1　引言 207
8．1．1　同步電路 207
8．1．2　電路與其環(huán)境的耦合 208
8．1．3　耦合的動態(tài)觀點(diǎn) 208
8．1．4　耦合的靜態(tài)觀點(diǎn) 209
8．1．5　協(xié)調(diào)性條件 209
8．1．6　一個警告 210
8．1．7　電路的最終構(gòu)造 210
8．1．8　一個非常小的示例 213
8．2　第 一個例子 214
8．2．1　非形式的規(guī)范描述 214
8．2．2　初始模型 215
8．2．3　精化電路以減少其非確定性 218
8．2．4　通過改變數(shù)據(jù)空間來精化電路 220
8．2．5　構(gòu)造最后的電路 222
8．3　第二個例子：仲裁器 225
8．3．1　非形式的規(guī)范描述 225
8．3．2　初始模型 226
8．3．3　第 一次精化：讓電路生成二進(jìn)制輸出 229
8．3．4　第二次精化 231
8．3．5　第三次精化：消除電路的非確定性 233
8．3．6　第四次精化：構(gòu)造最后的電路 234
8．4　第三個例子：一種特殊的道路交通燈 234
8．4．1　非形式的規(guī)范描述 235
8．4．2　關(guān)注點(diǎn)分離的方法 235
8．4．3　優(yōu)先權(quán)電路：初始模型 236
8．4．4　最后的Priority電路 238
8．5　Light電路 240
8．5．1　一個抽象：Upper電路 241
8．5．2　精化：加入Lower電路 242
8．6　參考資料 245
第9章　數(shù)學(xué)語言 246
9．1　相繼式演算 246
9．1．1　定義 246
9．1．2　一個數(shù)學(xué)語言的相繼式 248
9．1．3　初始理論 248
9．2　命題語言 249
9．2．1　語法 249
9．2．2　初始理論的擴(kuò)充 250
9．2．3　派生規(guī)則 250
9．2．4　方法論 252
9．2．5　命題語言的擴(kuò)充 252
9．3　謂詞語言 253
9．3．1　語法 253
9．3．2　謂詞和表達(dá)式 254
9．3．3　全稱量詞的推理規(guī)則 254
9．4　相等謂詞 256
9．5　集合論語言 257
9．5．1　語法 258
9．5．2　集合論公理 258
9．5．3　基本集合運(yùn)算符 259
9．5．4　基本集合運(yùn)算符的推廣 260
9．5．5　二元關(guān)系運(yùn)算符 261
9．5．6　函數(shù)運(yùn)算符 264
9．5．7　各種箭頭的總結(jié) 265
9．5．8　lambda抽象和函數(shù)調(diào)用 265
9．6　布爾和算術(shù)語言 266
9．6．1　語法 266
9．6．2　皮阿諾公理和遞歸定義 267
9．6．3　算術(shù)語言的擴(kuò)充 267
9．7　高級數(shù)據(jù)結(jié)構(gòu) 269
9．7．1　反自反的傳遞閉包 269
9．7．2　強(qiáng)連通圖 270
9．7．3　無窮表 271
9．7．4　有窮表 274
9．7．5　環(huán) 276
9．7．6　無窮樹 277
9．7．7　有窮深度樹 280
9．7．8　自由樹 281
9．7．9　良定義條件和有向無環(huán)圖 283
第 10章　環(huán)形網(wǎng)絡(luò)上選領(lǐng)導(dǎo) 284
10．1　需求文檔 284
10．2　初始模型 286
10．3　討論 286
10．3．1　第 一個嘗試 286
10．3．2　第二個嘗試 287
10．3．3　第三個嘗試 287
10．3．4　解的非形式化展示 287
10．4　第 一次精化 288
10．4．1　狀態(tài)：環(huán)的形式化 288
10．4．2　狀態(tài)：變量 289
10．4．3　事件 289
10．5　證明 289
10．5．1　事件elect的證明 290
10．5．2　事件accept的證明 291
10．5．3　事件reject的證明 293
10．5．4　新事件不發(fā)散的證明 293
10．5．5　無死鎖的證明 293
10．6　參考資料 294
第 11章　樹形網(wǎng)絡(luò)上的同步 295
11．1　引言 295
11．2　初始模型 296
11．2．1　狀態(tài) 296
11．2．2　事件 297
11．2．3　證明 297
11．3　第 一次精化 298
11．3．1　狀態(tài) 298
11．3．2　事件 300
11．3．3　證明 300
11．4　第二次精化 301
11．5　第三次精化 303
11．5．1　事件ascending的精化 303
11．5．2　事件descending的精化 304
11．5．3　證明定理thm3_4 306
11．5．4　證明不變式inv3_3的保持性 306
11．6　第四次精化 308
11．7　參考資料 310
第 12章　移動代理的路由算法 311
12．1　問題的非形式化描述 311
12．1．1　抽象的非形式化描述 311
12．1．2　第 一個非形式化的精化 312
12．1．3　第二個非形式化的精化 312
12．1．4　第三個非形式化的精化：解 314
12．2　初始模型 315
12．2．1　狀態(tài) 315
12．2．2　事件 316
12．2．3　證明 317
12．3　第 一次精化 318
12．3．1　狀態(tài) 318
12．3．2　事件 319
12．3．3　證明 320
12．4　第二次精化 320
12．4．1　狀態(tài) 320
12．4．2　事件 322
12．4．3　證明 323
12．5　第三次精化：數(shù)據(jù)精化 324
12．5．1　狀態(tài) 324
12．5．2　事件 324
12．5．3　證明 325
12．6　第四次精化 325
12．7　參考資料 325
第 13章　在連通圖網(wǎng)絡(luò)上選領(lǐng)導(dǎo) 326
13．1　初始模型 326
13．1．1　狀態(tài) 326
13．1．2　事件 327
13．2　第 一次精化 327
13．2．1　定義自由樹 327
13．2．2　擴(kuò)充狀態(tài) 327
13．2．3　事件的第 一次精化 328
13．2．4　第 一次精化的證明 329
13．3　第二次精化 329
13．3．1　第二次精化的狀態(tài) 329
13．3．2　事件 329
13．3．3　證明 330
13．4　第三次精化：競爭問題 330
13．4．1　引言 330
13．4．2　處理競爭的狀態(tài) 331
13．4．3　處理競爭的事件 332
13．5　第四次精化：簡化 332
13．6　第五次精化：引入基數(shù) 333
第 14章　證明義務(wù)的數(shù)學(xué)模型 335
14．1　引言 335
14．2　不變式保持性的證明義務(wù)規(guī)則 335
14．3　觀察離散遷移系統(tǒng)的演化：跡 337
14．3．1　第 一個例子 338
14．3．2　跡 338
14．3．3　跡的特征 339
14．3．4　演化圖 339
14．3．5　數(shù)學(xué)表示 339
14．4　用跡表示簡單精化 340
14．4．1　第二個例子 340
14．4．2　比較這兩個例子 341
14．4．3　簡單精化：非形式化的方法 342
14．4．4　簡單精化：形式化定義 342
14．4．5　考慮個別的事件 343
14．4．6　外部變量和內(nèi)部變量 344
14．4．7　外部集合 345
14．5　廣義精化的集合論表示 345
14．5．1　引言 346
14．5．2　精化的形式化定義 347
14．5．3　精化的充分條件：前向模擬 347
14．5．4　精化的另一充分條件：反向模擬 352
14．5．5　跡的精化 352
14．6　打破抽象和具體事件之間的一對一關(guān)系 353
14．6．1　分裂抽象事件 353
14．6．2　合并幾個抽象事件 353
14．6．3　引進(jìn)新事件 354
第 15章　順序程序的開發(fā) 357
15．1　開發(fā)順序程序的一種系統(tǒng)化方法 357
15．1．1　順序程序的組成部分 357
15．1．2　把順序程序分解為獨(dú)立的事件 358
15．1．3　方法梗概 359
15．1．4　順序程序的規(guī)范：前條件和后條件 359
15．2　一個非常簡單的例子 360
15．2．1　規(guī)范 360
15．2．2　精化 361
15．2．3　推廣 362
15．3　合并規(guī)則 362
15．4　例：排序數(shù)組里的二分檢索 363
15．4．1　初始模型 363
15．4．2　第 一次精化 364
15．4．3　第二次精化 365
15．4．4　合并 366
15．5　例：自然數(shù)數(shù)組中的最小值 366
15．5．1　初始模型 366
15．5．2　第 一次精化 367
15．6　例：數(shù)組劃分 367
15．6．1　初始模型 367
15．6．2　第 一次精化 368
15．6．3　合并 370
15．7　例：簡單排序 370
15．7．1　初始模型 370
15．7．2　第 一次精化 371
15．7．3　第二次精化 371
15．7．4　合并 373
15．8　例：數(shù)組反轉(zhuǎn) 373
15．8．1　初始模型 373
15．8．2　第 一次精化 374
15．9　例：鏈接表反轉(zhuǎn) 375
15．9．1　初始模型 375
15．9．2　第 一次精化 376
15．9．3　第二次精化 377
15．9．4　第三次精化 378
15．9．5　合并 378
15．10　例：計算平方根的簡單數(shù)值程序 378
15．10．1　初始模型 379
15．10．2　第 一次精化 379
15．10．3　第二次精化 379
15．11　例：內(nèi)射數(shù)值函數(shù)的逆 380
15．11．1　初始模型 380
15．11．2　第 一次精化 381
15．11．3　第二次精化 382
15．11．4　實(shí)例化 383
15．11．5　第 一次實(shí)例化 383
15．11．6　第二次實(shí)例化 384
第 16章　位置訪問控制器 385
16．1　需求文檔 385
16．2　討論 387
16．2．1　控制的共享 387
16．2．2　閉模型的構(gòu)造 387
16．2．3　設(shè)備的行為 388
16．2．4　處理安全問題 388
16．2．5　同步問題 388
16．2．6　邊界的功能 388
16．3　系統(tǒng)的初始模型 389
16．4　第 一次精化 390
16．4．1　狀態(tài)和事件 390
16．4．2　無死鎖 391
16．4．3　第 一個解 392
16．4．4　第二個解 393
16．4．5　無死鎖的修正 393
16．5　第二次精化 394
16．5．1　狀態(tài)和事件 394
16．5．2　同步 396
16．5．3　證明 396
16．5．4　讀卡器持續(xù)阻塞的危險 396
16．5．5　避免持續(xù)阻塞的提議 396
16．5．6　最后的決定 397
16．6　第三次精化 397
16．6．1　引進(jìn)讀卡器 397
16．6．2　與通信網(wǎng)絡(luò)有關(guān)的假設(shè) 398
16．6．3　變量和不變式 398
16．6．4　事件 399
16．6．5　同步 400
16．6．6　證明 400
16．7　第四次精化 400
16．7．1　與物理門有關(guān)的決策 400
16．7．2　變量和不變式：綠色鏈 401
16．7．3　變量和不變式：紅色鏈 401
16．7．4　事件 402
16．7．5　同步 404
第 17章　列車系統(tǒng) 406
17．1　非形式的引言 406
17．1．1　非形式描述的方法論約定 407
17．1．2　行車調(diào)度員控制下的軌道網(wǎng)絡(luò) 407
17．1．3　網(wǎng)絡(luò)的特殊組件：道岔和交叉點(diǎn) 407
17．1．4　阻塞的概念 409
17．1．5　通路的概念 409
17．1．6　信號的概念 411
17．1．7　通路和阻塞保持 412
17．1．8　安全性條件 414
17．1．9　運(yùn)行條件 415
17．1．10　列車的假設(shè) 415
17．1．11　事故 416
17．1．12　實(shí)例 417
17．2　精化策略 420
17．3　初始模型 420
17．3．1　狀態(tài) 420
17．3．2　事件 425
17．4　第 一次精化 427
17．4．1　狀態(tài) 427
17．4．2　事件 429
17．5　第二次精化 431
17．5．1　狀態(tài) 432
17．5．2　事件 432
17．6　第三次精化 433
17．6．1　狀態(tài) 433
17．6．2　事件 433
17．7　第四次精化 434
17．8　總結(jié) 436
17．9　參考資料 437
第 18章　一些問題 438
18．1　練習(xí) 438
18．1．1　銀行 438
18．1．2　生日記錄冊 438
18．1．3　有一行為0的數(shù)值矩陣 439
18．1．4　有序矩陣檢索 439
18．1．5　名人問題 439
18．1．6　在兩個有交集的有窮數(shù)值集合里找公共元素 440
18．1．7　簡單的訪問控制系統(tǒng) 441
18．1．8　簡單的圖書館 441
18．1．9　簡單的電路 441
18．1．10　鬧鐘 442
18．1．11　連續(xù)信號的分析 442
18．2　項(xiàng)目 443
18．2．1　旅館的電子鑰匙系統(tǒng) 443
18．2．2　Earley分析器 444
18．2．3　Schorr-Wait算法 446
18．2．4　線性表封裝 447
18．2．5　隊列的并發(fā)訪問 447
18．2．6　幾乎線性的排序 448
18．2．7　終止性檢查 449
18．2．8　分布式互斥 449
18．2．9　電梯 452
18．2．10　業(yè)務(wù)交易協(xié)議 453
18．3　數(shù)學(xué)的開發(fā) 454
18．3．1　良構(gòu)集合和關(guān)系 454
18．3．2　不動點(diǎn) 456
18．3．3　遞歸 457
18．3．4　傳遞閉包 457
18．3．5　過濾器和超過濾器 458
18．3．6　拓?fù)?458
18．3．7　Cantor-Bernstein定理 460
18．3．8　Zermelo定理 460
18．4　參考資料 462