工業(yè)關(guān)鍵系統(tǒng)的形式化方法：應(yīng)用綜述

譯者序
原書序
原書前言
第一部分 前言和發(fā)展現(xiàn)狀
第一章 形式化方法：應(yīng)用{邏輯關(guān)系，理論}的計算機科學(xué)
1.1前言和發(fā)展現(xiàn)狀
1.2未來發(fā)展方向
致謝
參考文獻(xiàn)

第二部分 建模范式
第二章一種正在應(yīng)用的同步語言：LUSTRE的發(fā)展
2.1前言
2.2同步語言風(fēng)格
2.3 LUSTR和SCADE的設(shè)計和開發(fā)
2.3.1 工業(yè)發(fā)展
2.3.2 研究階段
2.4 工業(yè)應(yīng)用案例
2.4.1預(yù)期成果
2.4.2意外功能和需求
2.5 現(xiàn)狀
第三章群智能方法形式化集成要求
3.1 前言
3.2 群體技術(shù)
3.2.1ANTS任務(wù)概述
3.2.2 ANTS規(guī)范和驗證
3.3 美國宇航局（NASA）FAST項目
3.4群體形式化集成方法
3.4.1 CSP簡述
3.4.2WSCCS 簡述
3.4.3X-機
3.4.4unity邏輯
3.5 結(jié)論
致謝
參考文獻(xiàn)

第三部分 交通運輸系統(tǒng)
第四章形式化方法在鐵路交通信號中的應(yīng)用趨勢
4.1 前言
4.2 CENELEC準(zhǔn)則
4.3 鐵路信號系統(tǒng)軟件采購
4.3.1系統(tǒng)分類
4.3.2需求分析和規(guī)范
4.4 成功案例：B方法
4.5 鐵路信號設(shè)備分類
4.5.1列車控制系統(tǒng)
4.5.2聯(lián)鎖系統(tǒng)
4.5.3 EURIS語言
4.6 結(jié)論
參考文獻(xiàn)
第五章航空電子設(shè)備的符號模型校驗
5.1前言
5.2 飛行跑道安全監(jiān)控應(yīng)用
5.2.1RSM的作用
5.2.2RSM的設(shè)計
5.2.3RSM的形式化驗證
5.2.4符號模型校驗結(jié)構(gòu)
5.2.5符號狀態(tài)空間生成飽和算法
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 經(jīng)驗教訓(xùn)
5.4.2 投入程度
5.4.3 故障容錯
5.4.4 面臨挑戰(zhàn)
參考文獻(xiàn)

第四部分 電信系統(tǒng)
第六章形式化方法在有源網(wǎng)絡(luò)電信服務(wù)中的應(yīng)用
6.1概述
6.2 有源網(wǎng)絡(luò)
6.3 Capsule法
6.4 有源網(wǎng)絡(luò)的之前分析方法
6.4.1Maude
6.4.2 ACTIVESPEC
6.4.3 Unity
6.4.4Verisim法
6.5 SPIN有源網(wǎng)絡(luò)模型校驗
6.5.1 PROMELA中的有源網(wǎng)絡(luò)模型
6.5.2實例：驗證主動協(xié)議
6.5.3在SPIN中更實際的代碼建模
6.6結(jié)論
參考文獻(xiàn)
第七章通信協(xié)議概率模型校驗的實際應(yīng)用
7.1前言
7.2 PTAs
7.3概率模型校驗
7.3.1概率模型校驗技術(shù)
7.3.2概率模型校驗工具
7.4案例分析:CSMA / CD
7.4.1協(xié)議
7.4.2PTA模型
7.4.3模型分析
7.5討論和結(jié)論
致謝
參考文獻(xiàn)

第五部分 互聯(lián)網(wǎng)與在線服務(wù)
第八章可驗證性設(shè)計：在線會議系統(tǒng)案例分析
8.1前言
8.2 用戶模型
8.3模型與框架
8.4模型校驗
8.5通過自動機學(xué)習(xí)的應(yīng)急全局行為驗證
8.5.1學(xué)習(xí)設(shè)置
8.5.2學(xué)習(xí)行為模型
8.5.3便于領(lǐng)域知識的自動機學(xué)習(xí)
8.6相關(guān)工作
8.6.1基于特征的系統(tǒng)
8.6.2在線會議系統(tǒng)
8.6.3 政策
8.7 結(jié)論和展望
參考文獻(xiàn)
第九章隨機模型校驗在工業(yè)中的應(yīng)用: 用戶中心建模和THINKTEAM中的合作分析
9.1 前言
9.2 THINKTEAM
9.2.1 技術(shù)特點
9.2.2thinkteam 的工作過程
9.3 thinkteam日志文件分析
9.4 具有復(fù)制倉庫的thinkteam
9.4.1 thinkteam的隨機模型
9.4.2 隨機模型分析
9.5 經(jīng)驗教訓(xùn)
9.6 總結(jié)
致謝
參考文獻(xiàn)

第六部分 運行時：測試和模型學(xué)習(xí)
第十章 測試和測試控制符號TTCN-3及其應(yīng)用
10.1前言
10.2 TTCN-3概念
10.2.1模塊
10.2.2測試系統(tǒng)
10.2.3測試案例和測試判決
10.2.4備選方案和快照
10.2.5 缺省處理
10.2.6 通信操作
10.2.7 測試數(shù)據(jù)規(guī)范
10.3 入門示例
10.4 TTCN-3語義及其應(yīng)用
10.5 TTCN-3的分布式測試平臺
10.6 案例分析I：開放式服務(wù)架構(gòu)（OSA）/增值服務(wù)測試
10.7 案例分析II：IP多媒體子系統(tǒng)（IMS）裝置測試
10.8 結(jié)論
參考文獻(xiàn)
第十一章 主動自動機學(xué)習(xí)的實際應(yīng)用
11.1 前言
11.2 常規(guī)外推法
11.2.1 充分行為建模
11.3 常規(guī)外推法的挑戰(zhàn)
11.3.1 等價查詢注釋
11.4 與實際系統(tǒng)交互
11.4.1測試驅(qū)動程序設(shè)計示例
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 參數(shù)和值域
11.7.1 參數(shù)化示例
11.8 NGLL
11.8.1 基本技術(shù)
11.8.2 建模學(xué)習(xí)設(shè)置
11.9 總結(jié)和展望
參考文獻(xiàn)