SysML 建模工具的调研

基于SysML模型驱动的软件开发应用与研究的开题报告一、研究背景及意义SysML是一种基于UML的建模语言，主要支持系统工程领域的建模需求。

其模型可以表达系统的结构、行为和功能等，同时也能够建立与系统开发各个阶段的关联。

近年来随着信息技术的不断发展和应用，系统工程需要处理的问题也变得越来越复杂，使得传统的建模和开发方法已经无法满足工业和军事领域的需求。

因此，如何利用SysML模型驱动的方法来更快、更有效地将其应用于各种复杂系统的开发过程中，成为了当前研究的热点之一。

在现实生产环境中，大多数软件项目采用的是传统的开发方法，即软件开发过程中要求做好文档、源代码、测试数据等文档资料的维护。

这种方法的缺点是在大量的人力、财力、时间资源的投入下很难做到高效、及时、准确的需求分析、设计、开发和测试等工作。

而SysML模型驱动的开发方法则能够减少手动参与，通过自动生成文档，测序和源代码等，降低工作难度和开发过程的复杂性，提高开发效率和软件产品质量，从而能够在软件开发过程中，更快、更精确地实现需求沟通，开展各个阶段流程的自动化及标准化。

二、研究内容本研究计划通过对SysML模拟器的应用研究，深入探讨模型驱动的软件开发方法在实际项目中的应用及优势。

具体而言，其研究主要包括以下几个方面：1. SysML模型驱动方法的理论研究。

通过对模型驱动的方法、模型的构建及其表达语言，模型驱动软件开发的基本概念等进行研究，为后续开发实践提供理论支撑。

2. 基于SysML模型的案例分析。

选取实际的开发项目，将SysML建模工具与传统的软件开发方法进行比较，并分析其优缺点。

其中包括传统的水坝开发方法与基于SysML模型的积极开发方法在工程上的差异和影响。

3. 基于SysML的软件开发流程探索。

通过根据SysML建好的模型来自动生产代码、文档、测试数据等资源，进而实现对软件生命周期各个阶段的标准化流程的探索。

三、研究方法与步骤本研究采用的是实证研究方法，以SysML建模为工具，结合软件开发实践及计算机技术，对软件开发中基于SysML模型驱动方法的应用及其优势进行探究。

第44卷 第8期 包 装 工 程2023年4月 PACKAGING ENGINEERING37收稿日期：2022–11–13作者简介：张强（1997—），男，博士生，主要研究方向为基于模型的系统工程（MBSE ）、数字主线。

通信作者：刘继红（1966—），男，博士，教授，主要研究方向为复杂产品数字化设计与制造、知识工程与知识管理、智基于SysML 的多学科设计建模与优化张强，刘继红（北京航空航天大学 机械工程及自动化学院，北京 100191）摘要：目的 基于系统建模语言SysML ，分析多学科设计建模与优化过程，在理解多学科设计与优化数学模型的基础上，构建系统设计优化模型。

方法 通过分析多学科设计优化的数学模型，利用SysML 语言对多学科优化对象模型进行元模型表征，将生成的SysML 模型进行模型转化，转换成XML 格式以便优化求解器进行求解。

结论 提出了一种用于多学科设计建模与优化的SysML 扩展优化建模方法。

通过SysML 系统建模语言的扩展版型，添加多学科优化相关的优化目标、优化约束、优化变量等优化元素的模型内容。

提出了SysML 优化信息的提取方法，以XML 为中间格式，将提取的优化模型与优化求解器进行集成。

通过系统设计与系统优化的集成求解为产品系统架构设计人员提供有效的决策支撑。

