實時隨機系統模型檢測

內容簡介

隨著計算機技術的飛速發展，計算機系統的規模越來越大，複雜性也不斷增加，要保證系統的正確性越來越困難；同時，隨著計算機系統越來越多地套用於對安全性和可靠性要求非常高的領域，如電話交換網路、航空宇航系統、電力系統、物聯網等，系統故障所帶來的後果越來越嚴重。刻畫這類實時系統在運行中存在的不確定性，檢驗這類系統運行的可信性，是需要解決的重要科學問題。本書針對這些科學問題提供了一系列解決方案。

本書內容新穎、原創性強、受益面廣。本書是作者近年來跟蹤國際研究熱點，結合國內產業界面臨的實際問題開展一系列研究的成果。本書的研究屬於套用基礎研究，適合高年級本科生或研究生閱讀，也可供相關領域科研工作者參考使用。

圖書目錄

第1章緒論

1.1選題背景

1.2國內外研究現狀

1.2.1實時隨機系統的模型檢測

1.2.2模型檢測實時隨機系統的反例生成

1.2.3實時隨機系統模型檢測的工具

1.2.4實時隨機系統模型檢測的套用

1.3本書的研究內容與結構安排

1.3.1研究內容

1.3.2結構安排

第2章實時隨機系統的建模與性質描述

2.1時間自動機與機率時間自動機

2.1.1時間自動機

2.1.2機率時間自動機

2.2Markov決策過程

2.2.1Markov鏈

2.2.2離散時間Markov決策過程

2.2.3連續時間Markov決策過程

2.3描述實時隨機系統性質的邏輯

2.3.1PCTL、LTL和PCTL*

2.3.2CSL

第3章實時隨機系統的模型檢測

3.1代價機率時間自動機上機率有界的成本最佳化可達性

3.1.1研究背景

3.1.2代價機率時間自動機

3.1.3機率有界的成本最佳化可達性

3.1.4算法

3.1.5算法套用的推廣

3.1.6小結

3.2區間機率時間自動機的模型檢測

3.2.1研究背景

3.2.2區間機率時間自動機

3.2.3模型檢測區間機率時間自動機

3.2.4計算寬鬆區間Markov決策過程上的最大機率

3.2.5相關工作

3.2.6小結

第4章基於場景規約的實時隨機系統模型檢測

4.1研究背景

4.2機率時間活性順序圖

4.3基於元模型的PTLSC到PTA的轉換框架

4.3.1MARTE和PTA的元模型

4.3.2ATL映射規則與ATL模型轉換

4.3.3基於ATL的模型轉換

4.3.4TCS轉換與PTA的驗證

4.4基於場景規約和可視化系統建模的物聯網可信驗證

4.5可信驗證的具體步驟

4.5.1組合UPPAAL類型的機率時間自動機網路

實時隨機系統模型檢測

基本介紹

內容簡介

圖書目錄

相關詞條

熱門詞條