系統工程中的驗證和確認--評估UML\SysML設計模型(精)
內容大鋼
本書組織結構：第1章簡要介紹驗證和確認問題、系統工程、各種相關標準、模型驅動架構以及建模語言。第2章討論經國防組織採用和擴展的架構框架的範式，它們也作為企業架構框架應用於商業領域。第3章簡要回顧導致UML 2.0模型語言誕生的歷史背景。第4章展示的SysML建模語言，列出其得到應用的時間歷程，並且比較SysML和UML之間的共同點和具體差異。第5章描述驗證、確認和認證的概念，回顧了基於軟體工程技術、形式化驗證和程序分析的評估方法。第6章描述一種高效協同的方法來驗證和確認用標準建模語言UML、SysML表示的系統工程設計模型。第7章展示軟體工程量度在評估由UML類和包圖捕獲的結構化系統方面的相關性和實用性。第8章詳細介紹UML行為圖的自動驗證和確認。計算模型由狀態機圖、序列圖或活動圖衍生而來，並與捕獲驗證和確認需求的邏輯屬性相匹配。同時對相應的模型檢測驗證方法進行了描述。第9章討論從帶有概率註釋的SysML活動圖到馬爾可夫決策過程（MDP）的映射過程，其中MDP可以通過概率模型檢測程序進行評估。第10章使用離散時間馬爾可夫鏈模型詳細分析帶有時間約束和概率工件註釋的SysML活動圖的性能。第11章專門討論SysML活動圖的語義基礎。我們定義了一個概率演算，稱為活動演算（AC）。後者使用操作語義框架從代數上捕獲活動圖的形式化語義。第12章建立從SysML活動圖轉換到PRISM規範的合理性，這確保由我們演算法生成的代碼能夠正確地捕獲作為輸入的SysML活動圖所期望的行為。第13章對所做的工作進行了討論，並給出了一些結束語作為結論。
作者介紹
編者:(加拿大)穆拉德·德巴比//法齊·哈桑//約薩爾·賈拉亞//安德烈·索亞努//盧埃·埃爾萬內|責編:崔艷陽|譯者:江洋溢//劉欣//姜海波//夏博遠//鄧森
目錄
第1章 緒論
1.1 驗證和確認問題語句
1.2 系統工程
1.3 系統工程標準
1.4 模型驅動架構
1.5 系統工程建模語言
1.5.1 統一建模語言
1.5.2 系統建模語言
1.5.3 功能模塊集成定義方法
1.6 本書組織結構
第2章 架構框架、模型驅動架構與模擬
2.1 架構框架
2.1.1 Zachman框架
2.1.2 開放組架構框架
2.1.3 DoD架構框架
2.1.4 英國國防部架構框架
2.1.5 用於DoDAF/MoDAF的UML概要文件
2.2 AP233數據交換標準
2.3 可執行架構或從設計到模擬
2.3.1 為什麼是可執行架構
2.3.2 建模和模擬作為可執行架構的使能器
2.4 關於SE和SysML的DoDAF
2.5 小結
第3章 統一建模語言
3.1 UML的歷史
3.2 UML圖
3.2.1 類圖
3.2.2 組件圖
3.2.3 組合結構圖
3.2.4 部署圖
3.2.5 對象圖
3.2.6 包圖
3.2.7 活動圖
3.2.8 活動圖執行
3.2.9 用例圖
3.2.10 狀態機圖
3.2.11 序列圖
3.2.12 通信圖
3.2.13 交互概覽圖
3.2.14 時序圖
3.3 UML概要分析機制
3.4 小結
第4章 系統建模語言
4.1 SysML歷史
4.2 UML與SysML的關係
4.3 SysML圖
4.3.1 塊定義圖
4.3.2 內部塊圖
4.3.3 包圖
4.3.4 參數圖
4.3.5 需求圖
4.3.6 活動圖
4.3.7 狀態機圖
4.3.8 用例圖
4.3.9 序列圖
4.4 小結
第5章 驗證、確認和認證
5.1 驗證和確認技術概述
5.1.1 檢查
5.1.2 測試
5.1.3 模擬
5.1.4 引用模型等價性檢驗
5.1.5 定理證明
5.2 面向對象設計的驗證技術
5.2.1 設計透視圖
5.2.2 軟體工程技術
5.2.3 形式化驗證技術
5.2.4 程序分析技術
5.3 系統工程設計模型的驗證和確認
5.4 工具支持
5.4.1 形式化驗證環境
5.4.2 靜態分析器
5.5 小結
第6章 用於協同驗證和確認的自動化方法
6.1 協同驗證和確認方法論
6.2 系統工程專用驗證和確認方法
6.2.1 系統設計模型的自動形式化驗證
6.2.2 行為設計模型的程序分析
6.2.3 軟體工程定量技術
6.3 概率行為評估
6.4 既定結果
6.5 驗證和確認工具
6.6 小結
第7章 系統工程背景下的軟體工程量度
7.1 量度指標概述
7.1.1 Chidamber和Kemerer量度
7.1.2 面向對象設計的量度
7.1.3 Li和Henry量度
7.1.4 Lorenz和Kidd量度
7.1.5 Robert Martin量度
7.1.6 Bansiya和Davis量度
7.1.7 Briand等量度
7.2 質量屬性
7.3 軟體量度計算
7.3.1 抽象性（A）
7.3.2 不穩定性（I）
7.3.3 到主序列的距離
7.3.4 類職責
7.3.5 類屬關係型內聚度
7.3.6 繼承樹深度
7.3.7 子類數
7.3.8 對象類之間的耦合
7.3.9 方法數
7.3.10 屬性數
7.3.11 附加方法數
7.3.12 重寫方法數
7.3.13 繼承方法數
7.3.14 專門化指數
7.3.15 公共方法比
7.4 案例研究
7.5 小結
第8章 UML行為圖的驗證和確認
8.1 配置遷移系統
8.2 配置遷移系統的模型檢測
8.3 使用CTL的屬性規範
8.4 配置遷移系統程序分析
8.5 UML狀態機圖的驗證和確認
8.5.1 語義模型推導
8.5.2 案例研究
8.5.3 程序分析的應用
8.6 UML序列圖的驗證和確認
8.6.1 語義模型推導
8.6.2 序列圖案例分析
8.7 UML活動圖的驗證和確認
8.7.1 語義模型推導
8.7.2 活動圖案例分析
8.8 小結
第9章 SysML活動圖的概率模型檢測
9.1 概率驗證方法
9.2 轉譯成PRISM
9.3 PCTL*屬性規範
9.4 案例研究
9.5 小結
第10章 帶時間約束的SysML活動圖的性能分析
10.1 時間註釋
10.2 語義模型的推導
10.3 模型檢測時間約束活動圖
10.3.1 離散時間馬爾可夫鏈
10.3.2 PRISM輸入語言
10.3.3 將SysML活動圖映射到DTMC
10.3.4 線程標識
10.4 績效分析案例研究
10.5 可伸縮性
10.6 小結
第11章 SysML活動圖的語義基礎
11.1 活動演算
11.1.1 語法
11.1.2 操作語義
11.2 案例研究
11.3 馬爾可夫決策過程
11.4 小結
第12章 轉譯演算法的合理�
[