关键词：基于模型的系统工程（MBSE ）；SysML ；多学科设计优化；优化模型构建 中图分类号：TB472 文献标识码：A 文章编号：1001-3563(2023)08-0037-11 DOI ：10.19554/ki.1001-3563.2023.08.004Modeling and Optimization of Multidisciplinary Design Based on SysMLZHANG Qiang , LIU Ji-hong(School of Mechanical Engineering & Automation-BUAA, Beijing 100191, China)ABSTRACT: The work aims to analyze the modeling and optimization process of multidisciplinary design based on sys-tem modeling language SysML, and build a design and optimization model of system based on the understanding the ma-thematical model of multidisciplinary design and optimization. By analyzing the mathematical model of multi-disciplinary design and optimization, the meta-model of multi-disciplinary optimization object model was characterized by SysML language, and the generated SysML model was transformed into XML format to be solved by the optimized solver. A SysML-extended optimization modeling method for multidisciplinary design modeling and optimization is put forward. Through the extended version of SysML system modeling language, model contents about optimization elements such as optimization objectives, optimization constraints and optimization variables related to multidisciplinary optimization are added. An extraction method of SysML optimization information is proposed. With XML as the intermediate format, the extracted optimization model is integrated with the optimization solver. The integrated solution of system design and system optimization provides effective decision support for product system architecture designers.KEY WORDS: model-based systems engineering (MBSE); SysML; multidisciplinary design and optimization; optimiza-tion model building随着科技水平的不断进步和经济的发展需求，工程系统的复杂性不断增大。

基于SysML的嵌入式软件系统建模与验证方法研究仵林博;陈小红;彭艳红;聂长海【摘要】嵌入式软件系统由于广泛采用分布式异构网络,使得软件系统复杂性呈现几何增长,因此需要在系统设计的论证阶段,对系统需求和设计方案进行正确性和充分性验证,进而发现系统性设计缺陷,避免可能引发或导致的严重系统性问题.为此,提出一种基于SysML的嵌入式软件系统结构与行为需求建模方法.通过对嵌入式软件系统的结构和逻辑行为进行层次化建模,并利用Modelica离散与连续融合的仿真特点,在系统需求论证阶段,基于建立的仿真模型对系统关键功能指标进行仿真,结果表明,该方法对系统需求论证具有可行性.【期刊名称】《计算机工程》【年(卷),期】2019(045)001【总页数】8页(P1-8)【关键词】SysML模型;系统建模;Modelica仿真;系统结构;嵌入式系统【作者】仵林博;陈小红;彭艳红;聂长海【作者单位】中国工程物理研究院计算机应用研究所,四川绵阳621999;华东师范大学计算机科学与软件工程学院,上海200062;中国工程物理研究院计算机应用研究所,四川绵阳621999;南京大学计算机科学与技术系,南京210023【正文语种】中文【中图分类】TP3910 概述随着网络和通信技术的快速发展,嵌入式系统从以单片微处理器为核心的简单嵌入式系统,逐渐发展成为通过外部总线、高速或低速网络连接起来的分布式系统[1],该系统称为网络化嵌入式软件系统。

与传统的软件系统相比,网络化嵌入式软件系统通常由很多节点组成,采用分布式网络互联,有些系统甚至内嵌在一个更大的系统中,形成规模更加庞大的网络结构。

随着系统规模的增加,系统交互复杂度越来越高,系统设计时不仅考虑内部节点之间存在各种交互行为,还要通过接口与周围环境中的节点进行交互通信,特别是不同节点的并发行为,这些行为之间需要同步完成特定功能。

从上述特点可以看出,网络化嵌入式软件系统在系统设计前期,即需求论证阶段,缺乏一套系统的建模与验证方法,需通过对嵌入式软件系统进行建模来验证系统功能正确性和业务逻辑一致性。

