面向航天型号软件的混成建模语言研究

胡指铭， 黄丽桃， 赵涌鑫

1. 华东师范大学软件工程学院， 上海 200062 2. 北京轩宇信息技术有限公司, 北京 100190

0 引 言

航天嵌入式软件及其运行环境具有高度的复杂性和不可预测性等特点，这就要求建模语言必须要有刻画系统和环境不同组件的表达能力，并且可以刻画面向嵌入式软件的模型特征，同时具有组合性和表达多重交互模式的能力.而周期控制系统语言SPARDL部分解决了前面的问题，但仅关注离散时间的动力系统，缺乏与物理世界的交互，为了实现对外部物理对象和环境的实时感知、可靠性信息传输、精确的动态控制与协调等目标，需要提出的语言能够对离散的控制逻辑和连续的物理变化建模，并描述它们之间的交互行为，从而更好地进行正确且精确的验证分析.

基于以上目的，本文提出了航天混成描述语言HSPARDL.为了更好地表示控制系统与物理世界的交互，在原有基础上引入了连续变量来描述物理设备组件的状态，并用微分方程来表示其变化规律，还引入了两个事件结构When和Until来连接物理设备和控制器.基于此框架，可以将物理过程和控制过程的描述和设计置于统一的形式化框架下，并且通过对该混成建模语言的形式化语义研究，消除由于自然语义二义性所引起的歧义性，揭示混成建模语言各语句的本质计算行为，从而为航天嵌入式系统的分析、设计、推理和验证提供坚实的理论基础.

1 航天混成描述语言HSPARDL

1.1 SPARDL

在介绍混成描述语言之前，先简单介绍其前身航天需求描述语言SPARDL.SPARDL是一种用来清晰且无二义性地描述航天型号软件需求的建模语言，其核心是模式图，它由一个个模式构成，模式间允许嵌套以生成子模式，模式内包含用于表示计算任务的控制流，这些控制流共用全局变量，由数据字典加以描述.图1是一个简单的模式图例子.

图1 SPARDL的整体架构Fig.1 SPARDL’s overall architecture

模式图的主要特点有：

(1)基本的建模元素为模式(mode).系统每个周期只处于一个模式，每个模式表示特定的状态，使用特定的控制流.

(2)模式图是周期驱动的.模式图作为一种反应式系统，会按照给定的时间反复执行计算任务，SPARDL定义模式图中每个模式都具有周期，且不一定完全相同，如载人航天器在其发射和绕轨道运行的周期就不同.同时模式间的迁移仅在一个周期结束时才会发生，这是模式图和状态图间一个比较明显的差异.

(3)模式图额外引入了时间谓词来作为模式间迁移的条件.考虑到控制系统的行为既取决于当前的状态，又取决于历史的状态，因此SPARDL定义了两种时间谓词Always和Eventually来表示历史状态是否成立，如Always(a==1，3)表示如果“连续3个周期a都为1，则该表达式的值为True”.

1.2 HSPARDL

SPARDL仅关注离散时间的动力系统，为了对航天型号软件中的物理环境和控制软件的交互进行建模，引入了只含连续变量的连续模型来表示物理设备的状态，用微分方程表示其变化规律，为了描述物理设备间的交互，还引入了卫兵条件以及连续谓词Until和等待谓词When，这构成了航天混成建模语言HSPARDL.

在HSPARDL中，仍采用模式图作为核心，它的整体架构如表1所示：

表1 HSPARDL的整体架构Tab.1 The overall architecture of HSPARDL

它表示HSPARDL是一个二元组，由数据字典Dictionary和模式图ModeDiagram构成.数据字典中的元素是一个四元组，包含名称name、属性attribute、类型type和默认值default value.属性有常量、离散变量和连续变量4种，类型有整型int、单精度float、双精度double、布尔bool和结构体struct 4种.模式图由若干个离散模式dMode和连续模式cMode构成，系统在某一时刻只能处于一个离散模式，也只能处于一个连续模式，但连续模式和离散模式间可以并行运行.

