PLC程序組合檢測理論與方法

定　價(jià)：￥139.00

作　者：	肖力田、肖楠、李孟源
出版社：	清華大學(xué)出版社
叢編項(xiàng)：
標(biāo)　簽：	暫缺

購買這本書可以去

當(dāng)當(dāng)網(wǎng) (￥115.40)

ISBN：	9787302617587	出版時(shí)間：	2022-11-01	包裝：	精裝
開本：	16開	頁數(shù)：		字?jǐn)?shù)：

內(nèi)容簡介

　　本書針對(duì)控制系統(tǒng)PLC程序的正確性和可信性檢測驗(yàn)證問題，介紹了以形式化理論方法綜合運(yùn)用形成組合檢測驗(yàn)證體系，從多個(gè)層次檢測驗(yàn)證PLC程序動(dòng)態(tài)、靜態(tài)和運(yùn)行的正確性

作者簡介

　　肖力田，清華大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)博士，北京特種工程設(shè)計(jì)研究院首席專家兼航天發(fā)射場建設(shè)責(zé)任總師、研究員；多個(gè)中央與國家專家咨詢委員會(huì)委員。作為我國航天測試發(fā)射與控制技術(shù)領(lǐng)域?qū)＜?，長期從事航天發(fā)射場總體論證、規(guī)劃、發(fā)展戰(zhàn)略和試驗(yàn)技術(shù)等研究工作，是我國新型航天發(fā)射場建設(shè)的體系設(shè)計(jì)者和重要開拓者之一。先后擔(dān)任項(xiàng)目負(fù)責(zé)人、總師和技術(shù)責(zé)任人，出色主持完成了一系列國家重大工程研究設(shè)計(jì)與建設(shè)任務(wù)；擔(dān)任指揮部成員和測試發(fā)射總體技術(shù)專家，遂行保障了200余次重大發(fā)射任務(wù)，為我國航天發(fā)射領(lǐng)域建設(shè)跨越式發(fā)展做出了卓越貢獻(xiàn)。先后獲國家科技進(jìn)步特等獎(jiǎng)1項(xiàng)、二等獎(jiǎng)1項(xiàng)，國家勘察設(shè)計(jì)金獎(jiǎng)1項(xiàng)等；軍隊(duì)及省部級(jí)科技進(jìn)步獎(jiǎng)等44項(xiàng)（一等獎(jiǎng)4項(xiàng)、二等獎(jiǎng)10項(xiàng)）；發(fā)明專利與軟件著作權(quán)47項(xiàng)，發(fā)表學(xué)術(shù)論文120余篇、著作5部，編制航天發(fā)射場類國軍標(biāo)3項(xiàng)。享受國務(wù)院政府特殊津貼；榮獲中國航天基金會(huì)獎(jiǎng)、信息化突出貢獻(xiàn)人物獎(jiǎng)，榮立個(gè)人二等功1次；原國防科學(xué)技術(shù)工業(yè)委員會(huì)授予“十大標(biāo)兵”稱號(hào)與英模等榮譽(yù)。

圖書目錄

