一、面向模型检验的UML状态机语义（论文文献综述）
肖伟[1]（2021）在《自主化CTCS-3级列控系统新增场景建模及安全分析》文中指出自主化CTCS-3级列控系统在确保高铁列车的安全运行方面起着至关重要的作用,有完全的自主产权,在软硬件设计以及功能需求上都新增了许多内容。因此,如何确保列控系统在新增规范要求下的安全性和可靠性就成为了重要的研究课题。同时对采用何种方法对列控系统安全因素进行分析在传统研究中并没有涉及,而形式化方法恰好弥补了这一不足,通过选取合适的形式化方法对列控系统进行建模及安全分析已成为目前列控系统安全保障技术的主流研究趋势。本论文以自主化CTCS-3级列控系统轨道电路行车许可校验场景为研究对象,采用两种形式化方法对场景开展研究。首先提出基于时间自动机的建模方法,针对列控系统的实时性,分析场景下列控系统各设备的工作流程,经过合理的抽象简化后,利用时间自动机理论构建了轨道电路行车许可校验场景的时间自动机模型,在UPPAAL模拟器中对各模块交互情况进行仿真,使用验证器验证其安全功能属性和受限活性,证明了此建模方式的有效性,最后结合京沈客专辽宁段试验数据,编制轨道电路行车许可校验场景相关的测试序列,通过自主化CTCS-3级列控系统场景控制器开展仿真测试验证。同时利用UML（Unified Modeling Language,统一建模语言）扩展机制进行轨道电路行车许可校验场景安全分析。针对列控系统的混成性,对轨道电路行车许可校验场景进行分析,根据UML扩展机制对于建模的要求,前期包含UML场景类图以及状态转移图模型构建,对于系统中的状态迁移部分和动态连续过程结合故障扩展模型进一步描述其行为,在列控系统规范要求的基础上建立混成性概要描述文件,后期将已经建立好的模型利用混成自动机模型检验工具进行转换,分析轨道电路行车许可校验场景中可能出现的故障并进行描述,采用故障模型融合算法将PHAVer模型和故障模型融合来描述轨道电路行车许可校验场景中的故障情形和因为故障造成的场景功能影响,利用故障检测器对系统模型开始进行可达集计算,确定涉及系统安全的故障因素组合实现轨道电路行车许可校验场景的安全分析。结果表明,本文提出的方法可以满足轨道电路行车许可校验场景在列控系统需求设计阶段的安全特性要求,为以后列控系统的形式化建模与安全评估提供了参考方法。
王媛[2]（2021）在《面向UML的模型检测方法研究》文中研究表明随着计算机技术的飞速发展,无论是软件系统还是硬件系统都变得越来越庞大而且复杂,保障这些系统的正确性就变成了人们必须正视的问题。在一些对安全需求比较高的领域里,更是需要对系统的安全性进行保证,因此保证系统安全性的方法也就成为了现在研究的热门内容。形式化验证是一种可以提高系统安全性的有用方法,而模型检测是形式化验证的一种主要技术。UML是一种面向对象系统所用的建模语言。它对建立模型所需要的一些元素进行了定义,可以利用多个视图的结合从不同的角度全面分析建模一个系统。然而UML只是一个半形式化的建模语言,并不能对系统的安全属性进行自动分析和验证。为了弥补上述不足,则需要形式化的验证工具对建模后的系统进行验证。本文使用形式化的方法以车身电子稳定系统为实例来对UML模型进行模型检测验证。所做的主要工作内容如下:（1）使用UML来对待检测的系统建模,再将UML图例输出为可扩展的XML文件。（2）通过分析了UML的语义和SMV的语义定义了将UML图例转换为SMV语言的规则。（3）在C#环境下设计代码来实现转换将XML文件转出SMV文件。（4）使用Nu SMV来对转换出的SMV文件进行验证工作。
周游[3]（2020）在《基于UML扩展机制的RBC控车场景功能安全分析方法》文中研究指明随着我国高速铁路技术的发展及对高速铁路管理规章制度的出台,我国对CTCS-3（China Train Control System level 3,中国列车运行控制系统）级列控系统的需求规范也逐渐完善。RBC（Radio Block Center,无线闭塞中心）作为CTCS-3级列控系统地面核心子系统用来保障列控系统的安全运营。CTCS-3级列控系统是同时具备了连续和离散的信息交互机制的混成系统,在RBC与其他设备进行交互时如果出现任何与行车许可、线路信息等相关的问题都可能影响高速列车的正常运行,因此需要对RBC控车场景进行安全分析来保证后续的系统安全设计和评估,而基于传统的安全保障技术在列控系统的安全分析中已略显其不足,通过形式化方法对列控系统进行安全分析已经成了研究的主要趋势。本文以CTCS-3级列车运行控制系统中RBC控车场景为研究对象,提出基于UML（Unified Modeling Language,统一建模语言）扩展机制的控车场景功能安全分析方法。首先,针对CTCS-3级列控系统的混成特性,采用面向对象的方法对RBC控车场景进行分析,根据UML扩展机制的安全特性建模方法,构建UML类图和状态转移图模型以及其故障扩展模型来描述系统的状态迁移和连续动态过程,再根据列控系统的需求规范构建具有安全特性的混成概要文件来准确地刻画列控系统的混成特性。然后,选择CPN（Colored Petri Net,有色Petri网）作为UML扩展模型的验证工具及分层控制结构的形式化建模规范,将扩展的UML模型转换成可执行的有色Petri网分层模型,通过ASK-TCL算法对系统模型进行动态行为和状态变化的检验,验证UML扩展模型和RBC控车场景的正确性和一致性。最后,根据已建立的UML扩展模型转化成PHAVer（Polyhedral Hybrid Automaton Verifier,混成自动机模型检验工具）模型,分析RBC控车场景中可能出现的故障并进行描述,将PHAVer和故障模型融合来描述RBC控车场景中设备故障情况以及故障对场景功能产生的影响,利用故障监视器对系统模型进行可达集计算,确定危及系统安全的故障组合实现RBC控车场景的安全分析。结果表明,本文提出的方法可以满足RBC控车场景在需求设计阶段的安全特性要求,为以后列控系统的形式化建模与安全评估提供了参考方法。
马燕燕[4]（2020）在《面向安全关键系统的SysML模型向AADL模型转换方法研究》文中指出安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。近年来,模型驱动开发方法逐渐成为安全关键系统设计与开发的重要手段。由于还没有一个建模语言能够支持整个安全关键系统开发生命周期,因此本文选择集成使用两种广泛使用的标准语言:系统建模语言（SysML）和嵌入式实时系统体系结构分析与设计语言（AADL）。SysML和AADL提供了同一系统的两个不同视图,SysML模型为系统工程师提供一个系统视图,AADL为架构设计师建立一个较低层次的设计视图,它结合了实现所有功能的软件、操作系统和硬件。同时根据ARP4761安全性评估标准,安全关键系统在设计时需评估每个阶段的设计是否符合安全性的需求,目前SysML对于安全性分析的支持比较不足,欠缺安全性相关信息的描述能力。本文提出面向安全关键系统的SysML模型向AADL模型转换方法,重点研究了在安全关键领域SysML对安全性信息描述能力不足的问题以及集成使用SysML和AADL语言时,SysML向AADL模型自动转换等关键问题。主要研究成果如下:首先,提出一种SysML安全性扩展及分析方法,通过定义失效概要文件Failure Profile,描述安全性相关概念,在SysML标准系统模型的基础上,Failure Profile对系统的故障信息建模,在系统设计信息和安全信息之间进行有效链接。并且提出Failure Profile到故障树的自动生成方法,设计了故障树的自动生成算法,支持用现有的故障树分析工具分析,将分析结果反馈到SysML设计模型中,尽早发现设计中潜在的风险,提高安全性分析的效率。其次,提出一种SysML和AADL集成使用的建模方法,使用SysML在系统概要设计阶段建模,AADL在系统详细设计阶段建模,给出SysML模型到AADL初始设计模型的自动转换方法,包括SysML核心子集和扩展的Failure Profile的元模型到AADL子集元模型的语义映射以及相关的转换算法,系统功能和故障信息传递到AADL模型中,减少手工建模传递设计信息的语义缺失和工作量较大的问题,并且使用AADL错误附件可以做进一步的安全性分析。最后,在集成了SysML建模工具Papyrus和AADL建模工具OSATE的Eclipse平台上设计并实现了SysML到AADL的模型转换原型工具SysML2AADL,工业界案例飞机空气增压系统案例验证了本文所提方法的有效性。
陈杨杨[5]（2020）在《用例图和顺序图的一致性研究》文中研究指明在软件开发过程中,需求分析和设计是整个软件开发过程的关键阶段,为了保证需求分析和设计的正确性,需要一些模型语言对用户需求和系统设计进行建模。统一建模语言（UML）是一种适用于软件系统开发的图形化语言,功能强大且易于表达,其中用例图和顺序图被广泛用于在需求分析和设计阶段的建模。用例图由事件流、执行者等构成,事件流描述了用户要求系统执行过程的功能行为,是用户需求的具体描述。一个完整的系统的用例图复杂且庞大,将一个个用例自动分解成用例切片,每个用例切片由多个用例故事组成,更易于分析和理解。顺序图是设计阶段具有代表性的模型,它是用例驱动开发过程中用例的实现图,为了系统设计满足用户的需求,必须保证用例图和顺序图的一致性。为了检验顺序图和用例图的一致性,传统的一致性检验方法直接检查两个模型的一致性。本文提出了一种新的方法来检验顺序图和用例图一致性,该方法是通过检验顺序图的子图与用例切片的一致性来判断顺序图和用例图的一致性。首先讨论了模型一致性检验基本原理,并提出了模型间一致性检验的新方法,即通过检验一个模型的子模型与另一个模型的子模型的一致性来判断这两个模型的一致性;其次,研究了将用例图中的用例自动分解成用例切片的方法;接着,讨论了将顺序图分解成子顺序图,每个子顺序图应该是一个完整的用例故事的实现;最后,检验每个顺序图的子图是否与相应的用例故事一致。这个方法是利用两个模型的对应的子模型之间的一致性来判断这两个模型之间的一致性。本文从理论上证明了这个方法的正确性,并且用实例演示了顺序图和用例图一致性的具体检验过程。
姜懿芮[6]（2019）在《日光温室蔬菜系统的UML建模与一致性检测》文中研究说明以物联网、大数据应用为代表的信息技术在新型农业中得到广泛应用,促进了农业生产方式的转变。在新型农业中,日光温室蔬菜系统利用传感器技术收集农业信息,准确捕捉各种环境参数,帮助生产者及时检测蔬菜生长环境,通过日光温室为蔬菜生长发育提供良好的环境条件。日光温室蔬菜系统中构建的各种智能化模型需要合理的管理和操作,因此对日光温室蔬菜系统建立UML模型和对UML模型一致性检测,有较大的研究价值和应用前景。本文主要针对日光温室蔬菜系统的UML建模和模型检测的关键问题进行深入研究。具体研究工作成果如下:本文首先分析日光温室蔬菜系统的需求,研究UML建模和模型检测的现状和发展趋势,阐述UML模型建模的方式和一致性检测的类型,总结UML常用的建模工具。设计系统模块组成和各模块的子系统,并对子系统进行UML建模。针对UML模型一致性检测方法的实用性差和检测范围低等不足,提出基于抽象规则的UML模型一致性检测的方法,识别UML类图中类之间的关系、类的属性和操作,检测类图中类之间各种关系问题。针对UML模型存在信息冗余问题,本文将UML模型转换为知识图谱,提出基于知识图谱的UML模型一致性性检测方法,利用知识图谱实现对UML模型的检测。该方法首先构建知识图谱的架构,然后将UML模型和知识图谱对应,将UML模型转换为知识图谱,最后通过遍历知识图谱中的节点,计算不同类之间的相关性,消除UML模型中的冗余。理论分析和实验验证表明,本文提出的基于抽象规则的UML模型检测的方法,能准确识别UML模型中存在的不一致问题,具有较高的检测效率。同时,本文提出的基于知识图谱的UML模型一致性性检测方法,能有效地检测UML模型一致性,提高模型检测的效率。
李宛倩[7]（2019）在《面向SysML的模型转换与安全性分析方法研究》文中认为近十年来随着基于计算机的系统应用的深入和功能的增强,航空、医疗、交通运输等若干安全关键领域规模越来越大,涉及到的系统设计与分析问题也越来越复杂,如何深入研究复杂系统建模以及安全性分析问题已经成为学术界和工业界共同关注的重点课题。SysML作为一门广泛应用于国内外航空航天领域的通用图形化建模语言,主要用于对复杂系统进行功能及性能的设计,但是SysML没有明确提供对系统故障和失效进行建模的符号和语义,因而如何对以SysML为典型的系统模型进行安全性分析验证是一个非常重要的问题。AltaRica作为一门基于模型的安全性分析建模语言,主要用于描述和分析复杂的多层次系统架构和故障及失效行为信息,在当前航空工业界应用较为广泛,因而建立起SysML架构设计模型和安全性分析模型之间的桥梁可以有效保证安全性分析与系统设计的同步展开,有利于提高系统安全性分析效率。本文的工作主要是围绕基于模型的安全性分析（MBSA）方法展开,具体工作包括如下几个方面:（1）设计了基于模型转换的SysML安全性分析与验证框架。该框架基于SysML和AltaRica各自的特点以及当前面临的复杂系统设计建模安全性的挑战,给出了从SysML设计模型至安全性分析验证过程的逻辑框架图与数据处理流程图,并详细分析了SysML图模型及AltaRica3.0模型的组成要素。（2）构建从SysML架构模型的核心模型元素到最新系统安全性建模语言AltaRica3.0的语义等价的转换规则并分析其正确性。首先分析了SysML和AltaRica3.0建模的模型特点,构造了SysML模型元素和AltaRica3.0模型元素之间的映射规则,包括核心的转换规则及如何扩展SysML故障的相关语法语义,然后给出转换规则的形式化描述并分析证明转换规则的正确性。（3）基于模型驱动的方法设计一个原型工具SafetyTool来完成模型的自动转换和系统安全性分析。原型工具集成了转换、编译、生成故障树、故障树分析、单步仿真及故障路径动态演示的功能,能够自动化的解析SysML的XMI模型,提取出所需要的模型元素,再根据AltaRica语法自动转换为AltaRica3.0模型文件,然后对所构造的AltaRica3.0模型进行安全性分析。（4）以SAE AIR6110标准中民机的机轮刹车系统实例来展示方法和工具。包括根据AIR6110文档标准和安全性需求建立机轮刹车系统的SysML模型,使用SafetyTool实现两种建模语言的转换,基于AltaRica3.0模型构建故障树,利用相关工具对系统进行安全性分析,分析故障传播路径并动态演示,最后对机轮刹车系统进行安全性属性验证。
邓刘梦[8]（2019）在《基于SysML的安全性需求追踪及验证方法研究》文中进行了进一步梳理安全关键系统广泛应用于各种行业领域,例如国家的航空航天项目以及近年来迅速发展的无人驾驶、智慧医疗等领域。该类系统对安全性有着极高要求,一旦出现系统失效即可能造成重大的生命财产损失,因此,如何保障该类系统的安全性一直是学术界以及工业界的重要议题。安全性需求描述了系统不应发生的危险状态,来源于系统的早期危害分析以及后续的安全性分析迭代,尽早对其验证可以有效提高系统安全性。然而,在实际的系统开发过程中,系统设计模型基于功能需求进行开发,这导致了安全性需求与系统设计之间存在沟壑,使得设计模型是否满足安全性需求难以验证,系统的安全性难以得到有效的保障。针对以上问题,本文提出了一种基于SysML面向安全关键系统的安全性需求追踪及验证方法。本文主要研究内容如下:首先,参照相关安全标准,提出一个面向安全关键系统的追踪信息模型用于指导建模中追踪信息的捕获;接着,针对标准SysML需求图缺乏描述安全性需求能力,本文对SysML需求图进行了扩展,使其可以建模安全性需求并捕获追踪信息;此外,针对SysML需求图缺乏安全性需求追踪信息的导出机制,文中通过模型转换将需求图转换到追踪信息表达模型,生成独立的追踪信息文档,为后续安全性验证提供直接支持。其次,利用追踪信息定位SysML设计模型中用于实现安全性需求的SysML块以及块中元素,根据定位到的安全关键SysML设计给出算法构建面向验证的SysML块定义图进行安全性验证;但由于SysML模型缺乏精确语义,难以直接进行验证,故而本文中接着给出了从SysML模型转换到NuSMV形式化模型的规则,将SysML块定义图和状态机图转换到可验证的NuSMV系统模型,通过模型检测器验证安全性需求满足情况。最后,使用本文的方法对一个铁路控制系统进行案例分析。通过验证发现了系统设计中存在的缺陷,有效识别了潜在风险,同时也说明了本文方法的有效性。本文方法提供了一种安全关键系统中可追踪性建立以及利用追踪信息在系统开发早期定位系统安全关键组件并验证安全性的可行思路。
许金淼[9]（2019）在《面向功能行为层次化建模的AADL行为附件扩展及验证方法》文中指出AADL（Architecture Analysis and Design Language）是一种用于描述复杂嵌入式系统体系架构的建模语言国际标准,被广泛用于安全关键系统的建模与验证。AADL通过系统、子系统、进程、线程等组件层次化地表达系统模型。行为附件（Behavior Annex）是AADL在功能行为方面的补充,它通过扁平状态机的形式对组件的内部功能行为以及组件和组件间的交互行为建模。工业界中的复杂系统常使用层次状态机描述组件的功能行为。但是,行为附件中没有表达层次状态机的机制,虽然可以利用AADL自身的分层描述能力对系统建模,但会导致线程的规模过于庞大。在实际的开发过程中,设计者们往往需要将层次化描述的功能需求进行手动扁平化处理,然后借助AADL行为附件对其建模,这个过程是繁琐的且易错的,并且扁平化的状态机会造成结构信息的丢失,无法直观的表示功能行为模块的包含层次关系。针对AADL行为附件不能以层次化的形式建模功能行为这一问题,本文提出了一种基于AADL行为附件的功能行为层次化建模及验证方法,包括基于扩展的AADL层次行为附件建模方法和层次行为附件的形式化验证方法两部分。为了适应工业界的实际建模需求,本文首先提出了AADL行为附件的层次化扩展——层次行为附件HBA,给出了HBA的形式语法,定义了HBA的操作语义,提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了对所建模型进行形式化验证,本文提出了层次行为附件的形式化验证方法。首先通过层次行为附件扁平化方法将层次行为模型转化为多个相关联的扁平状态机,然后通过层次行为附件到时间自动机的转换方法将层次行为模型转换为时间自动机网络,最后人工抽取与被验模型相关属性,并将待验证模型与待验证属性输入到UPPAAL中,对所建模型进行验证。最后,通过一个航天器导航、制导与控制系统案例来验证本文所提方法的有效性。首先通过详细描述建模过程、逐步精化原始需求的方式,检验本文所提建模方法是否适用于建模实际工业案例;然后通过在原始需求中预埋错误的方式,检验本文所提出的HBA形式化验证方法是否可以检测出所建模型与待验证属性存在不一致的问题。
栾家伟[10]（2019）在《基于UML状态图的软件系统测试用例生成方法》文中指出软件测试是软件开发过程中保证软件质量的至关重要的一个环节,是提高软件质量的关键。软件开发中的问题被测试出来的越早,解决问题的成本越低。而在软件测试的过程当中,测试用例的质量好坏对测试工作的有着举足轻重的影响,好的测试用例可以使测试工作事半功倍,差的测试用例却可能会导致软件开发成本的提高。基于模型的测试其测试工作不必拘泥于软件开发的进度具体实施完成度,能够在各个阶段开始工作。只需根据需求规格说明便可以在开发初期甚至未进行开发时进行测试用例的设计,将开发与测试并发进行,大大缩减了软件开发的时间成本,提高开发效率。最终通过实际输出结果与需求规格说明中预期输出结果相比较,验证功能的一致性。本文在基于模型测试的基础上,主要研究UML模型中的状态图,进行测试用例的生成。UML作为标准的建模语言,具有广泛的通用性,有着强大的表达能力,可以清晰的描述对象的结构特征和表述对象的行为特征,且拥有良好的重用性和迭代性。在基于状态图进行测试生成时,将状态图视作一种特殊的有向流程图,通过几种不同的覆盖策略得到大量的测试场景以及测试用例。一种覆盖策略是通过利用图论中的深度优先搜索算法对状态图进行遍历,实现对状态图状态与转移的全部路径覆盖,得到测试场景与测试用例。另一种覆盖测试通过借鉴回溯法,根据转移发生的监护条件的布尔值真与假,实现对状态图的监护条件的覆盖,得到从源状态到终态的完整路径。通过采用不同的覆盖策略,生成较为完备测试场景与测试用例,从而达到帮助软件测试工作的目的。
二、面向模型检验的UML状态机语义（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、面向模型检验的UML状态机语义（论文提纲范文）
（1）自主化CTCS-3级列控系统新增场景建模及安全分析（论文提纲范文）
| 摘要 |
| Abstract |
| 1 绪论 |
| 1.1 论文的研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 国外研究现状 |
| 1.2.2 国内研究现状 |
| 1.3 论文结构及主要内容 |
| 2 面向列控系统模型的形式化方法 |
| 2.1 适用于自主化CTCS-3 级列控系统建模的形式化方法 |
| 2.1.1 与列控系统安全有关的特性 |
| 2.1.2 形式化方法比较 |
| 2.2 面向列控系统实时性建模的时间自动机 |
| 2.2.1 时间自动机理论 |
| 2.2.2 时间自动机的积 |
| 2.3 验证工具UPPAAL |
| 2.3.1 UPPAAL介绍 |
| 2.3.2 UPPAAL中使用的验证语言 |
| 2.4 统一建模语言UML |
| 2.4.1 UML扩展机制 |
| 2.4.2 轨道电路行车许可校验场景的建模需求 |
| 2.5 安全特性扩展 |
| 2.5.1 列控系统的安全特性分析 |
| 2.5.2 安全特性包 |
| 2.5.3 UML概要文件 |
| 2.6 本章小结 |
| 3 基于时间自动机的轨道电路行车许可校验场景建模与验证 |
| 3.1 场景分析 |
| 3.1.1 轨道电路行车许可 |
| 3.1.2 轨道电路行车许可校验场景 |
| 3.2 轨道电路行车许可校验场景建模与验证 |
| 3.2.1 场景时间自动机模型建立 |
| 3.2.2 场景时间自动机模型验证 |
| 3.3 本章小结 |
| 4 基于UML扩展机制的轨道电路行车许可校验场景模型 |
| 4.1 轨道电路行车许可校验场景顺序图和类图 |
| 4.1.1 轨道电路行车许可校验场景的UML顺序图 |
| 4.1.2 轨道电路行车许可校验场景的UML类图 |
| 4.2 轨道电路行车许可校验场景UML状态图 |
| 4.3 本章小结 |
| 5 轨道电路行车许可校验场景模型的安全分析 |
| 5.1 基于CTCS-3 级列控系统测试平台的场景验证 |
| 5.1.1 测试案例与测试序列 |
| 5.1.2 自主化CTCS-3 级列控系统测试序列的编写 |
| 5.1.3 测试结果分析 |
| 5.2 轨道电路行车许可场景的安全分析 |
| 5.2.1 故障模型整合算法 |
| 5.2.2 PHAVer故障模型的建立 |
| 5.2.3 故障检测器建立与安全分析 |
| 5.3 本章小结 |
| 结论 |
| 致谢 |
| 参考文献 |
| 攻读学位期间的研究成果 |
（2）面向UML的模型检测方法研究（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 选题研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.3 论文结构以及主要研究内容 |
| 1.4 本章小结 |
| 第二章 相关技术介绍 |
| 2.1 统一建模语言 |
| 2.2 模型检测 |
| 2.3 本章小结 |
| 第三章 UML建模分析 |
| 3.1 系统描述 |
| 3.2 Enterprise Architect简介 |
| 3.3 使用UML进行建模 |
| 3.4 本章小结 |
| 第四章 语义转换设计 |
| 4.1 NuSMV的系统描述 |
| 4.2 类图转换规则 |
| 4.3 状态图转换规则 |
| 4.4 顺序图转换规则 |
| 4.5 本章小结 |
| 第五章 定义规则的代码转换 |
| 5.1 XML简介 |
| 5.2 UML导出为XML文件 |
| 5.3 XML文件转换为SMV文件 |
| 5.4 本章小结 |
| 第六章 属性验证 |
| 6.1 CTL简介 |
| 6.2 属性验证 |
| 6.3 本章小结 |
| 第七章 总结与展望 |
| 参考文献 |
| 致谢 |
| 个人简介 |
（3）基于UML扩展机制的RBC控车场景功能安全分析方法（论文提纲范文）
| 摘要 |
| Abstract |
| 1 绪论 |
| 1.1 论文的研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 国外研究现状 |
| 1.2.2 国内研究现状 |
| 1.3 论文结构及主要内容 |
| 1.4 本章小结 |
| 2 面向列控系统的模型的UML安全概要设计 |
| 2.1 统一建模语言UML概述 |
| 2.1.1 UML语义表达 |
| 2.1.2 UML的图形表达 |
| 2.2 面向列控领域建模需求UML扩展 |
| 2.2.1 UML扩展机制 |
| 2.2.2 RBC控车场景的建模需求 |
| 2.3 安全特性扩展 |
| 2.3.1 列控系统的安全特性需求 |
| 2.3.2 安全特性包中元素及关系 |
| 2.3.3 UML概要文件中的设计 |
| 2.4 本章小结 |
| 3 基于UML扩展机制的RBC控车场景模型 |
| 3.1 RBC系统结构 |
| 3.1.1 RBC系统配置 |
| 3.1.2 RBC系统外部接口 |
| 3.2 列控系统中的RBC控车场景 |
| 3.2.1 行车许可场景 |
| 3.2.2 等级转换场景 |
| 3.2.3 RBC切换场景 |
| 3.3 RBC控车场景UML模型 |
| 3.3.1 RBC控车场景的UML顺序图 |
| 3.3.2 RBC控车场景的UML类图 |
| 3.3.3 RBC控车场景的UML状态转移图 |
| 3.4 本章小结 |
| 4 可执行的有色Petri网模型与验证 |
| 4.1 有色Petri网 |
| 4.1.1 有色Petri网的基本概念 |
| 4.1.2 有色Petri网的层次化模型 |
| 4.1.3 有色Petri网动态性质 |
| 4.1.4 CPNTools介绍 |
| 4.2 基于ASK-CTL的 CPN模型合理性验证算法 |
| 4.2.1 基于CPN的 ASK-CTL逻辑语言 |
| 4.2.2 模型合理性验证算法 |
| 4.3 UML向 CPN转换的基本规则 |
| 4.3.1 UML中间模型的提取 |
| 4.3.2 中间模型向CPN模型的转换 |
| 4.4 基于CPN分层结构的RBC控车场景模型验证 |
| 4.5 本章小结 |
| 5 RBC控车场景安全分析方法 |
| 5.1 基于可达集的分析方法 |
| 5.2 故障描述方法 |
| 5.3 PHAVer故障模型的建立 |
| 5.3.1 PHAVer与致因监视器的建立 |
| 5.3.2 故障模型整合算法 |
| 5.4 RBC控车场景的安全分析 |
| 5.5 本章小结 |
| 结论 |
| 致谢 |
| 参考文献 |
| 攻读学位期间的研究成果 |
（4）面向安全关键系统的SysML模型向AADL模型转换方法研究（论文提纲范文）
| 摘要 |
| abstract |
| 缩略词 |
| 第一章 绪论 |
| 1.1 课题研究背景 |
| 1.2 研究现状和选题依据 |
| 1.2.1 研究现状 |
| 1.2.2 选题依据 |
| 1.3 论文组织结构 |
| 第二章 相关知识 |
| 2.1 SysML语言 |
| 2.1.1 SysML语言概述 |
| 2.1.2 SysML语言扩展机制 |
| 2.2 AADL语言 |
| 2.2.1 AADL概述 |
| 2.2.2 AADL行为附件概述 |
| 2.2.3 AADL错误附件概述 |
| 2.3 基于模型的系统安全性分析 |
| 2.4 基于MDA的模型转换 |
| 2.4.1 元模型理论 |
| 2.4.2 异构模型转换 |
| 2.4.3 EMF框架 |
| 2.5 面向安全关键系统的SysML 模型向AADL 模型转换方法框架 |
| 2.6 本章小结 |
| 第三章 SysML安全性扩展与分析 |
| 3.1 SysML子集元模型及形式化定义 |
| 3.2 SysML安全性扩展 |
| 3.2.1 Failure Profile |
| 3.2.2 Failure Profile建模示例 |
| 3.3 基于Failure Profile的故障树的自动生成 |
| 3.3.1 Failure Profile到故障树的转换规则 |
| 3.3.2 故障树的自动生成算法 |
| 3.3.3 生成的故障树与分析示例 |
| 3.4 本章小结 |
| 第四章 SysML到 AADL的自动转换方法 |
| 4.1 基于元模型的模型转换实施框架 |
| 4.2 AADL子集元模型及形式化定义 |
| 4.3 SysML 子集元模型到AADL 子集元模型的语义映射 |
| 4.3.1 Sub IBD和 Sub BDD到 AADL架构模型的语义映射 |
| 4.3.2 Sub ACT到 AADL行为附件的语义映射 |
| 4.3.3 Failure Profile到 AADL错误附件的语义映射 |
| 4.4 Sub ACT到 AADL行为附件的结构转换算法 |
| 4.4.1 分支结构的转换 |
| 4.4.2 并发结构的转换 |
| 4.4.3 循环结构的转换 |
| 4.5 本章小结 |
| 第五章 工具实现与案例分析 |
| 5.1 SysML2AADL原型工具实现 |
| 5.2 飞机空气增压系统概述 |
| 5.3 飞机空气增压系统SysML建模 |
| 5.3.1 Sub BDD和 Sub IBD建模 |
| 5.3.2 Sub ACT建模 |
| 5.3.3 Failure Profile建模 |
| 5.3.4 故障树的生成与分析 |
| 5.4 AADL模型的生成 |
| 5.5 讨论 |
| 5.6 本章小结 |
| 第六章 总结与展望 |
| 6.1 论文工作总结 |
| 6.2 未来工作展望 |
| 参考文献 |
| 致谢 |
| 在学期间的研究成果及发表的学术论文 |
（5）用例图和顺序图的一致性研究（论文提纲范文）
| 中文摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 研究背景与动机 |
| 1.2 国内外研究现状 |
| 1.2.1 一致性研究的相关工作 |
| 1.2.2 用例图与顺序图的功能分解的相关工作 |
| 1.3 本文主要工作与结构 |
| 第2章 形式化模型 |
| 2.1 依赖结构简介 |
| 2.2 依赖结构执行语义 |
| 2.3 依赖结构的性质 |
| 2.4 本章小节 |
| 第3章 一致性研究 |
| 3.1 一致性的定义 |
| 3.2 一致性的分解 |
| 3.3 一致性保持与验证 |
| 3.4 算法 |
| 3.5 本章小节 |
| 第4章 用例图的形式语义 |
| 4.1 用例图简介 |
| 4.2 流结构与形式化模型的转换 |
| 4.3 用例图的分解 |
| 4.4 算法 |
| 4.5 本章小节 |
| 第5章 用例图与顺序图的一致性 |
| 5.1 顺序图及其抽象语法 |
| 5.2 顺序图的依赖结构语义 |
| 5.3 顺序图的分解 |
| 5.4 用例图与顺序图的一致性 |
| 5.5 本章小节 |
| 第6章 案例与工具 |
| 6.1 案例研究 |
| 6.2 工具 |
| 第7章 总结与展望 |
| 7.1 本文总结 |
| 7.2 本文展望 |
| 第8章 参考文献 |
| 攻读学位期间承担的科研任务与主要成果 |
| 致谢 |
| 个人简历 |
（6）日光温室蔬菜系统的UML建模与一致性检测（论文提纲范文）
| 摘要 |
| Abstract |
| 1 绪论 |
| 1.1 研究背景与意义 |
| 1.2 国内外研究现状 |
| 1.3 研究内容与创新点 |
| 1.4 文章的组织结构 |
| 2 UML的建模和一致性检测的研究 |
| 2.1 UML建模方式 |
| 2.2 UML建模工具 |
| 2.3 一致性检测方式 |
| 2.4 本章小结 |
| 3 日光温室蔬菜系统建模 |
| 3.1 日光温室的原理 |
| 3.2 系统的架构 |
| 3.2.1 系统的组成 |
| 3.2.2 系统的设计 |
| 3.3 系统模块的建立 |
| 3.3.1 温室嵌入式操作系统 |
| 3.3.2 温室传感器节点系统 |
| 3.3.3 基站模块的设计 |
| 3.3.4 视频监视系统的实现 |
| 3.4 系统的建模 |
| 3.4.1 温室嵌入式操作系统的建模 |
| 3.4.2 温室传感器节点系统 |
| 3.4.3 基站设计系统 |
| 3.4.4 软硬件看护系统 |
| 3.5 本章小结 |
| 4 基于抽象规则的UML模型一致性检测方法 |
| 4.1 一致性检测的原理 |
| 4.2 模型抽象规则 |
| 4.2.1 关系抽象和分类器抽象的语法 |
| 4.3 检测关系 |
| 4.3.1 关系一致性 |
| 4.3.2 搜索循环 |
| 4.3.3 循环中的问题 |
| 4.4 路径中的不一致 |
| 4.4.1 可靠性不一致 |
| 4.4.2 关系不一致 |
| 4.5 检测实体 |
| 4.5.1 静态图的检测 |
| 4.5.2 动态图检测 |
| 4.6 实验与分析 |
| 4.6.1 UML静态图检测 |
| 4.6.2 UML动态图检测 |
| 4.6.3 UML静态图和动态图检测准确率对比实验 |
| 4.7 本章小结 |
| 5 基于知识图谱的UML模型一致性性检测 |
| 5.1 UML冗余性 |
| 5.2 相关知识 |
| 5.2.1 知识图谱的完成 |
| 5.2.2 使用知识图谱抽象类图 |
| 5.3 UML图和知识图谱的转换 |
| 5.3.1 类图和知识图谱的转换 |
| 5.3.2 用例图和知识图谱的转换 |
| 5.3.3 对象图和知识图谱的转换 |
| 5.4 知识图谱抽象原理 |
| 5.4.1 计算节点之间的相似性 |
| 5.4.2 生成抽象知识图谱 |
| 5.4.3 生成抽象类图 |
| 5.5 UML图中不一致消除 |
| 5.5.1 类图中不一致消除 |
| 5.5.2 用例图中冗余消除 |
| 5.5.3 对象图中冗余消除 |
| 5.6 实验与分析 |
| 5.6.1 时间效率检测实验 |
| 5.6.2 准确率检测实验 |
| 5.7 本章小结 |
| 6 总结与展望 |
| 6.1 本文总结 |
| 6.2 研究工作展望 |
| 参考文献 |
| 附录 |
| 致谢 |
（7）面向SysML的模型转换与安全性分析方法研究（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 课题研究背景及意义 |
| 1.2 当前研究现状 |
| 1.3 论文研究内容 |
| 1.4 论文组织结构 |
| 第二章 基于模型的系统安全性分析概述 |
| 2.1 模型驱动系统工程 |
| 2.1.1 系统工程概述 |
| 2.1.2 模型驱动工程 |
| 2.2 基于模型的系统安全性分析方法 |
| 2.2.1 MBSA简介 |
| 2.2.2 MBSA的优点 |
| 2.3 MBSA中的关键技术 |
| 2.3.1 功能建模技术SysML |
| 2.3.2 故障建模技术AltaRica |
| 2.3.3 故障树的生成与分析技术 |
| 2.4 面向SysML模型的系统安全性分析验证框架 |
| 2.4.1 逻辑框架图 |
| 2.4.2 数据处理流程图 |
| 2.5 本章小节 |
| 第三章 SysML至 AltaRica3.0 的模型转换规则 |
| 3.1 BDD的转换 |
| 3.1.1 基本元素block的转换 |
| 3.1.2 结构特性 |
| 3.1.3 行为特性 |
| 3.1.4 模块间关系 |
| 3.2 IBD的转换 |
| 3.3 stm的转换 |
| 3.4 ValueType的转换 |
| 3.5 转换规则正确性的证明 |
| 3.6 三余度发电机实例模型转换 |
| 3.6.1 系统介绍 |
| 3.6.2 系统建模与模型转换 |
| 3.7 本章小结 |
| 第四章 原型工具的设计 |
| 4.1 面向SysML模型的安全性分析工具设计 |
| 4.1.1 工具设计架构 |
| 4.1.2 工具执行流程 |
| 4.2 工具的设计 |
| 4.2.1 转换功能 |
| 4.2.2 安全性分析功能 |
| 4.2.3 模型仿真功能 |
| 4.3 工具的实现 |
| 4.3.1 转换的实现 |
| 4.3.2 编译、生成故障树、故障树分析的实现 |
| 4.3.3 单步仿真及故障路径动态演示的实现 |
| 4.4 本章小结 |
| 第五章 机轮刹车系统的建模分析与验证 |
| 5.1 机轮刹车系统简介 |
| 5.2 机轮刹车系统的SysML建模分析 |
| 5.2.1 蓄压泵建模 |
| 5.2.2 限量阀建模 |
| 5.2.3 液压系统建模 |
| 5.2.4 BSCU建模 |
| 5.2.5 WBS建模 |
| 5.3 机轮刹车系统的AltaRica3.0 设计模型 |
| 5.3.1 蓄压泵的AltaRica3.0 模型 |
| 5.3.2 限量阀的AltaRica3.0 模型 |
| 5.3.3 BSCU的 AltaRica3.0 模型 |
| 5.3.4 WBS的 AltaRica3.0 模型 |
| 5.4 故障分析与传播路径的动态演示 |
| 5.4.1 故障树分析 |
| 5.4.2 故障路径动态演示 |
| 5.4.3 安全性属性验证 |
| 5.5 本章小结 |
| 第六章 总结与展望 |
| 6.1 论文工作总结 |
| 6.2 未来工作展望 |
| 参考文献 |
| 致谢 |
| 在学期间的研究成果及发表的学术论文 |
（8）基于SysML的安全性需求追踪及验证方法研究（论文提纲范文）
| 摘要 |
| abstract |
| 缩略词 |
| 第一章 绪论 |
| 1.1 课题研究背景 |
| 1.1.1 安全关键系统 |
| 1.1.2 问题的提出 |
| 1.2 研究现状及选题依据 |
| 1.3 论文组织 |
| 第二章 基于SysML的安全性需求追踪及验证方法概述 |
| 2.1 基于SysML的需求追踪方法 |
| 2.1.1 需求可追踪性 |
| 2.1.2 安全性需求获取 |
| 2.1.3 SysML建模 |
| 2.2 形式化安全性验证方法介绍 |
| 2.3 基于扩展SysML的安全性需求追踪及验证框架 |
| 2.4 本章小结 |
| 第三章 扩展SysML支持安全性需求追踪信息的生成 |
| 3.1 追踪信息模型构建 |
| 3.2 SysML中追踪信息捕获 |
| 3.2.1 需求构造型扩展 |
| 3.2.2 SysML配置文件构建 |
| 3.3 安全性需求追踪信息抽取 |
| 3.3.1 追踪信息表达元模型 |
| 3.3.2 追踪信息文档自动生成 |
| 3.4 本章小结 |
| 第四章 结合追踪信息和模型检测的安全性需求验证 |
| 4.1 SysML安全相关模块定位 |
| 4.1.1 追踪完整性分析 |
| 4.1.2 追踪信息模型形式化定义 |
| 4.1.3 SysML块定义图精化 |
| 4.2 SysML模型到NuSMV的转换 |
| 4.2.1 SysML结构与行为模型 |
| 4.2.2 NuSMV输入模型 |
| 4.2.3 SysML模型到NuSMV模型转换规则 |
| 4.3 基于模型检测的安全性需求验证 |
| 4.4 本章小结 |
| 第五章 案例分析 |
| 5.1 RCS追踪信息生成 |
| 5.2 RCS安全性需求验证 |
| 5.3 本章小结 |
| 第六章 总结与展望 |
| 6.1 论文工作总结 |
| 6.2 未来工作展望 |
| 参考文献 |
| 致谢 |
| 在学期间的研究成果及发表的学术论文 |
| 附录 |
（9）面向功能行为层次化建模的AADL行为附件扩展及验证方法（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 课题研究背景 |
| 1.2 研究现状及选题依据 |
| 1.2.1 AADL行为附件研究现状 |
| 1.2.2 层次状态机研究现状 |
| 1.2.3 AADL形式化研究现状 |
| 1.2.4 选题依据 |
| 1.3 论文组织结构 |
| 第二章 基于AADL行为附件的功能行为层次化建模及验证方法 |
| 2.1 AADL语言及AADL行为附件概述 |
| 2.1.1 AADL概述 |
| 2.1.2 AADL行为附件概述 |
| 2.2 形式化验证方法概述 |
| 2.3 基于AADL行为附件的功能行为层次化建模与验证方法框架 |
| 2.4 本章小结 |
| 第三章 面向层次化建模的AADL行为附件扩展 |
| 3.1 AADL层次行为附件(HBA)定义 |
| 3.1.1 AADL行为附件定义 |
| 3.1.2 AADL层次行为附件定义 |
| 3.2 AADL层次行为附件(HBA)语法 |
| 3.3 AADL层次行为附件(HBA)语义 |
| 3.4 AADL层次行为附件(HBA)元模型扩展及实现 |
| 3.4.1 AADL层次行为附件(HBA)元模型扩展 |
| 3.4.2 基于ANTLR和 Xtext技术的HBA实现 |
| 3.5 本章小结 |
| 第四章 基于时间自动机的AADL层次行为附件的形式化验证 |
| 4.1 层次行为模型扁平化 |
| 4.1.1 XOR状态扁平化 |
| 4.1.2 AND状态扁平化 |
| 4.2 层次行为附件到时间自动机的转换 |
| 4.2.1 时间自动机语义 |
| 4.2.2 层次行为附件到时间自动机的转换规则 |
| 4.3 本章小结 |
| 第五章 案例分析 |
| 5.1 系统概述 |
| 5.2 系统功能行为建模 |
| 5.2.1 姿态控制线程初始行为模型 |
| 5.2.2 姿态控制线程精化行为模型 |
| 5.3 系统功能行为验证 |
| 5.3.1 系统功能行为模型扁平化 |
| 5.3.2 系统功能行为模型转换 |
| 5.3.3 系统功能行为验证与分析 |
| 5.4 本章小结 |
| 第六章 总结与展望 |
| 6.1 论文工作总结 |
| 6.2 未来工作展望 |
| 参考文献 |
| 致谢 |
| 在学期间的研究成果及发表的学术论文 |
| 附录 A 层次行为附件完整ANTLR代码 |
| 附录 B 姿态控制线程完整模型代码 |
（10）基于UML状态图的软件系统测试用例生成方法（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 研究背景与意义 |
| 1.2 软件测试分类 |
| 1.3 国内外研究现状 |
| 1.4 本文组织结构 |
| 1.5 本文主要研究内容 |
| 第2章 相关理论基础 |
| 2.1 模型 |
| 2.1.1 基于模型的测试 |
| 2.1.2 典型测试模型 |
| 2.1.3 基于代码测试和基于模型测试的比较 |
| 2.2 测试场景与用例 |
| 2.2.1 测试场景 |
| 2.2.2 测试用例 |
| 2.2.3 测试充分性 |
| 2.3 UML简介 |
| 2.3.1 UML的可测试性 |
| 2.3.2 视图和图 |
| 2.4 状态图 |
| 2.4.1 状态图的覆盖准则 |
| 2.5 本章小结 |
| 第3章 有限状态机和扩展有限状态机 |
| 3.1 基于有限状态机的测试 |
| 3.2 基于扩展有限状态机的测试 |
| 3.2.1 关于EFSM的优化 |
| 3.3 本章小结 |
| 第4章 基于UML状态图测试用例生成方法 |
| 4.1 基于深度优先搜索的生成策略 |
| 4.1.1 深度优先搜索的具体实现 |
| 4.1.2 算法描述 |
| 4.2 基于回溯法的生成策略 |
| 4.2.1 回溯方法的具体实现 |
| 4.2.2 算法描述 |
| 4.3 监护条件的条件覆盖 |
| 4.4 本章小结 |
| 第5章 仓库管理系统的实例分析 |
| 5.1 测试用例生成工具简介 |
| 5.2 仓库管理系统简介 |
| 5.3 测试用例生成 |
| 5.3.1 登录功能测试用例生成 |
| 5.3.2 库存预警子功能测试用例生成 |
| 5.3.3 订单管理子功能测试用例生成 |
| 5.3.4 入库子功能测试用例生成 |
| 5.3.5 出库子功能测试用例生成 |
| 5.4 本章小结 |
| 第6章 总结与展望 |
| 参考文献 |
| 攻读硕士学位期间发表的学术论文 |
| 致谢 |
四、面向模型检验的UML状态机语义（论文参考文献）
- [1]自主化CTCS-3级列控系统新增场景建模及安全分析[D]. 肖伟. 兰州交通大学, 2021(02)
- [2]面向UML的模型检测方法研究[D]. 王媛. 北方民族大学, 2021(08)
- [3]基于UML扩展机制的RBC控车场景功能安全分析方法[D]. 周游. 兰州交通大学, 2020(01)
- [4]面向安全关键系统的SysML模型向AADL模型转换方法研究[D]. 马燕燕. 南京航空航天大学, 2020(07)
- [5]用例图和顺序图的一致性研究[D]. 陈杨杨. 福建师范大学, 2020
- [6]日光温室蔬菜系统的UML建模与一致性检测[D]. 姜懿芮. 海南大学, 2019(06)
- [7]面向SysML的模型转换与安全性分析方法研究[D]. 李宛倩. 南京航空航天大学, 2019(02)
- [8]基于SysML的安全性需求追踪及验证方法研究[D]. 邓刘梦. 南京航空航天大学, 2019(02)
- [9]面向功能行为层次化建模的AADL行为附件扩展及验证方法[D]. 许金淼. 南京航空航天大学, 2019(02)
- [10]基于UML状态图的软件系统测试用例生成方法[D]. 栾家伟. 江苏科技大学, 2019(03)
标签：uml论文; 面向对象分析与设计论文; uml建模工具论文; 需求分析论文; 建模软件论文;