中圖網小程序
一鍵登錄
更方便
本類五星書更多>
-
>
公路車寶典(ZINN的公路車維修與保養秘籍)
-
>
晶體管電路設計(下)
-
>
基于個性化設計策略的智能交通系統關鍵技術
-
>
花樣百出:貴州少數民族圖案填色
-
>
山東教育出版社有限公司技術轉移與技術創新歷史叢書中國高等技術教育的蘇化(1949—1961)以北京地區為中心
-
>
鐵路機車概要.交流傳動內燃.電力機車
-
>
利維坦的道德困境:早期現代政治哲學的問題與脈絡
PLC程序組合檢測理論與方法 版權信息
- ISBN：9787302617587
- 條形碼：9787302617587 ; 978-7-302-61758-7
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
PLC程序組合檢測理論與方法 本書特色
工業控制系統廣泛應用于航空航天、國防工程、電力、水利、交通運輸、核電站和石油化工等安全攸關行業，是國家安全的重要組成部分。可編程邏輯控制器（Programming Logic Controler，PLC）是一種嵌入式系統和自動控制系統的核心部件，其復雜性及規模也愈加龐大，PLC運行所依賴的PLC程序正確性、可信性保障變得愈加緊迫。國際上，雖經測試的軟件由于軟件可信性問題所導致的重大災難、事故和嚴重損失屢見不鮮，如何保證PLC程序正確性得到可信驗證已經成為工業控制領域的重大現實問題。本書旨在總結在PLC程序正確性和可信安全驗證方面的研究工作，體系化構建集程序測試、模型檢測、定理證明、可信驗證和檢測優化為一體的組合檢測理論與方法，解決PLC程序運行可信性、安全與正確屬性檢測驗證等問題。
PLC程序組合檢測理論與方法 內容簡介
本書針對控制系統PLC程序的正確性和可信性檢測驗證問題，介紹了以形式化理論方法綜合運用形成組合檢測驗證體系，從多個層次檢測驗證PLC程序動態、靜態和運行的正確性
PLC程序組合檢測理論與方法 目錄
第1章 緒論
1.1 研究背景
1.1.1 PLC運行環境
1.1.2 PLC程序驗證需求
1.2 程序正確性檢測的現狀
1.2.1 代碼層次的測試技術
1.2.2 模型層次的模型檢測技術
1.2.3 規約層次的定理證明技術
1.2.4 運行層次的狀態檢測技術
1.3 程序檢測流程優化技術研究現狀
1.3.1 工作流程計劃相關研究
1.3.2 軟件檢測計劃優化技術
1.3.3 PLC程序檢測計劃技術
1.4 本書主要內容
第2章 PLC程序組合檢測體系架構
2.1 PLC工作模式以及系統模型
2.2 PLC程序組合檢測體系
2.2.1 PLC組合檢測體系構成
2.2.2 PLC程序組合檢測方法學
2.3 PLC程序組合檢測機理
2.3.1 PLC程序組合檢測流程
2.3.2 PLC程序模塊組合機制
2.4 PLC程序組合檢測研究內容
2.5 本章小結
第3章 PLC程序指稱語義
3.1 PLC主要編程指令簡介
3.1.1 IEC 61131-3
3.1.2 PLC主要硬件單元
3.1.3 PLC主要編程指令集
3.2 PLC程序體系結構的定義
3.3 PLC程序的指稱語義定義
3.3.1 PLC程序語句塊的劃分與定義
3.3.2 PLC程序基本語句塊的指稱語義函數
3.4 本章小結
第4章 PLC程序的組合測試
4.1 軟件測試技術概述
4.2 PLC嵌入式軟件測試技術的適應性研究分析
4.3 基于組合的PLC測試技術
4.3.1 PLC程序組合測試框架
4.3.2 PLC代碼塊的TA代碼
4.4 本章小結
第5章 PLC程序的組合模型檢測
5.1 組合模型檢測的主要思路
5.2 線性時序邏輯語法、語義
5.3 線性時序邏輯的模型檢測問題
5.4 模型檢測工具
5.4.1 模型檢測工具分類
5.4.2 面向屬性驗證的工具
5.4.3 面向系統分析和建模的工具
5.4.4 面向源程序驗證的工具
5.4.5 模型檢測驗證工具選擇
5.5 PLC程序的符號遷移系統表示
5.6 PLC程序的組合模型檢測
5.6.1 通用的組合檢測規則
5.6.2 PLC程序特有的組合規則
5.7 組合模型檢測的正確性
5.7.1 通用的組合檢測規則
5.7.2 PLC程序特有的組合檢測規則
5.8 檢測策略的案例分析
5.9 本章小結
第6章 PLC程序的組合證明
6.1 定理證明工具
6.1.1 COQ定理證明器
6.1.2 Automath定理證明器
6.1.3 Nqthm和ACL2定理證明器
6.1.4 Isabelle/HOL定理證明器
6.1.5 PVS定理證明器
6.1.6 Nuprl和LEGO證明開發系統
6.1.7 Mizar項目
6.2 直覺主義邏輯及其一階邏輯定義
6.3 交互式定理證明工具COQ
6.4 基于COQ的PLC程序建模
6.5 基于COQ的PLC程序性質證明
6.6 本章小結
第7章 PLC程序組合檢測實際應用
7.1 發射場系統任務與組成
7.1.1 傳統發射場系統
7.1.2 先進航天發射場系統
7.2 發射場控制系統
7.2.1 發射場智能系統構成
7.2.2 發射場控制系統組成
7.3 案例概述
7.4 航天發射擺桿控制系統
7.5 航天發射擺桿控制系統PLC輸出驅動模塊
7.5.1 發射擺桿控制功能
7.5.2 正確性驗證性質
7.6 PLC輸出驅動模塊的組合測試
7.6.1 實際測試
7.6.2 組合測試
7.7 PLC輸出驅動模塊的組合模型檢測
7.8 PLC輸出驅動模塊的組合證明
7.9 PLC輸出驅動模塊的組合檢測結果分析比較
7.10 本章小結
第8章 PLC程序運行狀態檢測
8.1 控制系統遠程智能支持體系架構
8.1.1 現場級
8.1.2 過程級
8.1.3 遠程級
8.1.4 控制任務中智能支持流程
8.2 遠程智能支持構建關鍵要素
8.2.1 PLC程序運行狀態檢測驗證
8.2.2 控制系統智能故障診斷
8.2.3 智能遠程支持
8.2.4 遠程智能支持平臺構建
8.3 可信標簽和檢測驗證協議
8.3.1 可信標簽構建
8.3.2 可信標簽簽名算法分析
8.3.3 PLC程序狀態遷移串行可信標簽檢測驗證協議
8.3.4 PLC程序狀態遷移并行可信標簽檢測驗證協議
8.3.5 協議原型系統部署試驗驗證
8.4 PLC程序狀態遷移可信標簽檢測驗證協議的安全性分析
8.4.1 外部獨立攻擊的安全性分析
8.4.2 聯合攻擊的安全性分析
8.5 本章小結
第9章 相關性驅動檢測流程優化
9.1 過程模型的選擇
9.1.1 以流程對象為主的過程模型
9.1.2 測試計劃的過程模型
9.2 PLC程序檢測過程模型的定義
9.3 檢測流程中檢測項相關性
9.4 檢測流程模型優化框架
9.4.1 強相關性檢測項的轉換
9.4.2 強相關性檢測項的同步檢測
9.4.3 強相關性檢測項的異步檢測
9.5 相關性驅動的組合檢測流程優化可行性
9.6 本章小結
參考文獻
1.1 研究背景
1.1.1 PLC運行環境
1.1.2 PLC程序驗證需求
1.2 程序正確性檢測的現狀
1.2.1 代碼層次的測試技術
1.2.2 模型層次的模型檢測技術
1.2.3 規約層次的定理證明技術
1.2.4 運行層次的狀態檢測技術
1.3 程序檢測流程優化技術研究現狀
1.3.1 工作流程計劃相關研究
1.3.2 軟件檢測計劃優化技術
1.3.3 PLC程序檢測計劃技術
1.4 本書主要內容
第2章 PLC程序組合檢測體系架構
2.1 PLC工作模式以及系統模型
2.2 PLC程序組合檢測體系
2.2.1 PLC組合檢測體系構成
2.2.2 PLC程序組合檢測方法學
2.3 PLC程序組合檢測機理
2.3.1 PLC程序組合檢測流程
2.3.2 PLC程序模塊組合機制
2.4 PLC程序組合檢測研究內容
2.5 本章小結
第3章 PLC程序指稱語義
3.1 PLC主要編程指令簡介
3.1.1 IEC 61131-3
3.1.2 PLC主要硬件單元
3.1.3 PLC主要編程指令集
3.2 PLC程序體系結構的定義
3.3 PLC程序的指稱語義定義
3.3.1 PLC程序語句塊的劃分與定義
3.3.2 PLC程序基本語句塊的指稱語義函數
3.4 本章小結
第4章 PLC程序的組合測試
4.1 軟件測試技術概述
4.2 PLC嵌入式軟件測試技術的適應性研究分析
4.3 基于組合的PLC測試技術
4.3.1 PLC程序組合測試框架
4.3.2 PLC代碼塊的TA代碼
4.4 本章小結
第5章 PLC程序的組合模型檢測
5.1 組合模型檢測的主要思路
5.2 線性時序邏輯語法、語義
5.3 線性時序邏輯的模型檢測問題
5.4 模型檢測工具
5.4.1 模型檢測工具分類
5.4.2 面向屬性驗證的工具
5.4.3 面向系統分析和建模的工具
5.4.4 面向源程序驗證的工具
5.4.5 模型檢測驗證工具選擇
5.5 PLC程序的符號遷移系統表示
5.6 PLC程序的組合模型檢測
5.6.1 通用的組合檢測規則
5.6.2 PLC程序特有的組合規則
5.7 組合模型檢測的正確性
5.7.1 通用的組合檢測規則
5.7.2 PLC程序特有的組合檢測規則
5.8 檢測策略的案例分析
5.9 本章小結
第6章 PLC程序的組合證明
6.1 定理證明工具
6.1.1 COQ定理證明器
6.1.2 Automath定理證明器
6.1.3 Nqthm和ACL2定理證明器
6.1.4 Isabelle/HOL定理證明器
6.1.5 PVS定理證明器
6.1.6 Nuprl和LEGO證明開發系統
6.1.7 Mizar項目
6.2 直覺主義邏輯及其一階邏輯定義
6.3 交互式定理證明工具COQ
6.4 基于COQ的PLC程序建模
6.5 基于COQ的PLC程序性質證明
6.6 本章小結
第7章 PLC程序組合檢測實際應用
7.1 發射場系統任務與組成
7.1.1 傳統發射場系統
7.1.2 先進航天發射場系統
7.2 發射場控制系統
7.2.1 發射場智能系統構成
7.2.2 發射場控制系統組成
7.3 案例概述
7.4 航天發射擺桿控制系統
7.5 航天發射擺桿控制系統PLC輸出驅動模塊
7.5.1 發射擺桿控制功能
7.5.2 正確性驗證性質
7.6 PLC輸出驅動模塊的組合測試
7.6.1 實際測試
7.6.2 組合測試
7.7 PLC輸出驅動模塊的組合模型檢測
7.8 PLC輸出驅動模塊的組合證明
7.9 PLC輸出驅動模塊的組合檢測結果分析比較
7.10 本章小結
第8章 PLC程序運行狀態檢測
8.1 控制系統遠程智能支持體系架構
8.1.1 現場級
8.1.2 過程級
8.1.3 遠程級
8.1.4 控制任務中智能支持流程
8.2 遠程智能支持構建關鍵要素
8.2.1 PLC程序運行狀態檢測驗證
8.2.2 控制系統智能故障診斷
8.2.3 智能遠程支持
8.2.4 遠程智能支持平臺構建
8.3 可信標簽和檢測驗證協議
8.3.1 可信標簽構建
8.3.2 可信標簽簽名算法分析
8.3.3 PLC程序狀態遷移串行可信標簽檢測驗證協議
8.3.4 PLC程序狀態遷移并行可信標簽檢測驗證協議
8.3.5 協議原型系統部署試驗驗證
8.4 PLC程序狀態遷移可信標簽檢測驗證協議的安全性分析
8.4.1 外部獨立攻擊的安全性分析
8.4.2 聯合攻擊的安全性分析
8.5 本章小結
第9章 相關性驅動檢測流程優化
9.1 過程模型的選擇
9.1.1 以流程對象為主的過程模型
9.1.2 測試計劃的過程模型
9.2 PLC程序檢測過程模型的定義
9.3 檢測流程中檢測項相關性
9.4 檢測流程模型優化框架
9.4.1 強相關性檢測項的轉換
9.4.2 強相關性檢測項的同步檢測
9.4.3 強相關性檢測項的異步檢測
9.5 相關性驅動的組合檢測流程優化可行性
9.6 本章小結
參考文獻
展開全部
PLC程序組合檢測理論與方法 作者簡介
肖力田，清華大學計算機科學與技術學科工學博士，北京特種工程設計研究院首席專家兼發射場建設責任總師、研究員；多個中央與國家專家委員會委員。 作為我國測試發射與控制技術領域專家，長期從事發射場總體論證、規劃、發展戰略和試驗技術等研究工作，是我國新型發射場建設的體系設計者和重要開拓者之一。先后擔任項目負責人、總師和第一技術責任人，出色主持完成了一系列國家重大工程研究設計與建設任務；擔任指揮部成員和測試發射總體技術專家，遂行保障了200余次重大發射任務，為我國運載火箭發射與試驗領域建設跨越式發展做出了卓越貢獻。 先后獲國家科技進步特等獎1項、二等獎1項，國家勘察設計金獎1項等；軍隊及省部級科技進步獎等44項（一等獎4項、二等獎10項）；發明專利與軟件著作權47項，發表學術論文120余篇（SCI、EI檢索46篇）、著作5部，編制發射場類國軍標3項。享受國務院政府特殊津貼；榮獲中國航天基金獎、全國工程勘察設計行業信息化突出貢獻人物獎，榮立個人二等功1次；國防科學技術工業委員會授予“十大標兵”稱號與英模等榮譽。
書友推薦
- >
唐代進士錄
- >
我與地壇
- >
推拿
- >
人文閱讀與收藏·良友文學叢書:一天的工作
- >
姑媽的寶刀
- >
伊索寓言-世界文學名著典藏-全譯本
- >
朝聞道
- >
史學評論
本類暢銷
