基于SysML的机载软件分层精化建模与验证方法

机载软件被广泛应用于航空航天领域, 大幅提升了机载设备的性能.但随着机载软件规模逐渐增大、功能逐渐增多, 给软件的开发带来了难度, 如何保障机载软件的正确性和安全性也成为一个难题.基于模型的开发可以有效提升开发效率, 而形式化方法能够有效保障软件的正确性.为了降低开发难度, 同时保障机载软件的正确性、安全性, 本文提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先使用SysML状态机图对机载软件的动态行为进行建模, 根据提出的精化规则, 对初始模型进行手动逐层精化得到精化设计模型.然后针对软件模型动态变化的特性, 将SysML状态机模型自动转换为时间自动机网络, 并从软件需求中手动提取形式化TCTL性质进行模型检验.其次, 为了实现编码自动化, 将SysML模型自动转换至Simulink, 利用Simulink Coder生成源代码.最后, 以一个自动飞行控制软件为例进行了开发和验证, 实验结果表明了该方法的有效性.     

基于SysML和Modelica的复杂机电产品系统设计与仿真集成

系统仿真是辅助系统设计的一种重要手段,如何将系统设计与系统仿真有机结合,从而支持设计工作的高效开展,是一项重要的研究课题.针对这一问题,基于系统工程标准建模语言SysML和多领域仿真建模语言Modelica提出一套系统层设计与仿真集成方法.首先基于元对象机制分析和比较了SysML和Modelica的元模型;然后以Modelica元模型为基准,构造了面向Modelica的SysML扩展包M-Design;最后依据扩展的SysML和Modelica元模型定义了二者之间的映射规则,从而实现SysML设计模型向Modelica仿真模型的自动转换.以储水池系统为例,展示了复杂机电系统的设计和仿真的集成过程.     

嵌入式软件形式化建模方法

随着嵌入式系统在各行各业的普及,嵌入式系统也越来越复杂,为保证嵌入式系统正确性,研究从需求分析、系统设计到系统验证、代码自动生成统一建模方法尤为重要。针对以上问题,提出采用状态变迁矩阵（STM）对嵌入式软件进行建模,通过确认STM中的每个单元格保证软件的正确性,且在需求分析阶段更容易发现需求遗漏。针对单元格处理经常出现大量的逻辑判断问题,提出采用决策表（DT）模型对复杂多条件判断分支问题进行建模。在模型建立后进行验证,最后自动生成代码。通过对紧急制动控制建模实验,说明方法的正确性。     

面向SysML的系统安全性分析工具与实例研究

基于模型的安全性分析方法能够提高对目前复杂安全关键系统的建模与分析能力。系统建模语言(System Modeling Language,SysML)是一类在工业领域被广泛应用的非形式化系统功能建模语言,AltaRica是面向系统安全性分析的形式化建模语言。针对国内目前缺乏面向SysML的系统安全性分析工具的现状,设计实现了一个面向SysML的系统安全性分析工具并进行了实例研究。首先建立了SysML设计模型到AltaRica分析模型的映射规则;同时根据映射规则设计算法实现两种模型的自动转换,并集成了Altarica的分析引擎对系统模型进行自动化安全性分析;最后以SAE-AIR6110标准中的一个复杂的机轮刹车系统(Wheel Brake System,WBS)为实例,验证了所提工具的可行性和有效性。实验结果表明,对于包含25个组件类型、34个组件实例的复杂系统,该工具可有效地完成SysML模型到AltaRica模型的转换并进行正确的安全性分析。     

模型驱动的嵌入式系统设计安全性验证方法研究

基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。     

基于Spin的SysML活动图验证框架

系统建模语言（systems modeling language,SysML）缺乏精确的形式化分析和验证手段,造成模型存在死锁、活锁等诸多问题,可以通过形式化验证方法来提高模型的正确性。然而,受制于传统的形式化方法需要复杂的公式推理,并且不易理解等方面局限性,大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题,提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型,将多层次活动图分解转换为Spin的输入模型,并对相关子图进行重组和验证。实验表明,该方法可以有效识别多层次活动图,并准确实施转换,为模型验证的演化提供支持。     

基于限定中文自然语言需求的SysML模型自动生成方法

