譯者序
原書序
原書前言
第一部分 前言和發展現狀
第一章 形式化方法：應用{邏輯關係，理論}的計算機科學
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 總結和展望
參考文獻
· · · · · · (收起)