离散模式和连续模式的定义如表2所示.

表2 HSPARDL的模式定义Tab.2 Mode definition of HSPARDL

dMode表示离散模式，它表示控制系统的状态，和SPARDL中的模式相同，它包含标签name、周期period、初始化Init、控制流cfg、子模式dmode以及离散迁移dTrans，当离散模式包含子模式时，它的控制流不存在，即cfg=empty.离散迁移由四个部分组成，它包含源模式dm，优先级priority、离散迁移条件dguard以及目标离散模式dm’.当离散模式不满足任意的离散迁移条件时，模式不会发生迁移，下个周期仍然执行本模式；当离散模式满足若干离散迁移条件时，模式会在周期结束时迁移至优先级最高的目标模式.

cMode表示连续模式，它用来模拟外界物理环境的变化情况，它包含标签name、微分方程EQ以及连续迁移cTrans.它不受周期的控制，模式中的连续变量只会根据微分方程所表示的物理规律以及连续时间来变化，当until后的连续条件cguard满足时，微分方程终止.系统一次只能处于一个连续模式，当满足连续迁移条件时，系统会从源模式cm迁移至优先级最高的目标模式cm’.

基本的表达式分为状态表达式、和卫士表达式，其定义如表3所示.

表3 HSPARDL的基本表达式定义Tab.3 Basic expression definition of HSPARDL