收稿日期:2018-11-25 修回日期:2019-03-26 网络出版时间:2019-06-26基金项目:国家自然科学基金(617722770);南京航空航天大学开放基金(kfjj 20171606)作者简介:邓刘梦(1995-),男,硕士研究生,CCF 会员(88983G ),研究方向为软件安全㊁嵌入式系统建模与分析㊁需求可追踪性㊂网络出版地址:http :// /kcms /detail /61.1450.TP.20190626.0829.038.html基于NuSMV 的SysML 模型形式化验证邓刘梦,葛晓瑜,宛伟健(南京航空航天大学计算机科学与技术学院,江苏南京211106)摘　要:航空航天道路交通等高安全领域的系统开发需要保证高安全㊁高可靠,对于该类系统的合理建模以及模型验证则尤为重要㊂当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制开发时间和成本,并降低系统出现风险的可能性㊂但与此同时,需求与设计模型之间仍然存在着沟壑,设计模型是否很好地满足用户所提出的需求在完成系统设计后仍需验证㊂针对系统建模语言缺乏精确形式化语义难以进行模型验证的问题,文中给出一套从SysML 设计模型到NuSMV 模型转换的语义规则,实现了一个自动转换程序,将SysML 模型文件转换成NuSMV 输入文件,进而利用NuSMV 实现SysML 模型的验证㊂最后通过一个铁路控制系统的案例证明了该方法的有效性㊂关键词:需求工程;模型转换;形式化验证;模型驱动开发中图分类号:TP311 文献标识码:A 文章编号:1673-629X (2019)10-0153-04doi:10.3969/j.issn.1673-629X.2019.10.030Formal Verification of SysML Model Based on NuSMVDENG Liu -meng ,GE Xiao -yu ,WAN Wei -jian(School of Computer Science and Technology ,Nanjing University of Aeronautics and Astronautics ,Nanjing 211106,China )Abstract :System development in aerospace road traffic and other high security areas needs to ensure high security and high reliability.It is especially important for the reasonable modeling and model verification of such systems.The model driven development (MDD )method has been widely used in the development of safety -critical systems ,which supports the safety analysis and verification of the system at an early stage ,effectively controlling development time and cost and reducing the possibility of system risk.At the same time ,there is still a gap between the textual requirement and the design model.Whether the design model can well meet the user ’s requirements still needs to be verified after the completion of the system design.Addressing the problem of the lack of precise formal se⁃mantics for the systems modeling language (SysML ),a set of semantic rules for the transformation from SysML design model to NuSMV model is given.An automatic conversion program is implemented to convert the SysML model file into NuSMV input file ,and then to verify the SysML model by NuSMV.In the end ,we prove the effectiveness of this method through the case of railway control system.Key words :requirement engineering ;model transformation ;formal verification ;model driven development0　引　言在过去多年,软件开发面临了多个挑战,新的需求和存在系统不断增长,系统也变得越来越复杂,以至于很难及时地对它们进行构建㊂为了解决这些问题,出现了很多新的方法,其中最突出的一个就是模型驱动开发㊂模型驱动开发代表了一套理论和工业化软件开发的方法框架,在软件开发全生命周期中系统的使用模型作为主要工件,主要是为了解决软件的两个根本危机:复杂性和变更能力㊂但与此同时,模型驱动开发也带来了一些问题:使用自然语言描述的需求与严格定义的模型之间的鸿沟无法很好地连通[1]㊂此外,对于SysML 描述的图形化模型,目前缺乏严格有效的分析和验证方法㊂针对以上存在的问题,文中给出了从SysML 模型到NuSMV 输入模型的转换规则,并实现自动化程序完成这一转换㊂接着利用NuSMV 模型检测的方法来验证SysML 模型的正确性㊂第29卷　第10期2019年10月 计算机技术与发展COMPUTER TECHNOLOGY AND DEVELOPMENT Vol.29　No.10Oct.　20191　SysML系统建模SysML是目前业界常用的系统体系结构建模语言,可用于由软硬件㊁数据和人综合而成的复杂系统的分析与设计㊂然而,为了保证一定的易读性,SysML 采用半形式化的描述方法来定义语义,使用自然语言描述约束和详细语义,力求在形式严格和易于理解间找到平衡[2]㊂在实际中,其图形化的建模方式十分简洁直观,关系链接与约束描述等方式也进一步缩小了模型驱动开发过程中需求描述与模型设计制品间的沟壑㊂但是,其牺牲的部分就是缺乏精确的语义,难以进行严格的语义分析以及正确性验证㊂SysML是一种图形化建模语言,是对象管理组织(object management group,OMG)在对UML2.0的子集进行重用和扩展的基础上提出的一种新建模语言[3]㊂它为软件体系结构建模提供了丰富的图标,涵盖了从系统需求到设计阶段的各项要求,广泛应用于航空航天软件开发过程㊂它致力于建模具有众多组件㊁难以描述㊁理解㊁预测㊁管理㊁设计以及更改的系统,并提供了表达个人需求及其组成的手段,已被学术界和工业界所广为接受,作为一种标准建模语言[4]㊂SysML为系统的结构模型㊁行为模型㊁需求模型和参数模型定义了语义㊂结构模型强调系统的层次以及对象之间的相互连接关系,包括类和装配㊂行为模型强调系统中对象的行为,包括它们的活动㊁交互和状态历史[5]㊂文中主要使用SysML的块定义图对系统的静态结构进行描述,使用状态机图对系统的动态迁移进行描述㊂SysML中,块(block)是系统描述的最小建模单位,可以用来描述每一个单独的组件,同时也是描述系统结构特征和行为特征的单元㊂SysML块以UML类图为基础,并扩展了UML复合结构的一些特征[6]㊂块定义图(block definition diagram)则是用于描述块信息的图㊂它描述了块的属性值㊁块的组成部分㊁块的操作以及对其他块的参考等[7]㊂而状态机图(state machine diagram)则是用来描述系统的状态迁移情况[8]㊂其中状态转移用来描述对象对事件的响应情况㊂关于SysML块定义图以及状态机图的实例将在下一节给出㊂2　NuSMV模型针对SysML模型进行验证,采用NuSMV作为验证工具㊂2.1　输入语言分析NuSMV模型中,系统被描述为模块化的层次结构,支持定义组件的重用[9]㊂其支持的数据类型主要有枚举类型㊁布尔类型和固定数组等㊂基本上,一个完整的NuSMV模型文件主要由两部分组成:系统模型和待验证的系统性质[10-11]㊂NuSMV系统模型部分主要用于描述系统的状态以及状态迁移关系,刻画出系统的静态结构与动态行为[12]㊂通过关键字MODULE来定义模块,通常每一个模块对应一个系统组件[13]㊂通过主模块中的SPEC 字段进行待验证需求性质描述,同时支持计算树逻辑(computation tree logic,CTL)和线性时序逻辑(linear-time temporal,LTL)的表达式[14-15]㊂2.2　SysML模型到NuSMV模型的转换本节根据SysML模型与NuSMV模型的特点[16],给出转化规则,并实现工具完成NuSMV模型实例的自动化生成㊂首先对SysML中的静态图进行转换,文中主要使用的是块定义图㊂规则1:模块名声明㊂描述:对于NuSMV中的模块名根据块定义图中的名称进行命名㊂规则2:静态变量声明㊂描述:对于块定义图中定义的属性都须在相应的模块中通过VAR关键字进行声明㊂规则3:变量初值㊂描述:对于块定义图中所有属性的初值都须在相应的模块中通过ASSIGN关键字进行声明㊂接下来对SysML中的动态行为模型进行转换㊂SysML中主要通过状态机图对系统的状态迁移进行刻画,系统中可能出现的状态迁移,都存在对应的状态机图[12]㊂从另一个侧面来看,状态图也可以理解为对块定义图动态的补充,故在转换中,应将其放入相应的模块中,而不是重新声明模块㊂规则4:状态机图声明㊂描述:对于状态机图转换不重新进行模块声明,将其状态迁移关系通过TRANS㊁next等关键字描述加入到从属的块定义图对应的模块中㊂例如:Car对应的状态机图,其描述的状态迁移关系都应该加入到MODULE car中㊂规则5:状态变量声明㊂描述:如果一个块定义图存在一个对应的状态机图,则应该在此块对应的模块中通过VAR声明一个state变量㊂规则6:状态变量赋值㊂描述:状态机图中state的取值是由去除初始状态和结束状态后所有状态值构成的枚举集合,其初始值应为状态机图中Initial节点指向的第一个状态,通过ASSGIN声明㊂例如:对于汽车car,通过一个状态机图描述其运㊃451㊃ 计算机技术与发展 第29卷行状态可能存在运行或者停止两种状态(见图1),那么MODULE car 中VAR 字段就需加入car _state :{stop ,running }声明,初始状态为stop ,通过ASSGIN init (car _state ):=stop 字段进行声明㊂图1　汽车运行状态机图实例规则7:状态迁移㊂描述:状态机图确定的状态转变使用next 进行描述,并通过case 来表达分支情况㊂例如:car _state 当前状态为stop 下一状态为running 和当前状态为running 下一状态为stop 表示如下:next (car _state ):=casecar _state =stop :{running };car _state =running :{stop };esac规则8:状态迁移条件㊂描述:如果状态机图中的状态迁移存在迁移条件,则需将该守卫条件加入到迁移描述字段中(见图2)㊂例如:在汽车启动前应确定车门是关闭的,否则无法启动㊂next (car _state ):=car _state =stop&door.closed =1:{running };图2　存在守卫条件的状态迁移实例3摇实验与案例分析根据前几节的理论分析,实现了一个SysML 模型到NuSMV 模型自动转换的工具㊂下面通过案例演示㊂案例的场景如下:在铁路控制系统中,在火车通过路口时需要关闭公路两侧的栅栏,保证在火车通过的过程中汽车无法驶入路口,避免发生火车汽车相撞的事故㊂首先通过SysML 建模工具建立该场景的模型如下:图3　铁路案例SysML 块定义图图3中块定义图描述了系统的静态结构信息,图4㊂图4　铁路案例SysML 状态机图在建模分别得到块定义图和状态机图后,利用工具将模型导出为XMI 文件格式以供后续转换使用㊂接着将得到的SysML 模型文件输入到自动转换工具中即可完成转换,得到铁路系统的SMV 文件(见图5)㊂图5　SysML 模型转换工具界面㊃551㊃　第10期 邓刘梦等:基于NuSMV 的SysML 模型形式化验证得到设计模型的实例后,即可利用已有的NuSMV 工具来检测系统需求是否被设计模型所实现㊂首先给出一条安全需求:该系统模型不得出现汽车和火车同时驶入路口的情况,避免事故发生㊂接着在得到的SMV 文件中写入该需求性质LTL 表达式:LTLSPEC G !((Car _state =Car _in )&(Train _state =Train _in ))㊂最后在Windows 10下采用命令行形式运行NuSMV 工具检测该SMV 文件得到的结果如图6所示㊂图6　需求验证结果得到LTL 公式检测结果为false ,即该需求没有被满足㊂NuSMV 工具给出了反例,观察到在1.5状态时同时出现了汽车和火车均进入路口的情况㊂同时表明文中转换工具得到的SMV 文件可以很好地作为NuSMV 工具的输入,证明了该方法的有效性㊂4摇结束语针对SysML 模型缺乏精确语义而难以进行模型正确性验证的问题,给出了一个通过模型转换技术实现模型验证的解决方法㊂实现了一个从SysML 设计模型到NuSMV 模型自动转换的工具,最后利用转换得到的SMV 文件作为模型检测器的输入即可进行SysML 模型的验证㊂参考文献:[1]　刘军霞,熊选东,王松锋.基于随机Petri 网的SysML 状态 机图的验证[J ].计算机应用与软件,2013,30(6):202-208.[2]　夏　宇.基于NuSMV 和STPA 的RBC 交接场景安全分析方法研究[D ].北京:北京交通大学,2018.[3]　SALMAN Y D ,HASHIM N L.Automatic test case genera⁃tion from UML state chart diagram :a survey [M ]//Ad⁃vanced computer and communication engineering technology [s.l.]:Springer International Publishing ,2016:123-134.[4]　FRIEDENTHAL S ,MOORE A ,STEINER R.A practicalguide to sysML [M ].[s.l.]:[s.n.],2011:41-46.[5]　曹德建,黄志球,阚双龙,等.基于故障扩展SysML 活动图的软件安全性分析方法研究[J ].小型微型计算机系统,2015,36(9):2067-2074.[6]　王　栋.基于SysML 的武器装备体系结构建模与仿真方法研究[D ].长沙:国防科学技术大学,2009.[7]　NEJATI S ,SABETZADEH M ,ARORA C ,et al.Automatedchange impact analysis between SysML models of require⁃ments and design [C ]//Proceedings of the 24th international symposium on foundations of software engineering.Seattle ,WA ,USA :ACM ,2016:242-253.[8]　ANDRADE E ,MACIEL P ,CALLOU G ,et al.A methodolo⁃gy for mapping SysML activity diagram to time petri net for requirement validation of embedded real -time systems with energy constraints [C ]//International conference on digital society.Cancun ,Mexico :IEEE ,2009:266-271.[9]　CIMATTI A ,CLARKE E ,GIUNCHIGLIA F ,et al.NUS⁃MV :a new symbolic model checker [J ].International Journal on Software Tools for Technology Transfer ,2000,2(4):410-425.[10]ARCAINI P ,GARGANTINI A ,RICCOBENE E.Asmeta⁃SMV :a way to link high -level ASM models to low -level NuSMV specifications [C ]//Proceedings of the second inter⁃national conference on abstract state machines ,alloy ,B and Z.Orford ,QC ,Canada :Springer -Verlag ,2010:61-74.[11]陈冬火,刘　全.基于符号执行和LTL 公式重写的测试用例产生方法[J ].计算机研究与发展,2013,50(12):2661-2675.[12]周玉平.基于UML -NuSMV 模型的列控系统需求阶段的安全分析[D ].北京:北京交通大学,2015.[13]何　洋,洪　玫,祁琳莹,等.基于模型检测工具NuSMV的功能测试用例生成方法[J ].计算机应用,2015,26(z 2):155-159.[14]王　曦,徐中伟,梅　萌.基于模型检测的软件安全性验证方法[J ].武汉大学学报:理学版,2010,56(2):156-160.[15]KAN Shuanglong ,HUANG Zhiqiu.Detecting safety -relatedcomponents in statecharts through traceability and model sli⁃cing [J ].Software :Practice and Experience ,2017,48(2):428-448.[16]俞晓锋,王立松.SysML 状态图合理性验证研究与实现[J ].电子科技,2014,27(5):127-131.㊃651㊃ 计算机技术与发展 第29卷。

