123,123

內(nèi)容簡(jiǎn)介

　　當(dāng)前，基于模型的系統(tǒng)工程（model - based systems engineering，MBSE）和 SysML 語(yǔ)言在國(guó)內(nèi)工業(yè)界和學(xué)術(shù)界得到廣泛應(yīng)用，但大多停留在作圖、描述或建模層面，利用系統(tǒng)模型開展問(wèn)題分析的案例鮮見(jiàn)。國(guó)際業(yè)界和研究機(jī)構(gòu)早期也有類似問(wèn)題，SysML v2 將加強(qiáng)基于模型的分析能力。基于模型的分析在復(fù)雜系統(tǒng)研究領(lǐng)域應(yīng)用廣泛，形式化驗(yàn)證是基礎(chǔ)且重要的方面，能確保系統(tǒng)邏輯建模的合理性，在 MBSE 中作用關(guān)鍵，但利用 SysML 系統(tǒng)模型開展形式化模型驗(yàn)證存在諸多不足與挑戰(zhàn)，如應(yīng)用場(chǎng)景和方法難形成標(biāo)準(zhǔn)化框架、對(duì)數(shù)學(xué)和邏輯背景要求高、缺少工具支持等，許多工程團(tuán)隊(duì)更依賴傳統(tǒng)方法，限制了系統(tǒng)模型價(jià)值，制約數(shù)字化轉(zhuǎn)型。本書介紹通過(guò)數(shù)學(xué)方法驗(yàn)證系統(tǒng)模型是否符合預(yù)期需求和規(guī)范的方法，開展基于系統(tǒng)模型的形式化分析，以解決高端裝備和復(fù)雜體系設(shè)計(jì)與評(píng)估問(wèn)題，確保系統(tǒng)正確運(yùn)行。內(nèi)容安排上，前 4 章是系統(tǒng)工程、體系架構(gòu)與框架和建模語(yǔ)言等基礎(chǔ)內(nèi)容；從第 5 章開始，介紹基于系統(tǒng)模型的驗(yàn)證、確認(rèn)和認(rèn)證的方法。在基于模型的設(shè)計(jì)實(shí)踐中，形式化驗(yàn)證是確保系統(tǒng)符合嚴(yán)格安全標(biāo)準(zhǔn)和法規(guī)的重要手段，與 MBSE 工具鏈集成實(shí)現(xiàn)自動(dòng)化驗(yàn)證后，可大幅提高驗(yàn)證效率和準(zhǔn)確性。譯者希望借此為提升國(guó)內(nèi)復(fù)雜系統(tǒng)設(shè)計(jì)能力、加速數(shù)字化轉(zhuǎn)型落地提供支撐。

作者簡(jiǎn)介

暫缺《系統(tǒng)工程中的驗(yàn)證和確認(rèn)》作者簡(jiǎn)介

圖書目錄

目錄
第 1 章緒論
1.1 驗(yàn)證和確認(rèn)問(wèn)題語(yǔ)句
1.2 系統(tǒng)工程
1.3 系統(tǒng)工程標(biāo)準(zhǔn)
1.4 模型驅(qū)動(dòng)架構(gòu)
1.5 系統(tǒng)工程建模語(yǔ)言
1.5.1 統(tǒng)一建模語(yǔ)言
1.5.2 系統(tǒng)建模語(yǔ)言
1.5.3 功能模塊集成定義方法
1.6 本書組織結(jié)構(gòu)
第 2 章架構(gòu)框架、模型驅(qū)動(dòng)架構(gòu)與仿真
2.1 架構(gòu)框架
2.1.1 Zachman 框架
2.1.2 開放組織架構(gòu)架
2.1.3 DoD 架構(gòu)框架
2.1.4 英國(guó)國(guó)防部架構(gòu)框架
2.1.5 用于 DoDAF/ModDAF 的 UML 概要文件
2.2 AP233 數(shù)據(jù)交換標(biāo)準(zhǔn)
2.3 可執(zhí)行架構(gòu)或從設(shè)計(jì)到仿真
2.3.1 為什么是可執(zhí)行架構(gòu)
2.3.2 建模和仿真作為可執(zhí)行架構(gòu)的使能器
2.4 關(guān)于 SE 和 SysML 的 DoDAF
2.5 小結(jié)
第 3 章統(tǒng)一建模語(yǔ)言
3.1 UML 的歷史
3.2 UML 圖
3.2.1 類圖
3.2.2 組件圖
3.2.3 組合結(jié)構(gòu)圖
3.2.4 部署圖
3.2.5 對(duì)象圖
3.2.6 包圖
3.2.7 活動(dòng)圖
3.2.8 活動(dòng)圖執(zhí)行
3.2.9 用例圖
3.2.10 狀態(tài)機(jī)圖
3.2.11 序列圖
3.2.12 通信圖
3.2.13 交互概覽圖
3.2.14 時(shí)序圖
3.3 UML 概要分析機(jī)制
3.4 小結(jié)
第 4 章系統(tǒng)建模語(yǔ)言
4.1 SysML 歷史
4.2 UML 與 SysML 的關(guān)系
4.3 SysML 圖
4.3.1 塊定義圖
4.3.2 內(nèi)部塊圖
4.3.3 包圖
4.3.4 參數(shù)圖
4.3.5 需求圖
4.3.6 活動(dòng)圖
4.3.7 狀態(tài)機(jī)圖
4.3.8 用例圖
4.3.9 序列圖
4.4 小結(jié)
第 5 章驗(yàn)證、確認(rèn)和認(rèn)證
5.1 驗(yàn)證和確認(rèn)技術(shù)概述
5.1.1 檢查
5.1.2 測(cè)試
5.1.3 仿真
5.1.4 引用模型等價(jià)性檢驗(yàn)
5.1.5 定理證明
5.2 面向?qū)ο笤O(shè)計(jì)的驗(yàn)證技術(shù)
5.2.1 設(shè)計(jì)透視圖
5.2.2 軟件工程技術(shù)
5.2.3 形式化驗(yàn)證技術(shù)
5.2.4 程序分析技術(shù)
5.3 系統(tǒng)工程設(shè)計(jì)模型的驗(yàn)證和確認(rèn)
5.4 工具支持
5.4.1 形式化驗(yàn)證環(huán)境
5.4.2 靜態(tài)分析器
5.5 小結(jié)
第 6 章用于協(xié)同驗(yàn)證和確認(rèn)的自動(dòng)化方法
6.1 協(xié)同驗(yàn)證和確認(rèn)方法論
6.2 系統(tǒng)工程專用驗(yàn)證和確認(rèn)方法
6.2.1 系統(tǒng)設(shè)計(jì)模型的自動(dòng)形式化驗(yàn)證
6.2.2 行為設(shè)計(jì)模型的程序分析
6.2.3 軟件工程定量技術(shù)
6.3 概率行為評(píng)估
6.4 既定結(jié)果
6.5 驗(yàn)證和確認(rèn)工具
6.6 小結(jié)
第 7 章系統(tǒng)工程背景下的軟件工程量度
7.1 量度指標(biāo)概述
7.1.1 Chidamber 和 Kemerer 量度
7.1.2 面向?qū)ο笤O(shè)計(jì)的量度
7.1.3 Li 和 Henry 量度
7.1.4 Lorenz 和 Kidd 量度
7.1.5 Robert Martin 量度