状态表达式SExpr由常数c、离散变量dv、连续变量cv以及它们的算数组合f构成，布尔项BTerm由true、false以及状态表达式的关系运算p(如a

最后控制流的形式化定义如表4所示.

控制流用来表示模块的执行任务以及计算流程，它由局部声明declare、控制语句stmt以及它们的组合构成.控制语句stmt由原子语句pstmt和复合语句cstmt构成，原子语句包含对离散变量的赋值x:=SExpr、对连续变量的采样x←cv、调用控制算法.

表4 HSPARDL的控制流定义Tab.4 The control flow definition of HSPARDL

模块call name、跳过skip和混乱⊥，由于HSPARDL中的全局变量可以被当前模式所获的，因此无需引入其他语言中常用的信号的概念.复合语句包含语句的顺序组合、循环While、条件选择if以及等待语句when(dguard) stmt.if语句和when语句看似效果类似，但仍有区别，if语句的条件分支的选择是非阻塞的，而when语句会根据卫兵的成立情况选择下一步执行的对象，如果没有卫兵成立，系统会处于等待状态直至卫兵成立.

本文还引入了连续模块所特有的微分方程EQ表达式，它用常微分方程显式地表达连续变量的变化规律，微分方程可以被赋初值，还可以是多个微分方程的组合，IDLE是它的一种特殊情况，即连续模式中的连续变量不发生改变.为了使微分方程能够终止，设置了终止条件until cguard与其相组合，使微分方程能够构成一个完整的语句EQstmt，当cguard满足时，微分方程EQ随时间的变化终止.

2 HSPARDL的操作语义

本节将给出HSPARDL的基于迁移系统的操作语义.HSPARDL是一个层次模型，本文设计的语言主要着眼于模式层和控制流层，因此分两层讨论其操作语义.在模式层只关心由数据字典定义的全局变量，在控制流层中则注重描述计算过程.

2.1 模式层的操作语义

HSPARDL模型语义状态可用一个五元组表示

Config≜(cm,dm,l,per,Tr)

cm表示系统所处的连续模式，dm表示系统当前所处的离散模式，l∈{Begin,Excute,End}表示系统所处的离散模式的阶段，Begin表示周期初始，主要用来数据的采样，Excute表示准备执行周期任务，End表示周期末尾，用来发生迁移.per是周期计数器，如果系统发生模式切换，则per被置为1.Tr表示离散模式中变量的的历史取值序列，用来判断转移的条件.本节主要介绍模式级别的操作语义：

离散模式的采样规则：

其中σ′=σ(x1←v1,…xn←vn),vi是cm中的变量在cm(t)时的取值，t为取样时的连续时间

dm′是dm的子模式

以上两条规则均发生在离散模式的采样时刻.Rule1表示如果当前所处离散模式的控制流不为empty，即该离散模式不包含子模式，则系统所处的离散模式的阶段由Begin转为Excute，准备执行周期任务，并将连续模式中当前连续变量的值采样至离散模式的只读变量.Rule2表示如果当前所处离散模式的控制流为⊥，即该离散模式包含子模式，则系统将会立刻由当前模式进入到子模式，其他的值保持不变.

离散模式的执行规则：

且Tr.σ′(ts)=Tr.σ(ts)+period(dm)

Rule3发生在离散模式的执行过程中，表示如果离散模式的控制流执行后，模式中的值由σ变为σ^′，则系统所处离散模式的阶段由Excute变为End，离散模式中的值由σ变为σ′，模式的时间戳会自动加上本模式的周期.

模式的转移规则：

且dm′=tran.dm

且cm′=tran.cm

以上三条规则发生在模式的转移过程，rule4和rule5表示离散模式的转移，rule6表示连续模式的转移.rule4意为当没有一个离散转移条件能被满足时，系统继续执行该离散模式，系统所处阶段由End更新为Begin，且运行周期加1.rule5意为当至少有一个离散转移条件被满足时，选择优先级最高的进行转移，系统由当前离散模式dm转为目标离散模式dm’，并重置运行周期为1.rule6作用在连续模式上，意味当当前连续模式满足转移条件时，系统就可以按照最高的优先级转移到目标连续模式cm’，且不影响系统中的其他状态.

2.2 控制流层的操作语义

控制流层是用来描述模式的计算任务的，它由局部声明declare、控制语句stmt以及它们的组合构成，用一个三元组来描述控制流层的语义状态：

Config∷=(σ,stmts,status)

σ表示变量集合，它由全局变量和局部变量构成，stmts表示待执行的语句,status表示控制流层处于何种状态，它包含终止term、等待wait以及发散div三种状态.终止表示上一条语句成功运行，可以继续执行本条语句，wait表示上一条语句阻塞，需要一个卫兵事件来激活系统，div表示系统出现错误，无法执行后续的程序.以下是控制语句的语义规则：

接下来针对操作语义给出详细的解释说明：

rule1和rule2均表示赋值语句执行的操作语义，如果当前系统状态为term，则可以执行离散变量的赋值和连续变量的赋值，变量集合σ中的变量得到修改.

rule3表示调用某函数的操作语义，如果在当前变量集合σ下执行该函数可以得到新的变量集合 σ′，那么执行该语句会更新变量集合中的变量，并使当前执行的语句变为空.

rule4表示skip语句的操作语义，该语句不改变任何状态.rule5表示当出现发散语句时，不论系统时处于终止还是等待状态，系统都将变化至发散状态.rule6表示顺序组合语句的操作语义，意为一段顺序语句的执行结果等同于一步步执行每一条语句的结果.

rule7和rule8表示循环语句的操作语义，它们分别表示循环条件成立和不成立的情况，若成立，则执行循环内的语句和整个循环语句的顺序组合，若不成立，则不改变当前状态，循环结束，当前需要执行的语句变为空.

rule9和rule10表示条件语句，当满足对应的条件时执行对应的语句.

rule11和rule12表示等待语句的操作语义，它区别于条件语句，若等待卫士条件满足，则不论语句是处于终止状态还是等待状态，都将被触发并执行，若等待卫士条件不满足，则语句将从等待或终止状态变为等待状态，等待语句仍然在待执行的控制语句队列中.

rule13和rule14是对应连续模式中的语句的操作语义，当系统处于终止或等待状态时，如果cguard条件不成立，则连续变量会根据其微分方程的变化规律随时间发生变化，系统的状态变为等待，当cguard条件成立时，则连续变量不再发生变化，待执行语句变为空，系统的状态变为终止，还需注意的一点是，连续模式和离散模式是并发执行的，因此它们的语义状态除变量集合外都不相关.

3 应用案例

本节以某月球着陆器的慢速下降阶段为例，对本文提出的混成建模语言进行了一个简单的应用.动力下降是月球着陆过程中最具有挑战性的任务，因为它是完全自主的一个过程.由于存在通信的延迟，地球方面是无法追踪快速移动的航天器的，并且来自地球的远程控制命令也无法立即生效，故航天器必须依靠自己的制导、导航和控制系统实时获取当前状态，计算控制命令并使用该命令调整其姿态和发动机推力.本文选取六个下降阶段中的慢速下降阶段，作为建模的目标.

图2是在模式层上对离散模式的建模，它表示慢速下降模式的执行周期是128 ms，当停机信号1(通常由6 m高的传感器发出)被接收且着陆器在慢速下降阶段停留了10 s以上时，转移到SW1模式，若停机信号2(通常应由3 m高的传感器发出)被接收且着陆器在慢速下降阶段停留了10 s以上时，转移到SW2模式，当未收到关机信号且在慢速下降阶段停留了20 s以上时，转移到SW3模式，如果以上条件都不满足，系统将停留在缓慢下降阶段，并继续进行引导计算.

图3是对缓慢下降阶段的控制流进行的建模，控制流主要执行对着陆器的引导计算并发出相应的控制命令.由于引导计算涉及了大量的数学公式.

为简化起见，本文用文字代替了程序的执行过程.当进入缓慢下降模式时，系统会对v、gm、Fc和M四个量进行采样，接着根据引导规则进行了相应的计算，最后程序会根据不同的结果来执行相应的控制命令.

图4是对连续层模式的建模，连续模式一开始处于IDLE模式，不会改变任何连续变量的值，当系统进入缓慢下降阶段模式后，它就进入特定冲量模式1，模式中的连续变量按照微分方程的变化规律进行变化直到收到停机信号，如果施加在着陆器上的推力Fc大于3000，则会转移到特定冲量模式2进行相应的变化.当缓慢下降阶段模式结束后，连续模式变化为IDLE，系统的连续变量不再发生变化.

图2 缓慢下降阶段模式图Fig.2 Mode diagram of the slow descent phase

图3 缓慢下降阶段的控制流Fig.3 Control flow in the slow descent phase

该模型较好地描述了着陆器慢速下降的控制系统，既刻画了系统内部的交互行为，又展现了离散状态和连续状态的融合，一定程度上反映了混成语言的准确性与可靠性.

图4 连续变量的模式图Fig.4 Mode diagram of continuous variables

4 结 论

本文研究已有的混成建模语言的特点，整理出混成建模语言的特征和方法，同时结合航天型号软件的特点、以及其运行的物理环境以及解决离散问题的航天需求描述语言SPARDL，设计提出面向航天型号软件的混成建模语言HSPARDL.针对该语言研究了其严格的形式化操作语义，这为航天型号软件建模设计奠定坚实的语义基础.最后针对月球着陆器的慢速下降阶段，用本文提出的语言对其进行了建模，模型能够很好地刻画系统的特点以及状态的交互，进一步展示了HSPARDL的建模能力.

在今后的研究中，一方面还会继续优化更新已有的混成建模语言，深入探讨混成建模语言的代数语义，研究将离散控制行为从系统整体规范分离的代数方法和理论；另一方面，会结合已有的混成系统验证工具如SpaceEx、Flow*、HyTech等，建立相应的翻译规则，将混成语言所建立的模型转换到他们的模型中去，验证各种混合系统的性质，使语言能够为航天型号软件的设计和实现提供更加坚实的理论基础和方法支撑.