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

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

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

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

嵌入式软件建模、实现与验证：研究与进展

随着计算机硬件设备计算能力的迅速提高,嵌入式系统中软件的规模和复杂度的急剧增大,软件可靠性在嵌入式系统中的重要性占据了统治地位。本文首先概要介绍了嵌入式软件不同于传统商业软件、科学计算软件的物理性、实时性、领域性等重要特征,以及由此带来的困难和挑战。然后重点介绍目前在解决嵌入式软件系统开发过程中的问题时所采取的建模思想、实现技术和验证方法。最后对嵌入式软件及其相关技术的发展进行了展望。     

基于ADS2的嵌入式软件测试仿真建模方法研究

嵌入式软件通常运行于特定的物理环境中,外部设备接口种类多,功能差异大,实时性强,在进行测试时需要花费大量人力、物力来构建测试环境。针对这一问题,采用半实物仿真技术,利用ADS2测试工具对外部设备进行仿真建模,构建一个逼真的模拟环境来进行嵌入式软件测试。ADS2能够满足嵌入式软件仿真测试的通用化和实时性要求,可以有效支持数据源、交联设备等多种仿真模型的设计开发。测试实例表明,利用ADS2进行嵌入式软件半实物仿真测试,能够加快测试环境构建过程,降低测试成本,拓宽测试范围,提高嵌入式软件测试的质量和效率。     

基于UML的嵌入式软件建模研究

本文以某型嵌入式控制系统软件的设计建模为例,证明了以可视化面向对象的UML建模工具,能够有效克服传统嵌入式系统软件设计中出现的问题,为嵌入式系统软件开发人员提供了一种新的设计开发方法。     

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

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

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

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

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

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

制导兵器系统建模与仿真的校核、验证与认可

介绍模型校核、验证与认可的基本概念,研究制导兵器系统建模与仿真发ＶＶＡ技术方法。从系统工程观点出发,首先给出制导兵器系统仿真研究全生命周期框架,在此基础上探讨具体的ＶＶＡ技术。所给出的制导兵器系统建模与仿真的ＶＶＡ技术方法,可用来指导建模与仿真,对提高仿真系统的置信度、增加仿真结果可信性具有重要的意义。     

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

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

基于时间STM的软件形式化建模与验证方法

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.     

基于虚拟微处理器的嵌入式软件开发与系统验证环境

嵌入式系统设计过程中软件与硬件集成验证的滞后，已成为制约整个系统开发进程的重要因素．虚拟微处理器是指在嵌入式系统硬件原型形成之前构造的可仿真原型，通过对微处理器的仿真支持软件嵌入式软件开发．介绍了基于虚拟微处理器技术的嵌入式软件开发环境的设计和实现，利用该环境，设计者可在设计早期进行系统集成验证，减少设计错误并缩短设计周期．该环境已经在嵌入式系统开发过程中得到成功应用．     

可组合嵌入式软件建模与验证技术研究综述

可组合嵌入式软件以构件开发技术为基础,研究嵌入式构件的建模、组合性质、构件间组合机制以及组合验证等理论、方法和技术.从组合理论、建模与验证技术这3个方面对可组合嵌入式软件的研究现状进行调研分析.组合理论研究给出构件可组合性的乐观定义和悲观定义,从组合操作、组合规则两个方面定义构件间的组合机制.针对嵌入式构件的特点,着重调研了非功能特性和异构构件的建模与组合技术,分析了非功能特性约束、面向多特性的模型等方法.分析了基于契约的验证、基于不变量的验证、基于模型检查的验证等多种嵌入式软件组合验证技术.最后,探讨了需要进一步研究的问题.     

基于SysML与Simulink的机载传感器建模方法

飞行器管理系统的传感器具有种类繁多、易受环境因素干扰、冗余设计等特点.而以往系统的传感器建模过程中,主要依靠简单的数学公式模拟部件的主要特性,忽略了绝大部分的真实细节,无法高度还原系统特性.基于模型的系统工程(Model Based System Engineering,MBSE)思想,提出一种高度还原飞行器管理系统传感器特性的建模方法,并给出建模步骤.利用系统建模语言(Systems Modeling Language,SysML)的各类图形,对系统传感器的物理特征、不同工作状态以及余度设计等特点建立模型;并基于Simulink建立传感器的连续动态行为模型;最后,通过联合仿真对整体模型进行验证.结果表明,上述方法实现了对系统传感器真实物理特性的全面描述,提高了传感器模型的仿真度.     

UML建模的嵌入式系统开发方法研究

介绍了嵌入式系统的特点,总结了开发嵌入式系统所要解决的关键问题,论证了使用UML开发嵌入式系统的可行性,并给出了一个在Rhapsody开发环境下使用UML开发嵌入式系统的实例.实例证明,使用UML开发嵌入式系统能够缩短开发周期,提高软件质量,降低测试成本.     

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

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

基于嵌入式方法的浮点单元验证系统设计

浮点单元的验证是最具挑战性的任务之一。基于Xilinx FX系列带powerpc 405硬核的FPGA,利用嵌入式系统开发套件EDK,设计了一个嵌入式系统对浮点单元进行验证。验证原理为把用户IP(被测浮点单元)通过APU控制器连接到powerpc 405处理器核,编写测试程序,通过自定义指令对用户IP进行访问,根据程序的运算结果判断被测IP的正确性。     

一种基于模型检查的嵌入式软件验证方法

嵌入式软件广泛应用于不同领域,如消费电子、工业控制、汽车电子、移动通信等。嵌入式软件的可靠性保证十分关键。嵌入式软件中常见的错误包括状态机错误、时序错误、栈溢出／存储溢出等,在开发过程中对嵌入式软件进行验证十分重要。