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

yangyang110

关注我们，免费订阅航电一手资讯



摘要

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



关键词

机载软件;模型精化;模型转换;模型检验

随着计算机系统在航空航天领域的广泛应用,机载软件已经成为飞行控制、通信导航、火力控制以及维修保障的核心。但机载软件的安全性得不到足够的保障,一旦软件失效,很可能造成巨大的财产损失和人员伤亡.为确保机载软件的正确性、安全性,机载软件必须经过安全认证、符合适航标准才能投入使用.目前,航空领域广泛采用的是航空无线电技术委员会(radio technical commission for aeronautics,RTCA)提出的适航认证标准体系。适航标准是以目标为导向的,规定了机载软件开发以及验证过程中所必须满足的一些目标,但并未提供详细的开发和验证方法说明。本文基于DO-331和DO-333标准对机载软件进行开发和验证,可为面向适航标准的相关工作提供参考。

在民用航空领域,研究人员常基于模型进行机载软件的开发和验证.模型的使用,便于对系统工程进行管理,还支持模型仿真、模型验证、自动化代码生成等手段,可以大幅提高开发效率.软件开发人员通常采用半形式化的建模语言对机载软件进行建模,如统一建模语言(unified modeling language,UML)、系统建模语言(system modeling language,SysML)等.其中,SysML是UML[5]的完善和扩展,支持对软件的需求、动态行为以及静态结构进行建模.美国宇航局的喷气推进实验室曾基于SysML模型来设计研发飞行系统。文献对民用飞机的高升力系统进行基于模型的设计,利用模型的关联性和追溯关系来保证设计过程的完整性。

模型检验是一种常用的形式化方法,可以自动地对系统的功能属性定量地可重复性验证。目前,基于模型的形式化验证方法已经存在一系列工具,包括NuSMV,Spinp,UPPAAL等.利用模型转换将SysML转换至形式化模型,可以重用这些工具已有的验证和分析能力.其中,UPPAAL可以将实时系统建模为时间自动机(timed automata,TA),可以对目标系统的动态行为进行仿真,验证模型是否满足时间计算树逻辑(timed computation treelogic,TCTL)语言描述的形式化性质。

代码自动生成可以提高软件开发的效率,减轻软件开发的工作量.为实现软件自动编码,可以利用现有的支持模型生成代码的工具,如Mathworks公司开发的可视化仿真工具Simulink、Esterel公司开发的SCADE等.如文献将UML与Simulink结合起来,自动生成飞控软件的产品级代码。

为确保机载软件安全性和正确性,一方面需要对软件运行模式进行分析,获取软件的功能性需求,同时对软件的故障模式进行分析,从中获取软件的安全性需求,以支持软件开发和验证;另一方面,从软件开发和验证过程出发,根据适航标准相应的目标,判断软件开发和验证过程中是否符合适航审定目标.基于上述背景,本文提出了一种基于SysML状态机图子集的机载软件分层精化建模与验证方法(如图1所示)。



图 1 基于SysML的分层精化建模和验证方法框架

首先,利用SysML需求图来描述和记录机载软件需求,便于后续管理.其次,基于SysML状态机图(state machine diagram,SMD)子集建立初始设计模型(高级需求模型),然后手动应用精化规则得到详细精化模型(低级需求模型).同时,建立关系矩阵记录模型和需求间的追溯关系.检测出内在缺陷的时间越晚,修复该缺陷的代价也越高.因此在每层模型建立后,通过自动模型转换得到形式化的时间自动机模型,从需求中手动提取TCTL形式化性质进行模型检验,对没有通过验证的模型,修改其源SysML模型并再次进行模型检验,直到所有需求约束通过检验.最后,将精化模型进行自动模型转换得到Simulink模型,利用SimulinkCoder自动生成源代码。

总结该方法主要优点有:(1)可以对复杂机载软件进行分析和开发,保障其安全性和正确性;(2)提出了SysML状态机模型的精化规则,从而进行分层建模;(3)模型转换过程和编码过程高度自动化。