第1章緒論 1
1.1 研究背景 2
1.1.1 PLC運(yùn)行環(huán)境 5
1.1.2 PLC程序驗(yàn)證需求 7
1.2 程序正確性檢測的現(xiàn)狀 8
1.2.1 代碼層次的測試技術(shù) 9
1.2.2 模型層次的模型檢測技術(shù) 10
1.2.3 規(guī)約層次的定理證明技術(shù) 14
1.2.4 運(yùn)行層次的狀態(tài)檢測技術(shù) 16
1.3 程序檢測流程優(yōu)化技術(shù)研究現(xiàn)狀 24
1.3.1 工作流程計(jì)劃相關(guān)研究 25
1.3.2 軟件檢測計(jì)劃優(yōu)化技術(shù) 32
1.3.3 PLC程序檢測計(jì)劃技術(shù) 36
1.4 本書主要內(nèi)容 37
第2章 PLC程序組合檢測體系架構(gòu) 39
2.1 PLC工作模式以及系統(tǒng)模型 41
2.2 PLC程序組合檢測體系 44
2.2.1 PLC組合檢測體系構(gòu)成 44
2.2.2 PLC程序組合檢測方法學(xué) 45
2.3 PLC程序組合檢測機(jī)理 48
2.3.1 PLC程序組合檢測流程 48
2.3.2 PLC程序模塊組合機(jī)制 50
2.4 PLC程序組合檢測研究內(nèi)容 54
2.5 本章小結(jié) 57
第3章 PLC程序指稱語義 59
3.1 PLC主要編程指令簡介 60
3.1.1 IEC 61131-3 60
3.1.2 PLC主要硬件單元 61
3.1.3 PLC主要編程指令集 64
3.2 PLC程序體系結(jié)構(gòu)的定義 73
3.3 PLC程序的指稱語義定義 76
3.3.1 PLC程序語句塊的劃分與定義 76
3.3.2 PLC程序基本語句塊的指稱語義函數(shù) 79
3.4 本章小結(jié) 86
第4章 PLC程序的組合測試 87
4.1 軟件測試技術(shù)概述 88
4.2 PLC嵌入式軟件測試技術(shù)的適應(yīng)性研究分析 88
4.3 基于組合的PLC測試技術(shù) 92
4.3.1 PLC程序組合測試框架 92
4.3.2 PLC代碼塊的TA代碼 93
4.4 本章小結(jié) 100
第5章 PLC程序的組合模型檢測 102
5.1 組合模型檢測的主要思路 103
5.2 線性時(shí)序邏輯語法、語義 105
5.3 線性時(shí)序邏輯的模型檢測問題 106
5.4 模型檢測工具 108
5.4.1 模型檢測工具分類 108
5.4.2 面向?qū)傩则?yàn)證的工具 110
5.4.3 面向系統(tǒng)分析和建模的工具 113
5.4.4 面向源程序驗(yàn)證的工具 117
5.4.5 模型檢測驗(yàn)證工具選擇 124
5.5 PLC程序的符號(hào)遷移系統(tǒng)表示 125
5.6 PLC程序的組合模型檢測 128
5.6.1 通用的組合檢測規(guī)則 129
5.6.2 PLC程序特有的組合規(guī)則 131
5.7 組合模型檢測的正確性 133
5.7.1 通用的組合檢測規(guī)則 133
5.7.2 PLC程序特有的組合檢測規(guī)則 136
5.8 檢測策略的案例分析 138
5.9 本章小結(jié) 141
第6章 PLC程序的組合證明 142
6.1 定理證明工具 144
6.1.1 COQ定理證明器 145
6.1.2 Automath定理證明器 146
6.1.3 Nqthm和ACL2定理證明器 147
6.1.4 Isabelle/HOL定理證明器 149
6.1.5 PVS定理證明器 151
6.1.6 Nuprl和LEGO證明開發(fā)系統(tǒng) 152
6.1.7 Mizar項(xiàng)目 154
6.2 直覺主義邏輯及其一階邏輯定義 155
6.3 交互式定理證明工具COQ 159
6.4 基于COQ的PLC程序建模 161
6.5 基于COQ的PLC程序性質(zhì)證明 173
6.6 本章小結(jié) 174
第7章 PLC程序組合檢測實(shí)際應(yīng)用 176
7.1 發(fā)射場系統(tǒng)任務(wù)與組成 177
7.1.1 傳統(tǒng)發(fā)射場系統(tǒng) 178
7.1.2 先進(jìn)航天發(fā)射場系統(tǒng) 180
7.2 發(fā)射場控制系統(tǒng) 185
7.2.1 發(fā)射場智能系統(tǒng)構(gòu)成 185
7.2.2 發(fā)射場控制系統(tǒng)組成 187
7.3 案例概述 189
7.4 航天發(fā)射擺桿控制系統(tǒng) 190
7.5 航天發(fā)射擺桿控制系統(tǒng)PLC輸出驅(qū)動(dòng)模塊 192
7.5.1 發(fā)射擺桿控制功能 192
7.5.2 正確性驗(yàn)證性質(zhì) 194
7.6 PLC輸出驅(qū)動(dòng)模塊的組合測試 196
7.6.1 實(shí)際測試 196
7.6.2 組合測試 197
7.7 PLC輸出驅(qū)動(dòng)模塊的組合模型檢測 198
7.8 PLC輸出驅(qū)動(dòng)模塊的組合證明 199
7.9 PLC輸出驅(qū)動(dòng)模塊的組合檢測結(jié)果分析比較 201
7.10 本章小結(jié) 202
第8章 PLC程序運(yùn)行狀態(tài)檢測 203
8.1 控制系統(tǒng)遠(yuǎn)程智能支持體系架構(gòu) 204
8.1.1 現(xiàn)場級(jí) 205
8.1.2 過程級(jí) 206
8.1.3 遠(yuǎn)程級(jí) 206
8.1.4 控制任務(wù)中智能支持流程 207
8.2 遠(yuǎn)程智能支持構(gòu)建關(guān)鍵要素 208
8.2.1 PLC程序運(yùn)行狀態(tài)檢測驗(yàn)證 208
8.2.2 控制系統(tǒng)智能故障診斷 209
8.2.3 智能遠(yuǎn)程支持 210
8.2.4 遠(yuǎn)程智能支持平臺(tái)構(gòu)建 211
8.3 可信標(biāo)簽和檢測驗(yàn)證協(xié)議 212
8.3.1 可信標(biāo)簽構(gòu)建 212
8.3.2 可信標(biāo)簽簽名算法分析 214
8.3.3 PLC程序狀態(tài)遷移串行可信標(biāo)簽檢測驗(yàn)證協(xié)議 215
8.3.4 PLC程序狀態(tài)遷移并行可信標(biāo)簽檢測驗(yàn)證協(xié)議 218
8.3.5 協(xié)議原型系統(tǒng)部署試驗(yàn)驗(yàn)證 220
8.4 PLC程序狀態(tài)遷移可信標(biāo)簽檢測驗(yàn)證協(xié)議的安全性分析 221
8.4.1 外部獨(dú)立攻擊的安全性分析 222
8.4.2 聯(lián)合攻擊的安全性分析 223
8.5 本章小結(jié) 224
第9章相關(guān)性驅(qū)動(dòng)檢測流程優(yōu)化 225
9.1 過程模型的選擇 226
9.1.1 以流程對(duì)象為主的過程模型 226
9.1.2 測試計(jì)劃的過程模型 228
9.2 PLC程序檢測過程模型的定義 228
9.3 檢測流程中檢測項(xiàng)相關(guān)性 232
9.4 檢測流程模型優(yōu)化框架 233
9.4.1 強(qiáng)相關(guān)性檢測項(xiàng)的轉(zhuǎn)換 233
9.4.2 強(qiáng)相關(guān)性檢測項(xiàng)的同步檢測 234
9.4.3 強(qiáng)相關(guān)性檢測項(xiàng)的異步檢測 234
9.5 相關(guān)性驅(qū)動(dòng)的組合檢測流程優(yōu)化可行性 236
9.6 本章小結(jié) 238
參考文獻(xiàn) 239