模型驱动开发方法逐渐成为安全关键信息物理融合系统(safety-critical cyber-physical system,SC-CPS)设计与开发的重要手段.然而,安全关键信息物理融合系统需求往往是通过自然语言描述的,如何自动化或半自动化链接自然语言需求和基于模型驱动的系统设计与开发过程是目前面临的重要挑战.面向安全关键信息物理融合系统,提出基于限定中文自然语言需求的SysML模型自动生成方法RNL2SysML.首先,为了降低自然语言需求表达的二义性,提出一种结构化的限定自然语言需求模板进行需求规约,并通过基于人工智能的(AI)安全关键信息物理融合系统术语提取和推荐方法,对系统需求中的领域术语和数据字典加以自动提取,提高限定自然语言需求规约工作的自动化程度.然后,给出限定自然语言需求规约到SysML系统设计模型的转换方法.最后,基于开源工具Papyrus对所提方法进行了原型工具实现,并通过航空领域的飞机空气增压系统(airplane air compressor system)案例验证了方法的有效性和实用性.     

模型驱动的复杂装备系统设计与仿真验证研究

复杂装备体系化、产品化的发展方向推动了MBSE在装备研制领域的应用发展。针对复杂装备功能高度复杂的设计难点,提出了一种模型驱动的复杂装备系统设计与仿真验证方法,阐述了从作战需求分析到产品实现的装备研制全流程的建模设计与仿真分析验证思路。同时,基于SysML仿真平台,结合装备作战过程典型案例,对装备系统模型进行仿真分析,实现了装备作战全过程的功能仿真,验证了模型逻辑的一致性、接口和输入输出流的准确性以及设计方法的可行性。结果证明,所提出的设计与仿真方法具有较高的工程实用价值,可极大地提高装备设计的完备性和效率。     

基于SysML的通信卫星故障分析方法研究

针对大型通信卫星故障分析过程复杂、系统性差等问题,采用MBSE思想,提出基于SysML的通信卫星故障分析方法,在卫星方案设计早期以SysML所表达的系统模型为中心开展故障分析与故障预案的验证.上述方法定义了针对卫星故障分析的元模型,以通信卫星姿态控制系统为对象,构建出规范表达的故障模型、系统功能模型以及故障处置行为模型...     

一种网构软件体系结构中的纵横验证机制*

如何在开放、动态、复杂的Internet环境下开发网构软件是软件技术领域一个挑战性课题。从网构软件整个生命周期入手,对网构软件的形式化模型,在简单介绍抽象状态机(ASM)的基础理论之后,刻画了网构软件的构件模型,并对构件模型进行了基于ASM的形式化描述,在此基础上,将粗粒度抽象构件的精化问题转换为求解构件组合方案的问题,并在体系结构元层,提出一种双向验证方法对不同抽象程度的组合方案进行横向和纵向的验证,以保证目标系统的正确性和求精过程的正确性。以上形式化建模和双向验证方法尽可能地避免和消除了软件设计早期的错误。通过系统实验验证可以看出,该方法对网构软件的开发具有一定指导意义。     

一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式,它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求,提出了对该模型进行形式化验证的算法：基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高可验证系统的规模.另外结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.     

基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究

能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括:构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析.     

一种基于LHPN的信息物理融合系统模型验证方法

由于信息物理融合系统(CPS)的硬件集成度和软件参与度不断提高,大量软件与硬件间异构连通并相互控制,使得CPS的分析设计、建模与验证也愈加困难,由此引起模型的状态空间膨胀问题。提出利用带标记混合Petri网方法对CPS进行建模和验证研究,在CPS中采用模型检测和定理证明相结合的形式化方法,对试图解决系统验证时状态空间膨胀问题供理论依据。提出一种自动抽取及其简化模型的方法,在容错温度传感器系统中的初步实验结果表明该方法是可行的,通过一个实例原型的应用说明了该方法的有效性。     

基于SysML的船厂堆场作业系统建模与仿真*

研究了基于系统建模语言SysML的船厂堆场作业系统建模及仿真实现问题。首先基于SysML的系统建模方法建立了堆场作业系统的系统需求、结构及行为模型;然后利用仿真系统ARENA解决SysML模型的实现问题,并设计了从SysML模型到ARENA模型的转换方法。实例验证结果表明,SysML在系统建模方面具有良好的表达性,利用ARENA对SysML模型进行仿真实现是可行的。     

