基于模型的系統(tǒng)工程(Model-Based Systems Engineering,MBSE)常被應用于開發(fā)大型軟件系統(tǒng),以提高軟件的可靠性。系統(tǒng)建模語言(Systems Modeling Language,SysML)是MBSE中使用的標準建模語言,它用于支持系統(tǒng)工程中需求分析、設(shè)計、編碼、測試等活動。SysML模型也常被應用于軟件的代碼設(shè)計。因此,SysML模型在是否準確地表達用戶的需求成為了軟件代碼是否具備高可靠性的關(guān)鍵。然而,很少有算法或者工具能夠以形式化的方式支持SysML模型的需求分析與驗證,特別是基于非基本結(jié)構(gòu)的SysML模型的驗證更是不多見。本文選取了具有描述系統(tǒng)動態(tài)行為能力的SysML活動圖模型作為研究對象,創(chuàng)新性地提出了一種基于測試用例的形式化驗證方法(Testing-Based Formal Verification for Model,TBFV-M)來檢驗SysML活動圖是否滿足用戶需求。本文的主要工作分為以下3個方面:(1)設(shè)計了基于SysML活動圖的測試用例生成算法。該算法改善了當前主流生成算法只能夠應用于結(jié)構(gòu)化的活動圖的局限性,將非基本結(jié)構(gòu)的活動圖進行轉(zhuǎn)化...

【文章頁數(shù)】：89 頁

【學位級別】：碩士

【部分圖文】：

圖1.1基于文檔的軟件工程與MBSE之間的對比

圖1.1基于文檔的軟件工程與MBSE之間的對比系統(tǒng)建模語言(SystemsModelingLanguage，SysML)是基于模型的系統(tǒng)工程的重要支柱之一。它可以為包含硬件、軟件、信息、過程、人員和設(shè)備等等的復雜系統(tǒng)進行系統(tǒng)建模[12][13]，是一種能夠表意豐富內(nèi)....

圖2.1SysML圖的分類SysML是在UML的基礎(chǔ)上提出的，重用了UML2.0的一個子集，也定義了

模語言SysML、霍爾邏輯、以及基于測試的形式化驗證方法TBFV。SysML可以為系統(tǒng)模型進行建模，本文選擇了SysML活動圖作為研究對象。TBFV-M方法以TBFV為基礎(chǔ)，其應用對象是SysML活動圖模型，并且最終使用霍爾邏輯進行需求的形式化驗證。系統(tǒng)建模語....

圖3.1活動圖節(jié)點圖示

第三章活動圖測試用例自動生成算法華東師范大學碩士學位論點�？刂乒�(jié)點有7種類型：起始節(jié)點(InitialNode)、活動終止節(jié)點(ActivityFinNode)、流終止節(jié)點(FlowFinalNode)、條件分支節(jié)點(DecisionNode)、合并節(jié)點(Mer....

圖3.2循環(huán)模塊的分類圖

圖3.2循環(huán)模塊的分類圖3.2.2并發(fā)模塊在SysML活動圖中，并發(fā)模塊最常見的組成方式是由一對fork節(jié)點和join節(jié)點，以及兩個節(jié)點之間的所有action構(gòu)成，如圖3.3(a)所示，本文稱其為簡單并發(fā)。fork節(jié)點表示的是多個并行活動同時開始，joi....

本文編號：3895847