本文第1节主要介绍相关基础知识.第2节介绍基于SysML状态机图子集的精化规则和精化建模实例.第3节详细介绍模型转换的算法、映射规则和实例,并分析模型转换的正确性.第4节给出模型转换的工具实现.第5节通过实例验证文中提出方法的有效性.第6节分析国内外相关工作并与本文方法进行比较.第7节总结本文工作并提出未来的研究方向。

1

基础知识介绍

1.1适航标准DO-331和DO-333

机载软件作为安全关键软件,必须通过适航审定才能投入使用.RTCA发布了适航标准DO-331和DO-333,为机载软件的安全性保障提供了审查目标.其中,DO-331提供了一些行业实践中的模型使用样例.本文参考DO-331中模型使用样例4,将机载软件的生命周期划分为需求、设计模型和源代码这3个阶段.其中,初始设计模型描述较高级别需求,精化设计模型描述较低级别需求,二者之间没有明确界限.DO-333介绍了3类形式化方法:演绎法、模型检验、抽象解释.模型检验与演绎法相比,自动化程度更高且不需要验证人员掌握深厚的逻辑知识;与抽象解释相比,可应用于需求和设计过程的软件制品[14].因此,本方法中使用模型检验,对机载软件制品进行形式化验证,验证其是否满足需求约束.同时,审查软件制品是否满足DO-331和DO-333规定的目标。

1.2SysML基础知识与子集选取

系统建模语言SysML是对象管理组织(object management group,OMG)提出的标准建模语言.在实际应用中,机载软件建模不会涉及SysML的全部元素.基于机载软件动态行为建模研究需要,本工作依据最小化原则以及可描述性原则,选取SysML状态机图子集进行机载软件建模。

(1) 最小化原则

最小化原则指选取的SysML子集是满足机载软件建模的最小子集. SysML状态机图定义了3种状态内部行为entry, do, exit, 它们分别可以用进入状态、状态向自身状态以及迁出状态的迁移”影响”代替. 因此, 基于最小化原则, 本工作选取的状态机子集不包括entry, do, exit.

(2) 可描述性原则

可描述性指选取的SysML子集足以用于机载软件建模. 本工作主要考虑对机载软件动态行为的安全性和正确性进行分析, 其中: 安全性可以通过状态机能否正常运行, 以及故障条件判断、故障状态来体现; 正确性是从状态机对输入的处理是否符合需求来体现, 主要用到的是状态、迁移以及输入的数据变量。

依据上述子集选取原则, 最终我们选取了状态、迁移、变量、复合状态进行建模, 并给出SysML状态机子集的形式化定义。

定义1. 状态机可以定义为一个六元组STM: =〈S, s0, sf, V, T, CS〉。

● S为状态的有限集合, 状态主要分为初始状态(initial state)、简单状态(simple state)、最终状态(final state)以及复合状态(composite state);

● s0∈S, 表示初始状态;

● sf∈S, 表示最终状态;

● V是变量的有限集合, 其数据类型有整型、浮点型、布尔型和实数型等;

● T⊆S×{Tri, G, Eff}×S, 表示状态迁移有限集合, 其中, Tri表示事件触发器, G表示守卫, Eff表示影响. 源状态向目标状态的迁移可写作t(ss, st), t=(ss, tri, g, eff, st);

● CS⊆S, CS=S×T×S, 表示复合状态, 内含嵌套子状态以及子状态之间的迁移. 复合状态内部结构与状态机总体类似, 复合状态活动时, 首先进入子初始状态; 复合状态活动时, 有且仅有一个子状态活动.

SysML状态机初始处于初始状态s0, 后根据迁移上的tri和g进行状态迁移, 同时执行eff, 进入最终状态sf时结束运行. 迁移踪迹可以写作s0−→t0s1−→t1s2...−→tnsf