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

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

基于SysML & AADL的IMA刹车控制系统实时性需求验证

针对设计阶段难以对刹车控制系统进行实时性分析验证的问题,提出基于SysML & AADL的实时性需求验证方法。首先论述综合模块化航电系统中刹车控制系统的组成和实时性定义,基于SysML建模语言建立系统模型,并添加MARTE描述的组件时间延迟;然后建立SysML/MARTE与AADL的模型元素映射关系,根据该关系,将SysML模型转化为符合AADL语义的模型。最后利用AADL分析工具得到实时性验证结果,验证了所提出实时性验证方法的有效性。     

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

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

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

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

一种基于四变量模型的系统安全性建模与分析方法

近年来,基于模型的系统安全性分析与验证方法是安全关键系统工程领域中的一个重要研究方向。提出了一种基于四变量模型的系统安全性建模与分析验证方法,该方法利用AltaRica建模语言对系统进行建模。通过对四变量模型及AltaRica进行语义研究构建二者之间的映射规则,以民用飞机中机轮刹车系统(Wheel Brake System,WBS)为例来说明整个验证过程,即首先利用四变量模型从系统的需求层次上对WBS进行需求分析并根据映射关系构建AltaRica模型,接着利用故障树分析方法对WBS进行安全性研究,最后基于AltaRica配套工具ARC对系统的安全性属性进行验证。验证结果表明了该方法在系统安全工程领域中的实用性。     

基于MDA的MARTE模型形式化方法

针对嵌入式系统对可靠性和可预测性的要求,提出基于MDA对嵌入式系统的建模语言MARTE进行形式化描述的方法。建立Object-Z的元模型,定义了MARTE元模型与Object-Z元模型之间的模型转换关系,给出了MARTE模型到Object-Z模型的语义映射和语法转换的具体过程。该方法支持将MARTE模型形式化转换为Object-Z模型,有利于软件开发早期的检验和验证。     

基于SysML的复杂机电系统设计模型形式化扩展与验证

形式化系统验证是保证系统设计正确性的一种重要手段.如何针对复杂机电系统物理与软件相融合的特征,对系统设计的动态特征进行验证,是系统验证研究领域亟待解决的问题.针对这一问题,对系统工程标准建模语言SysML进行扩展,提出了一套形式化系统模型验证方法.首先,以计算树逻辑和基于流的功能表示为形式化基础,形成基于SysML的系统功能建模方法;然后,以混合自动机为基础,建立基于SysML的系统行为建模方法;最后,针对物理与软件子系统的不同动态特征,借助NuSMV模型校验器,以层次化方式实现系统模型的自动验证.以移动机器人系统为例,展示了复杂机电系统设计模型的自动验证过程.     

无人机飞控软件系统建模与测试用例生成研究

软件规模与复杂度的迅速增长已成为设计与检验现代高质量无人机飞行控制软件(FCS)系统的重要挑战。采用模型驱动工程(MDE)的框架,使用嵌入式实时系统建模语言(MARTE)建立起某型无人机飞控软件系统的模型,给出了基于时间自动机的系统动态行为的形式化模型实例;结合无人机FCS系统的应用背景,建立了基于时间自动机模型的测试用例生成方法,包括建立测试用例生成框架、测试用例生成规则以及用例生成策略等;对某型无人机飞控软件系统中的主控模块进行了建模与测试用例生成的实例分析研究。     

基于随机Petri网的SysML状态机图的验证

针对SysML状态机图本身缺乏分析和验证手段的问题,提出一种SysML状态机图向广义随机Petri网的转换方法。主要定义将SysML状态机图转换为相应Petri网可执行模型的八种转换规则,应用这些规则可以将状态机图转换为Petri网模型,进而对其进行分析、验证,并可检测SysML的行为规范与并发相关的性质,如死锁、有界性等,同时,该方法可处理带有时间延迟和概率信息的状态转换。最后通过数字证书系统的一个实例说明该方法的可行性。     

系统架构描述语言AADL的功能行为建模扩展

架构分析与设计语言(AADL)是一种用于描述复杂嵌入式系统体系架构的建模语言,被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为,而行为附件中没有表达层次自动机的机制。针对这一问题,提出了AADL行为附件的层次化扩展——HBA。首先给出了HBA的形式语法,然后定义了HBA的操作语义。提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了便于形式化验证,给出了HBA到时间自动机(TA)的转换规则,并基于模型检测工具UPPAAL进行形式化验证。最后,给出一个案例研究来验证所提方法的有效性。     

一种基于故障扩展SysML活动图的安全性验证框架研究

随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。     

AltaRica 3.0模型到Promela模型转换与验证方法研究

AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力方面的改进,以及其底层模型GTS的基本结构。以AltaRica3.0扁平化为GTS模型的思想为基础,提出了一种AltaRica3.0模型向Promela模型的转换规则。以民用飞机中机轮刹车系统WBS为例,建立了AltaRica3.0模型,并且通过转换规则转为Promela模型。最后根据民用航空标准SAE ARP 4761中对机轮刹车系统的安全性要求,利用SPIN工具对机轮刹车系统的安全属性进行了验证。     

Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata

UML is a widely-used,general purpose modeling language.But its lack of a rigorous semantics forbids the thorough analysis of designed solution,and thus precludes the discovery of significant problems at design time.To bridge the gap,the paper investigates the underlying semantics of UML state machine diagrams,along with the time-related modeling elements of MARTE,the profile for modeling and analysis of real-time embedded systems,and proposes a formal operational semantics based on extended hierarchical timed automata.The approach is exemplified on a simple example taken from the automotive domain.Verification is accomplished by translating designed models into the input language of the UPPAAL model checker.     

Ptolemy离散事件模型形式化验证方法

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。