基于SysML的模型驱动武器装备体系结构设计与分析陆法;孙文虎;贾鹏【摘要】随着武器装备体系规模、复杂度的不断膨胀,模型驱动的体系结构设计方法成为解决复杂系统开发的研究热点.选择SysML(Systems Modeling Language)作为建模语言,提出了一种由三个基本步骤(能力需求分析、黑盒分析和白盒分析)组成的模型驱动体系设计方法, 探索了 SysML在体系层面建模的应用,并针对当前SysML建模工具在仿真可视化与系统分析等能力上的不足,将建模工具与仿真分析工具进行集成,共同完成武器装备体系结构的设计与仿真分析.%With increase of scale and complexity of Weapon System-of-Systems, model driven architecture design method has become a research hotspot of complex system development.This paper uses systems modeling language (SysML) and proposes a model driven architecture design method composed of capability requirement analysis, black-box analysis and white-box analysis.The application of SysML in architecture modeling is presented.Because the SysML tool is insufficient in simulation visualization and system analysis, the modeling tool is integrated with the simulation analysis tool in design and simulation analysis of weapon equipment architecture.【期刊名称】《指挥控制与仿真》【年(卷),期】2017(039)001【总页数】5页(P44-47,56)【关键词】基于模型的系统工程;武器装备体系结构;模型驱动方法;SysML【作者】陆法;孙文虎;贾鹏【作者单位】解放军后勤学院,北京 100858;解放军后勤学院,北京 100858;解放军后勤学院,北京 100858【正文语种】中文【中图分类】E917武器装备体系结构描述了武器装备体系组件的结构、组件之间的关系以及约束它们设计和发展进的原则和指导方针[1]。