《工業關鍵系統的形式化方法》是2015年機械工業出版社出版的圖書，作者是Stefania Gnesi。
綜合最先進的文獻資料和常用方法，案例均來自實際開發過程。
基本介紹
- 書名：工業關鍵系統的形式化方法：套用綜述
- 作者：（意）Stefania Gnesi
- 譯者：靳添絮
- ISBN：978-7-111-48521-6
- 頁數：228
- 定價：69.00
- 出版社：機械工業出版社
- 出版時間：2015-01
- 裝幀：平裝
- 開本：16
- 叢書名：國際信息工程先進技術譯叢
內容簡介,目錄,
內容簡介
形式化方法以數學為基礎，其目標是建立精確的、無二義性的語義，對系統開發的各個階段進行有效地描述，使系統的結構具有先天的合理性、正確性和良好的維護性，能較好地滿足用戶需求。本書記錄和展示了作者關於形式化方法如何在工業關鍵系統中進行套用的研究成果。
本書分為6部分。第1部分是概述；第2部分致力於介紹建模範例；第3部分介紹了包括形式化方法和相關工具的使用以及應用程式在實際系統領域的發展；第4部分則向讀者展示了形式化方法在通信系統中的發展和成果；第5部分則介紹了形式化方法在網際網路和線上服務方面的套用；而在第6部分則介紹了實時應用程式的形式化方法。
本書可用作高等院校計算機科學、自動化相關專業本科生、研究生以及教師的參考用書，也可作為業內專業人士的參考書。
目錄
譯者序
原書序
原書前言
第一部分 前言和發展現狀
第一章 形式化方法：套用{邏輯關係，理論}的計算機科學
1.1前言和發展現狀
1.2未來發展方向
致謝
參考文獻
第二部分 建模範式
第二章一種正在套用的同步語言：LUSTRE的發展
2.1前言
2.2同步語言風格
2.3 LUSTR和SCADE的設計和開發
2.3.1 工業發展
2.3.2 研究階段
2.4 工業套用案例
2.4.1預期成果
2.4.2意外功能和需求
2.5 現狀
第三章群智慧型方法形式化集成要求
3.1 前言
3.2 群體技術
3.2.1ANTS任務概述
3.2.2 ANTS規範和驗證
3.3 美國宇航局（NASA）FAST項目
3.4群體形式化集成方法
3.4.1 CSP簡述
3.4.2WSCCS 簡述
3.4.3X-機
3.4.4unity邏輯
3.5 結論
致謝
參考文獻
第三部分 交通運輸系統
第四章形式化方法在鐵路交通信號中的套用趨勢
4.1 前言
4.2 CENELEC準則
4.3 鐵路信號系統軟體採購
4.3.1系統分類
4.3.2需求分析和規範
4.4 成功案例：B方法
4.5 鐵路信號設備分類
4.5.1列車控制系統
4.5.2聯鎖系統
4.5.3 EURIS語言
4.6 結論
參考文獻
第五章航空電子設備的符號模型校驗
5.1前言
5.2 飛行跑道安全監控套用
5.2.1RSM的作用
5.2.2RSM的設計
5.2.3RSM的形式化驗證
5.2.4符號模型校驗結構
5.2.5符號狀態空間生成飽和算法
5.2.6基於飽和算法的模型校驗
5.2.7隨機模型校驗可靠性和定時分析工具(SmArT)
5.3 RSM的離散模型
5.3.1整型變數和實型變數抽象化
5.3.2RSM的SMART模型
5.3.3RSM模型校驗
5.4 探討80
5.4.1 經驗教訓
5.4.2 投入程度
5.4.3 故障容錯
5.4.4 面臨挑戰
參考文獻
第四部分 電信系統
第六章形式化方法在有源網路電信服務中的套用
6.1概述
6.2 有源網路
6.3 Capsule法
6.4 有源網路的之前分析方法
6.4.1Maude
6.4.2 ACTIVESPEC
6.4.3 Unity
6.4.4Verisim法
6.5 SPIN有源網路模型校驗
6.5.1 PROMELA中的有源網路模型
6.5.2實例：驗證主動協定
6.5.3在SPIN中更實際的代碼建模
6.6結論
參考文獻
第七章通信協定機率模型校驗的實際套用
7.1前言
7.2 PTAs
7.3機率模型校驗
7.3.1機率模型校驗技術
7.3.2機率模型校驗工具
7.4案例分析:CSMA / CD
7.4.1協定
7.4.2PTA模型
7.4.3模型分析
7.5討論和結論
致謝
參考文獻
第五部分 網際網路與線上服務
第八章可驗證性設計：線上會議系統案例分析
8.1前言
8.2 用戶模型
8.3模型與框架
8.4模型校驗
8.5通過自動機學習的應急全局行為驗證
8.5.1學習設定
8.5.2學習行為模型
8.5.3便於領域知識的自動機學習
8.6相關工作
8.6.1基於特徵的系統
8.6.2線上會議系統
8.6.3 政策
8.7 結論和展望
參考文獻
第九章隨機模型校驗在工業中的套用: 用戶中心建模和THINKTEAM中的合作分析
9.1 前言
9.2 THINKTEAM
9.2.1 技術特點
9.2.2thinkteam 的工作過程
9.3 thinkteam日誌檔案分析
9.4 具有複製倉庫的thinkteam
9.4.1 thinkteam的隨機模型
9.4.2 隨機模型分析
9.5 經驗教訓
9.6 總結
致謝
參考文獻
第六部分 運行時：測試和模型學習
第十章 測試和測試控制符號TTCN-3及其套用
10.1前言
10.2 TTCN-3概念
10.2.1模組
10.2.2測試系統
10.2.3測試案例和測試判決
10.2.4備選方案和快照
10.2.5 預設處理
10.2.6 通信操作
10.2.7 測試數據規範
10.3 入門示例
10.4 TTCN-3語義及其套用
10.5 TTCN-3的分散式測試平台
10.6 案例分析I：開放式服務架構（OSA）/增值服務測試
10.7 案例分析II：IP多媒體子系統（IMS）裝置測試
10.8 結論
參考文獻
第十一章 主動自動機學習的實際套用
11.1 前言
11.2 常規外推法
11.2.1 充分行為建模
11.3 常規外推法的挑戰
11.3.1 等價查詢注釋
11.4 與實際系統互動
11.4.1測試驅動程式設計示例
11.5 隸屬度查詢
11.5.1 冗餘度
11.5.2前綴閉包
11.5.3 行為獨立性
11.5.4 確定性輸入
11.5.5 對稱性
11.5.6 濾波器示例
11.6 重置
11.6.1 重置示例
11.7 參數和值域
11.7.1 參數化示例
11.8 NGLL
11.8.1 基本技術
11.8.2 建模學習設定
11.9 總結和展望
參考文獻
原書序
原書前言
第一部分 前言和發展現狀
第一章 形式化方法：套用{邏輯關係，理論}的計算機科學
1.1前言和發展現狀
1.2未來發展方向
致謝
參考文獻
第二部分 建模範式
第二章一種正在套用的同步語言：LUSTRE的發展
2.1前言
2.2同步語言風格
2.3 LUSTR和SCADE的設計和開發
2.3.1 工業發展
2.3.2 研究階段
2.4 工業套用案例
2.4.1預期成果
2.4.2意外功能和需求
2.5 現狀
第三章群智慧型方法形式化集成要求
3.1 前言
3.2 群體技術
3.2.1ANTS任務概述
3.2.2 ANTS規範和驗證
3.3 美國宇航局（NASA）FAST項目
3.4群體形式化集成方法
3.4.1 CSP簡述
3.4.2WSCCS 簡述
3.4.3X-機
3.4.4unity邏輯
3.5 結論
致謝
參考文獻
第三部分 交通運輸系統
第四章形式化方法在鐵路交通信號中的套用趨勢
4.1 前言
4.2 CENELEC準則
4.3 鐵路信號系統軟體採購
4.3.1系統分類
4.3.2需求分析和規範
4.4 成功案例：B方法
4.5 鐵路信號設備分類
4.5.1列車控制系統
4.5.2聯鎖系統
4.5.3 EURIS語言
4.6 結論
參考文獻
第五章航空電子設備的符號模型校驗
5.1前言
5.2 飛行跑道安全監控套用
5.2.1RSM的作用
5.2.2RSM的設計
5.2.3RSM的形式化驗證
5.2.4符號模型校驗結構
5.2.5符號狀態空間生成飽和算法
5.2.6基於飽和算法的模型校驗
5.2.7隨機模型校驗可靠性和定時分析工具(SmArT)
5.3 RSM的離散模型
5.3.1整型變數和實型變數抽象化
5.3.2RSM的SMART模型
5.3.3RSM模型校驗
5.4 探討80
5.4.1 經驗教訓
5.4.2 投入程度
5.4.3 故障容錯
5.4.4 面臨挑戰
參考文獻
第四部分 電信系統
第六章形式化方法在有源網路電信服務中的套用
6.1概述
6.2 有源網路
6.3 Capsule法
6.4 有源網路的之前分析方法
6.4.1Maude
6.4.2 ACTIVESPEC
6.4.3 Unity
6.4.4Verisim法
6.5 SPIN有源網路模型校驗
6.5.1 PROMELA中的有源網路模型
6.5.2實例：驗證主動協定
6.5.3在SPIN中更實際的代碼建模
6.6結論
參考文獻
第七章通信協定機率模型校驗的實際套用
7.1前言
7.2 PTAs
7.3機率模型校驗
7.3.1機率模型校驗技術
7.3.2機率模型校驗工具
7.4案例分析:CSMA / CD
7.4.1協定
7.4.2PTA模型
7.4.3模型分析
7.5討論和結論
致謝
參考文獻
第五部分 網際網路與線上服務
第八章可驗證性設計：線上會議系統案例分析
8.1前言
8.2 用戶模型
8.3模型與框架
8.4模型校驗
8.5通過自動機學習的應急全局行為驗證
8.5.1學習設定
8.5.2學習行為模型
8.5.3便於領域知識的自動機學習
8.6相關工作
8.6.1基於特徵的系統
8.6.2線上會議系統
8.6.3 政策
8.7 結論和展望
參考文獻
第九章隨機模型校驗在工業中的套用: 用戶中心建模和THINKTEAM中的合作分析
9.1 前言
9.2 THINKTEAM
9.2.1 技術特點
9.2.2thinkteam 的工作過程
9.3 thinkteam日誌檔案分析
9.4 具有複製倉庫的thinkteam
9.4.1 thinkteam的隨機模型
9.4.2 隨機模型分析
9.5 經驗教訓
9.6 總結
致謝
參考文獻
第六部分 運行時：測試和模型學習
第十章 測試和測試控制符號TTCN-3及其套用
10.1前言
10.2 TTCN-3概念
10.2.1模組
10.2.2測試系統
10.2.3測試案例和測試判決
10.2.4備選方案和快照
10.2.5 預設處理
10.2.6 通信操作
10.2.7 測試數據規範
10.3 入門示例
10.4 TTCN-3語義及其套用
10.5 TTCN-3的分散式測試平台
10.6 案例分析I：開放式服務架構（OSA）/增值服務測試
10.7 案例分析II：IP多媒體子系統（IMS）裝置測試
10.8 結論
參考文獻
第十一章 主動自動機學習的實際套用
11.1 前言
11.2 常規外推法
11.2.1 充分行為建模
11.3 常規外推法的挑戰
11.3.1 等價查詢注釋
11.4 與實際系統互動
11.4.1測試驅動程式設計示例
11.5 隸屬度查詢
11.5.1 冗餘度
11.5.2前綴閉包
11.5.3 行為獨立性
11.5.4 確定性輸入
11.5.5 對稱性
11.5.6 濾波器示例
11.6 重置
11.6.1 重置示例
11.7 參數和值域
11.7.1 參數化示例
11.8 NGLL
11.8.1 基本技術
11.8.2 建模學習設定
11.9 總結和展望
參考文獻
