基于SysML模型的需求分析与验证

发布时间：2024-02-04 21:00

　　基于模型的系统工程(Model-Based Systems Engineering,MBSE)常被应用于开发大型软件系统,以提高软件的可靠性。系统建模语言(Systems Modeling Language,SysML)是MBSE中使用的标准建模语言,它用于支持系统工程中需求分析、设计、编码、测试等活动。SysML模型也常被应用于软件的代码设计。因此,SysML模型在是否准确地表达用户的需求成为了软件代码是否具备高可靠性的关键。然而,很少有算法或者工具能够以形式化的方式支持SysML模型的需求分析与验证,特别是基于非基本结构的SysML模型的验证更是不多见。本文选取了具有描述系统动态行为能力的SysML活动图模型作为研究对象,创新性地提出了一种基于测试用例的形式化验证方法(Testing-Based Formal Verification for Model,TBFV-M)来检验SysML活动图是否满足用户需求。本文的主要工作分为以下3个方面:(1)设计了基于SysML活动图的测试用例生成算法。该算法改善了当前主流生成算法只能够应用于结构化的活动图的局限性,将非基本结构的活动图进行转化...

【文章页数】：89 页

【学位级别】：硕士

【部分图文】：

图1.1基于文档的软件工程与MBSE之间的对比

图1.1基于文档的软件工程与MBSE之间的对比系统建模语言(SystemsModelingLanguage，SysML)是基于模型的系统工程的重要支柱之一。它可以为包含硬件、软件、信息、过程、人员和设备等等的复杂系统进行系统建模[12][13]，是一种能够表意丰富内....

图2.1SysML图的分类SysML是在UML的基础上提出的，重用了UML2.0的一个子集，也定义了

模语言SysML、霍尔逻辑、以及基于测试的形式化验证方法TBFV。SysML可以为系统模型进行建模，本文选择了SysML活动图作为研究对象。TBFV-M方法以TBFV为基础，其应用对象是SysML活动图模型，并且最终使用霍尔逻辑进行需求的形式化验证。系统建模语....

图3.1活动图节点图示

第三章活动图测试用例自动生成算法华东师范大学硕士学位论点。控制节点有7种类型：起始节点(InitialNode)、活动终止节点(ActivityFinNode)、流终止节点(FlowFinalNode)、条件分支节点(DecisionNode)、合并节点(Mer....

图3.2循环模块的分类图

图3.2循环模块的分类图3.2.2并发模块在SysML活动图中，并发模块最常见的组成方式是由一对fork节点和join节点，以及两个节点之间的所有action构成，如图3.3(a)所示，本文称其为简单并发。fork节点表示的是多个并行活动同时开始，joi....

本文编号：3895847