Synergistic verification and validation of systems and software engineering models

In this paper, we present a unified approach for the verification and validation of software and systems engineering design models expressed in UML 2.0 and SysML 1.0. The approach is based on three well-established techniques, namely formal analysis, programme analysis and software engineering (SwE) techniques. More precisely, our contribution consists of the synergistic combination of model checking, static analysis and SwE metrics that enables the automatic and efficient assessment of design models from static and dynamic perspectives. Additionally, we present the design and implementation of an automated computer-aided assessing framework integrating the proposed approach. Moreover, we discuss the related technical details and the underlying synergism. Finally, we illustrate the proposed approach by assessing a design case study that is composed of state machine and sequence diagrams.     

一种SysML模型到AADL模型的自动转换方法

安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。近年来,模型驱动开发方法逐渐成为安全关键系统设计与开发的重要手段。由于还没有一个建模语言能够支持整个安全关键系统开发生命周期,因此选择集成使用2种广泛使用的标准语言:系统建模语言(SysML)和嵌入式实时系统体系结构分析与设计语言(AADL)。SysML和AADL提供了同一系统的2个不同视图,SysML模型为系统工程师提供了一个系统视图,AADL为架构设计师建立一个较低层次的设计视图,它结合了实现所有功能的硬件、操作系统和代码。提出一种SysML模型到AADL模型的自动转换方法。首先,定义SysML子集SubSysML,主要包括模块定义图(BDD)、内部模块图(IBD)、活动图(ACT)子集和从IBD和BDD扩展的AADL Profile;其次,定义SubSysML到AADL的转换规则并设计转换算法;然后,对生成的AADL初始模型进行精化;最后,使用EMF框架技术实现SubSysML到AADL的模型转换工具并通过雷达案例验证所提方法的有效性。     

基于SysML的航电系统架构安全性评估方法

针对现有系统安全性分析方法中安全性分析与航电系统架构设计过程无法融合的问题,提出基于SysML的航电系统架构安全性评估方法。首先在EA中基于SysML建模语言建立系统架构模型;然后利用XML解析技术从中提取系统关键信息,并建立故障树模型对其失效概率与区域安全性等进行分析,得到安全性评估结果;最后基于SysML语言对IMA架构下的显示系统进行架构设计和安全性评估,评估结果验证了所提出安全性评估方法的有效性。      

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

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

SysML及其在C4ISR系统建模中的应用研究

针对C4ISR分析与设计中建模手段的不足,提出了基于SysML对C4ISR系统的组成、接口与通信、功能、状态变迁、系统事件跟踪等进行建模的方法.在分析SysML四层元模型体系结构基础上,分析了SysML的语义与图形表示机制,探讨了SysML对C4ISR系统建模的支持作用,并以某防空指挥系统的建模为例,对系统的组成、接口与通信关系、系统功能、状态转移以及事件跟踪进行了描述,系统分析了基于SysML的C4ISR系统建模过程.对于提高C4ISR系统建模能力提供了一种可行的思路.     

基于SysML的可执行体系结构框架

目前可执行体系结构的相关研究缺乏统一的描述框架和分析设计方法.为此,结合系统建模语言(SysML)中的行为图、需求图和结构图,改进美国国防部体系结构框架的三视图体系结构,在此基础上提出一种可执行体系结构框架模型,并规范可执行开发过程.应用结果表明,该框架是可行的,能为下一步体系结构的动态仿真评估验证提供方法指导.     

面向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状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。     

基于有色Petri网的SysML序列图的分析与验证

针对SysML序列图本身缺乏分析和验证手段的问题,提出了一种序列图到有色Petri网的转换方法:定义了将序列图的常用操作转换为等价有色Petri网的转换规则,重点是把序列图的常用结构如可选结构、条件结构、并行结构以及循环结构等映射为有色Petri网。这当中既包含结构元素,如库所、变迁、输入/输出弧,又包含逻辑元素,如全局声明中的颜色集和变量、颜色集与库所、弧表达式以及初始标志。应用这些规则可以将序列图转换为有色Petri网模型,进而对其进行仿真分析,并可通过有色Petri网工具验证模型的无死锁性、可达性、有界性和活性。最后通过数字证书更新的实例分析了映射前后两种模型的语义,验证了映射的正确性。