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

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

第二部分 建模范式
第二章一種正在應(yīng)用的同步語(yǔ)言：LUSTRE的發(fā)展
2.1前言
2.2同步語(yǔ)言風(fēng)格
2.3 LUSTR和SCADE的設(shè)計(jì)和開(kāi)發(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ī)范和驗(yàn)證
3.3 美國(guó)宇航局（NASA）FAST項(xiàng)目
3.4群體形式化集成方法
3.4.1 CSP簡(jiǎn)述
3.4.2WSCCS 簡(jiǎn)述
3.4.3X-機(jī)
3.4.4unity邏輯
3.5 結(jié)論
致謝
參考文獻(xiàn)

第三部分 交通運(yùn)輸系統(tǒng)
第四章形式化方法在鐵路交通信號(hào)中的應(yīng)用趨勢(shì)
4.1 前言
4.2 CENELEC準(zhǔn)則
4.3 鐵路信號(hào)系統(tǒng)軟件采購(gòu)
4.3.1系統(tǒng)分類
4.3.2需求分析和規(guī)范
4.4 成功案例：B方法
4.5 鐵路信號(hào)設(shè)備分類
4.5.1列車控制系統(tǒng)
4.5.2聯(lián)鎖系統(tǒng)
4.5.3 EURIS語(yǔ)言
4.6 結(jié)論
參考文獻(xiàn)
第五章航空電子設(shè)備的符號(hào)模型校驗(yàn)
5.1前言
5.2 飛行跑道安全監(jiān)控應(yīng)用
5.2.1RSM的作用
5.2.2RSM的設(shè)計(jì)
5.2.3RSM的形式化驗(yàn)證
5.2.4符號(hào)模型校驗(yàn)結(jié)構(gòu)
5.2.5符號(hào)狀態(tài)空間生成飽和算法
5.2.6基于飽和算法的模型校驗(yàn)
5.2.7隨機(jī)模型校驗(yàn)可靠性和定時(shí)分析工具(SmArT)
5.3 RSM的離散模型
5.3.1整型變量和實(shí)型變量抽象化
5.3.2RSM的SMART模型
5.3.3RSM模型校驗(yàn)
5.4 探討80
5.4.1 經(jīng)驗(yàn)教訓(xùn)
5.4.2 投入程度
5.4.3 故障容錯(cuò)
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ò)模型校驗(yàn)
6.5.1 PROMELA中的有源網(wǎng)絡(luò)模型
6.5.2實(shí)例：驗(yàn)證主動(dòng)協(xié)議
6.5.3在SPIN中更實(shí)際的代碼建模
6.6結(jié)論
參考文獻(xiàn)
第七章通信協(xié)議概率模型校驗(yàn)的實(shí)際應(yīng)用
7.1前言
7.2 PTAs
7.3概率模型校驗(yàn)
7.3.1概率模型校驗(yàn)技術(shù)
7.3.2概率模型校驗(yàn)工具
7.4案例分析:CSMA / CD
7.4.1協(xié)議
7.4.2PTA模型
7.4.3模型分析
7.5討論和結(jié)論
致謝
參考文獻(xiàn)

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

第六部分 運(yùn)行時(shí)：測(cè)試和模型學(xué)習(xí)
第十章 測(cè)試和測(cè)試控制符號(hào)TTCN-3及其應(yīng)用
10.1前言
10.2 TTCN-3概念
10.2.1模塊
10.2.2測(cè)試系統(tǒng)
10.2.3測(cè)試案例和測(cè)試判決
10.2.4備選方案和快照
10.2.5 缺省處理
10.2.6 通信操作
10.2.7 測(cè)試數(shù)據(jù)規(guī)范
10.3 入門示例
10.4 TTCN-3語(yǔ)義及其應(yīng)用
10.5 TTCN-3的分布式測(cè)試平臺(tái)
10.6 案例分析I：開(kāi)放式服務(wù)架構(gòu)（OSA）/增值服務(wù)測(cè)試
10.7 案例分析II：IP多媒體子系統(tǒng)（IMS）裝置測(cè)試
10.8 結(jié)論
參考文獻(xiàn)
第十一章 主動(dòng)自動(dòng)機(jī)學(xué)習(xí)的實(shí)際應(yīng)用
11.1 前言
11.2 常規(guī)外推法
11.2.1 充分行為建模
11.3 常規(guī)外推法的挑戰(zhàn)
11.3.1 等價(jià)查詢注釋
11.4 與實(shí)際系統(tǒng)交互
11.4.1測(cè)試驅(qū)動(dòng)程序設(shè)計(jì)示例
11.5 隸屬度查詢
11.5.1 冗余度
11.5.2前綴閉包
11.5.3 行為獨(dú)立性
11.5.4 確定性輸入
11.5.5 對(duì)稱性
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)