基于UML的商业建模及模型验证机制研究

传统的商业建模方法存在无法为商业系统开发提供一个集成的"从概念到代码"的方案的缺陷,为解决在商业建模中存在的问题,提出了使用基于UML的商业建模方法.用实例阐述了该方法的具体步骤,并针对基于UML模型形式化复杂、验证难的问题,进一步提出了一种模型形式化的方法.应用实例和实验结果表明,基于UML建模方法和形式化方法能够减少商业建模的工作量,提高商业软件的开发效率及质量,较好地解决了商业建模中存在的问题.     

基于UML的嵌入式系统建模及模型验证机制研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可，并有很多成功的应用，但UML存在时间约束描述能力不强和所建模型形式化复杂、验证难的问题。针对上述问题，本文提出了使用UML扩展机制对UML状态图进行时间扩展，建立系统状态一约束一事件矩阵来对模型进行形式化描述的方法。该方法解决了UML在嵌入式系统建模时存在的问题。应用实例和实验结果验证了该方法的可行性和有效性。     

基于MTRDL的自动飞行系统模式需求建模与验证方法[1]

在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中必需的多重飞行模式之间的交互关系,还体现在模式转换与外部环境之间复杂的数据与控制交联关系,这些交联关系同时隐含了飞行模式转换的安全性质,这些特征提高了形式化方法的应用难度.本文工作提出一种领域特定的建模验证框架:首先,提出面向自动飞行系统模式转换的领域需求建模语言MTRDL,和基于该语言扩展于SysML上的建模方法;其次,提出基于安全需求模板的安全性质辅助规约方法;最后,通过对某机型的若干条目化需求的实例研究,证明了本文方法在自动飞行系统模式转换需求验证中的有效性.     

一种嵌入式系统设计的建模方法研究

针对在嵌入式系统设计中,目前常用的VHDL建模方法方法存在不易理解、模型描述困难、工作量大的问题,UML建模方法存在模型需形式化、验证难等问题,提出了一种基于SpecCharts语言的嵌入式系统建模方法--使用SpecCharts语言语法、文字和图形相结合来描述嵌入式系统,能满足嵌入式系统设计的描述要求,建模效率是VHDL方法的2.82倍,是UML方法的1.25倍,并且具有容易理解、容易描述、能利用VHDL的支撑工具直接进行模拟验证、建模工作量小等优点,较好地解决了嵌入式系统设计建模中存在的上述问题,有较高的实用价值.     

信息-物理融合系统动态行为模型构建方法

信息-物理融合系统(Cyber-Physical System,CPS)特有的计算、通信、控制的联合动态性,计算与物理的多尺度融合性,系统环境及状态的时空交互性以及系统动态行为的非确定性,不但使面向CPS的模型驱动设计与验证方法在CPS系统设计中更为重要,而且也向其提出了新的技术挑战.论文在结合典型实例分析CPS系统特征及其模型构建具体挑战的基础上,研究并总结了CPS动态行为建模的主要方法:一体化建模方法从CPS系统层面描述计算过程与物理过程的交互与融合;时空交互建模方法关注CPS系统行为与时间及空间关系的语义表示;功能和实现兼容建模方法侧重刻画CPS系统的逻辑设计和物理实现的映射与支撑;而集成建模方法则重点解决多异构模型的交互方式与语义的一致表达.论文基于多异构实体的CPS系统建模框架,提出了一种CPS系统结构与动态行为的协同建模方法,并用CPS-ADL对其进行了实现和验证.     

基于UML类图模型的一致性检查方法

UML中的类图采用直观的图形化表示方法,有效描述了待建系统的静态特征,为系统设计人员发现系统模型中存在的不一致性和冗余等问题,提供了有效的分析工具.但是对于复杂的系统,完全依靠系统分析人员发现模型中存在的不一致性和冗余等问题是不现实的,应当为建模工具赋以模型自动一致性检查功能.SHOIQ(D)是描述逻辑家族中可判定的子集,它在保证推理可判定的同时,具备较强的描述知识能力.鉴于上述特点,通过从UML类图图元中抽取语义.用SHOIQ(D)形式化描述类图图元,借助自动推理引擎,从而使基于UML类图模型的自动一致性检查功能得到实现.根据该方法改进后的建模工具,可以自动发现基于UML类图模型中存在的不一致性和冗余等问题.