基于形式化方法的DIMA动态重构仿真与验证

刘嘉琛, 董 磊,3,*, 赵长啸,3, 陈泓兵

(1. 中国民航大学安全科学与工程学院, 天津 300300; 2. 中国民航大学民航航空器适航审定技术重点实验室, 天津 300300; 3. 天津市民用航空器适航与维修重点实验室, 天津 300300)

0 引 言

随着微电子技术、信息技术和高性能计算技术的迅猛进步,新型航电系统的研发也得到不断促进,目前正朝着分布式综合模块化航空电子(distributed integrated modular avionics, DIMA)系统的方向发展。DIMA利用分布式架构将联合式和模块化航空电子(integrated modular avio-nics, IMA)的系统理念优势进行结合,通过高容错的实时通信网络将所有模块相连,降低了系统和布线的复杂度。与此同时,欧盟FP7框架下的“可扩展可重配置电子平台工具”项目指出先进的航电系统中必不可少的一项技术是具有动态重构能力,这种能力使飞行器可以充分利用功能冗余来进行系统重配置,使其快速适应不同飞行任务模式和资源失效状态。因此,动态重构技术可以减少航电系统对硬件冗余的要求,有效提高了资源的利用率及灵活性。

近年来,国内外研究人员针对航电系统的动态重构做了诸多研究。文献[5]基于动态重构策略及重构过程构建了面向DIMA系统的联合k/n(G)可靠性模型,通过改变功能模块的不同配置研究其对系统可靠度的影响。文献[6]提出了一种基于模型的动态重构分析方法,利用架构分析与设计语言(architecture analysis and design language, AADL)建立了动态重构过程模型并将其转化为有色Petri网进行多约束仿真分析,以证明方法的有效性和正确性。文献[7]提出了一种基于安全性的IMA软件重构方法,利用AADL错误模型附件对运行时的体系结构进行了描述,建立了AADL模型到确定性随机Petri网的映射规则并验证了基于安全性的重构方法的适用性。文献[8]提出了一种分布式的可重构航电系统体系结构,利用AADL语言对平台、应用程序和属性进行建模,还结合模型检验工具对系统可预见的情况进行实时性分析。文献[9]对DIMA系统重构实现机制进行了研究,开发了一种基于DIMA工作流程的调度程序,并基于动态重构演示了故障恢复过程。文献[10]以标准航空电子系统结构联合委员会(Allied Standard Avionics Architecture Council, ASAAC)的系统管理为框架和VxWorks653操作系统的健康监控机制为基础,设计并实现了DIMA平台级和系统级的健康管理方案。文献[11]提出了一种基于分布式通用系统管理的消息交互机制,满足了通用系统管理中多节点、多数据流的消息通信需求,有效减少了系统设计冗余。

可以看出,目前对于DIMA动态重构的研究主要有基于模型的DIMA动态重构可靠性与实时性分析,航电系统体系架构的扩展支持以及DIMA动态重构的机制策略方面。这些研究大多将处理模块内部的动态重构功能性组件交互过程视为黑盒,虽然也有针对通用系统管理的研究,但只停留在机制和理论层面,并未涉及具体的形式化建模、仿真及验证。因此,本文针对可重构DIMA系统在设计初期缺少仿真与验证手段的问题,使用AADL核心语言及其相关附件对DIMA动态重构的建模深入到了通用系统管理(generic system management, GSM)功能性组件层级,设计了基于形式化定义的模型转换规则,形成可执行的时间自动机模型并进行仿真验证。结果表明,本文所提的仿真与验证方法具有可行性和有效性,并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

1 可重构DIMA系统特性分析

在系统科学中,系统并不专指某一特定实体或特定事物,国际系统工程协会对系统给出的定义为:实现一个或多个特定目标的交互元素组合。可重构DIMA系统包括功能软件、硬件、接口和相关功能性组件等元素,可以实现任务-功能-硬件资源的映射,以便清晰地表达动态重构过程中资源模块的调用关系;本文将环境定义为航电系统当前的配置状态,配置状态的改变也是动态重构的触发条件,此时需要通过重新配置来提高飞机的可靠性、保障其安全性;系统与环境还以一定的边界相区分,可重构DIMA系统的边界参考ASAAC及ARINC653标准中提出的软件体系架构,本文与动态重构的相关研究均在此范围内开展。

1.1 可重构DIMA系统映射关系研究

设计一个系统时,首先需要对系统的功能进行定义和划分,然后选择一个能够实现这些功能的体系结构,将功能体系结构映射到系统体系架构中,可重构DIMA系统的映射关系包括软件映射和硬件映射,如图1所示。

图1 可重构DIMA系统的映射关系Fig.1 Mapping relationship of reconfigurable DIMA system

DIMA动态重构是系统在静态配置基础上的一种能力延伸,主要体现在系统运行中资源重新配置的能力。这使得航电系统能依据当前飞行任务、功能需求和可用资源条件进行合理的配置,实现航电功能对现阶段任务模式的最大化支撑和对飞行安全的保证。由于硬件故障是不可逆的,因此动态重构的本质只与软件有关。虽然本文也会对执行平台进行建模,但仿真与验证工作是在其基础上面向软件组件展开的。

1.2 可重构DIMA系统软件体系架构研究

目前航空领域有两种典型的DIMA软件体系架构,分别来自美国航空无线电技术委员会提出的ARINC653标准,以及北约联合标准航空电子系统结构委员会提出的ASAAC标准,其需要实现的两个主要目标为:① 搭建可重构的软件框架;② 建立可重用的应用程序组件。

经对比研究发现,两种标准提出的软件体系架构趋于一致,但仍有各自的特点。ARINC653标准将架构分为应用软件层和核心处理层,核心概念是时空分区及其协调技术,通过APEX接口为应用软件提供实时安全的各类功能服务。ASAAC标准将架构分为应用层、操作系统层和模块支持层,采用4种直接接口和5种逻辑接口实现逻辑通信,通过蓝印系统实现调度控制、配置管理以及健康管理而不是由APEX接口进行控制,还采用了层次化的通用系统管理进一步强化应用软件的功能独立性。总的来说,ASAAC软件体系架构更适用于可重构DIMA系统的应用案例,但在ASAAC标准中分区的定义和有效范围跨越了单个处理模块,这使得ASAAC架构在实现方面比ARINC653架构更为复杂。本文结合以上两种架构的优点,给出了一种经过优化的软件体系架构作为可重构DIMA系统边界,使其同时具备时空分区与层次化的通用系统管理技术,如图2所示。

图2 优化的可重构DIMA系统软件体系架构Fig.2 Optimized software architecture of reconfigurable DIMA system

1.3 DIMA通用系统管理机制研究

GSM在DIMA软件体系结构的核心软件层和应用软件层之间工作,由健康监控(health monitor, HM)、故障管理(failure management, FM)、配置管理(configuration management, CM)和安全管理(safety management, SM)4部分组成。GSM是基于NATO STANAG 4626标准的机载系统管理机制,是实现DIMA动态重构不可或缺的重要组成部分。通用系统管理的功能性组件属于非飞行功能的管理类软件,功能划分如表1所示。

表1 GSM组件功能划分Table 1 Function division of GSM

主动式系统管理会根据需求变化逐层向下分解实施,如任务模式改变等。被动式系统管理会根据状态变化逐层上报处理,如系统资源失效等。GSM功能性组件间的消息传递包括健康监控心跳消息、故障处理信息消息和配置管理动作消息等,相应的触发动作在蓝印系统中定义以供调用,工作流程如图3所示。

图3 GSM的层次化工作流程Fig.3 GSM hierarchical workflow of GSM

2 可重构DIMA系统的AADL建模方法

2.1 AADL概述

AADL是由美国汽车工程师协会于2004年提出的一种面向安全关键系统的建模语言标准,即AS5506标准。AADL模型主要由组件类型、组件实现和属性集等元素构成,支持对软件、硬件和系统3个层次的文本或者图形化建模,旨在实现基于航空标准的嵌入式系统模型的开发工作。AADL在软件体系结构上通过线程、进程、子程序等组件以及组件交互进行描述;在硬件体系结构上通过处理器、虚拟处理器和总线等组件以及组件交互进行描述;功能和非功能属性通过通信协议、模式变换协议以及分区机制等属性进行描述;最后,通过系统组件的组合,能够层次化地建立起系统的体系结构模型。本文使用开源工具环境OSATE(open source AADL tool environment)进行建模,此工具由软件工程师协会开发的基于Eclipse平台的AADL模型建模和分析工具,支持以文本和图形的方式建立并编辑AADL模型。

此外,AADL还支持语义扩展,在AS5506标准的基础上相继颁布了ARINC653 Annex、Behavior ModelAnnex和Error Model Annex等附件,进一步扩展了AADL语言的描述能力,使其更适合具体的建模需求。

2.2 DIMA动态重构的AADL模型

根据前述对可重构DIMA系统特性和AADL建模工具的分析,建立DIMA动态重构到AADL实体的映射规则如表2所示。通过AADL核心语言以及ARINC653 Annex对这些AADL实体进行建模,用虚拟处理器为子组件的处理器表示动态重构中的通用功能模块(common function model, CFM);用绑定到虚拟处理器的进程表示分区;用线程表示功能应用和与动态重构相关的功能性组件以及分区中的功能应用;用端口和端口之间的连接表示模块间和应用间的交互;用数据表示DIMA动态重构策略中各功能应用的资源要求、与其他应用的通讯配置、故障处理动作等信息;再以绑定语法实现系统的软硬件物理资源分配关系,建立可重构的DIMA架构模型;接下来,通过Behavior Model-Annex定义一个状态迁移模型以表征重构过程的迁移和动作,包含变量声明、状态声明和转换声明;将其与模态结合,表示通用功能模块在重构过程的不同配置状态。DIMA动态重构模型用AADL图形化的方式表达如图4和图5所示。

表2 DIMA动态重构到AADL实体的映射规则Table 2 Mapping rules from DIMA dynamic reconfiguration to AADL entities

图4 AADL图形化表示的系统级动态重构模型Fig.4 System level dynamic reconfiguration model based on AADL graphical representation

图5 AADL图形化表示的模块级动态重构模型Fig.5 Module level dynamic reconfiguration model based on AADL graphical representation

需要注意的是,AADL模型中变量选择的依据是系统理论过程分析(systematic theory process analysis, STPA),此方法不再关注组件的故障或可靠性目标是否达到要求,而是在识别不安全控制行为的基础上将安全问题转化为控制问题,更注重系统本身的特点以及多方交互的非线性影响。本文将从3个方面归纳动态重构组件控制行为中可能存在的安全隐患,对应的变量值分别为{1,2,3}:① 未提供控制行为导致危险;② 提供错误的控制行为导致危险;③ 提供可能安全的控制行为但提供节点过早、过晚或顺序错误;④ 控制行为持续太久或过早停止(仅针对持续性控制行为而非离散行为,本文不予考虑)。

2.3 针对动态重构的AADL形式化定义

AADL虽然有确定的语义和严格的语法表达规范,但不可执行性决定了其无法直接仿真模型以评估系统特性。因此,学术界倾向于使用模型转换方法,利用现有的形式化理论或工具间接分析AADL模型。由于本文的目的是通过模型转换生成可执行的DIMA动态重构目标模型,因此源模型的主要关注点为线程和行为模型附件,这两部分的元素已经可以充分表达动态重构过程中的组件交互关系,其形式化定义如下。

AADL线程组件可以定义为一个五元组Th=〈,, Disp, BA, Con〉其中:

(1)={eventport, dataport, eventport}是绑定线程的数据接口、事件端口和数据事件端口的集合;

(2)={×, La}是线程内部数据流flow的表示,La是时延属性Latency的集合,以端口到端口以及转移过程中的时延定义;

(3) Disp表示线程的调度策略,其主要属性有Period、Compute_Execution_Time、Priority等。其中Period为时钟周期,本文默认截止时钟为周期值;

(4) BA表示线程的具体行为,即行为模型;

(5) Con={×,}是线程间端口连接connection的集合,为连接的约束条件。

AADL行为模型附件可以定义为一个六元组BA=〈,,,,,〉,其中:

(1)是状态集合。状态有多种类型,如Initial表示初始状态,Complete表示完成状态,Final表示最终状态,Complete表示该状态可以是一个组合状态;

(2)∈是初始状态的有限集合;

(3)是局部变量的集合,一般为行为附件使用的辅助变量;

(4)是状态转换的使能条件,针对状态变量进行逻辑判断,确定是否进行状态转换;

(5)是状态转换需要执行的动作,包括发送数据,计算等;

3 DIMA动态重构模型转换及仿真验证方法

3.1 时间自动机概述及形式化定义

由于可重构DIMA系统功能性组件交互复杂,且具有周期性、有界响应等与时间相关的系统行为特征。为了研究可重构DIMA系统状态之间的迁移需要满足的时钟约束,本文选择时间自动机作为目标模型。时间自动机理论是在有限状态自动机的基础上扩充时钟、时钟约束和不变条件而得到的,自提出后便一直广泛应用于描述实时系统,有助于对系统体系结构进行分析与验证。UPPAAL是一种基于时间自动机的形式化验证工具,可以通过编辑器、模拟器和验证器构造时间自动机网络模型对实时系统进行建模、仿真和验证。不仅能描述动态重构行为的连续时间特性,还可以体现系统多方交互的特点,实现对可重构DIMA系统特性的模拟与验证。时间自动机的形式化定义如下。

一个时间自动机可以定义为一个六元组TA=〈,,, Var,,〉,其中:

(1)是时间自动机中所有位置(状态)的非空集合;

(2)∈是时间自动机的初始状态;

(3)={clock}是有穷的时钟集合,时钟默认从0开始,每次自增1,且可以在任意时刻被复位为0;

(4) Var是一系列变量的集合;

(5)⊆×Gu×Act××是位置变迁的集合。Gu表示一个使能条件的集合。Act表示输入(记为？)和输出(记为！)的同步信号。是对时钟变量或整型变量的更新操作,在状态变迁的同时完成变量的赋值;

(6)是不变条件,是状态转移约束函数的集合。

时间自动机网络可以定义为一个四元组NTA=〈TA,Var,, Ch〉,其中:

(1) TA=〈TA,TA,…,TA〉是一组相互平行且相互关联的时间自动机;

(2) Var是一系列共享(全局)变量的集合;

(3)是全局时钟的集合;

(4) Ch是同步信道的集合。

3.2 AADL到UPPAAL的模型转换规则设计

不同的模型转换具有不一样的评价标准,寻求统一的向导式规则以供选择最佳的模型转换方式显然是不现实的,但可以借鉴软件工程中的一些基本评价标准。本文拟解决可重构DIMA系统在设计初期缺少安全性评估手段的问题,因此模型转换的主要评价手段是目标模型的行为可达性、逻辑正确性以及模型转换的完整性。两种模型的形式化的语义已在上文明确定义,接下来将具体阐述语义映射的转换规则。

3.2.1 AADL线程到时间自动机的映射

Th→TA/TA对于AADL的每一个线程实现,都转换为一个单独的时间自动机,即UPPAAL中的模板。

La→〈〉对应于时间自动机的时钟变量,可以设置组件内部数据流中几个分段的时延(或整个流的总时延)。

〈,Disp〉→〈(Gu,),〉每个线程内部数据流的时延转换有时钟赋值、不变条件和转移条件3个部分,其中时钟赋值包括时钟clock的重置与变量值的更新,在端口对应状态的进入条件钟设置,其时钟设置为0。

不变条件表示当前位置下恒满足的时钟约束,映射到流延迟属性是线程的最大处理时间,即clock≤max{Compute_Execution_Time}。

转移条件是模板内位置间的转移约束,通常是时钟范围以及共享全局变量的要求,映射到流延迟属性中是数据流的延迟,即clock==Latency。

3.2.2 行为模型附件到时间自动机的映射

〈,〉→〈,〉,时间自动机中以位置表示状态的存在,因此本文将行为模型中的状态声明映射为时间自动机中的位置。同时,行为模型中初始状态作为线程调度执行的最初状态,与对应时间自动机模板中的初始位置相对应,完成状态和最终状态表示线程行为变化的结束。

〈Con,〉→〈Var/Var, Ch〉将AADL行为模型中的变量映射为时间自动机变量Var的集合,端口输出的变量值可以映射为同步信道Ch的集合,Con规定了端口连接的方向。

〈,〉→(Act,)AADL行为附件状态迁移过程的动作对应于时间自动机位置变迁过程发生的动作Act,分为一般动作、端口动作和延时动作3类。一般动作包括变量的赋值和子程序调用,本文将其映射为时间自动机位置变迁过程中的变量更新;端口动作表示线程通过端口输出事件或变量值;延时动作包含delay和computation两种,本文采取computation(clock)表达此动作消耗的计算时间,可以将其作为时间自动机位置迁移的使能条件之一。

3.2.3 基本数据类型的映射

AADL标准语义中已经定义了基本数据类型的package,包括布尔型(boolean)、实型(float)和整型(integer)。时间自动机建模工具UPPAAL的变量声明中主要包含布尔型(bool)、整型(int)、数组类型(array)和结构数据类型(struct)，其映射关系如表3所示。

表3 数据类型映射关系Table 3 Mapping of data types

3.3 DIMA动态重构的时间自动机模型

根据前述的模型转换规则,可以将第2节建立的AADL动态重构模型中的线程和行为模型附件转换为基于UPPAAL的时间自动机模型,如图6所示。时间自动机模型使用AADL模型中定义的变量来区分功能状态,例如变量“XXX_s”表示当前线程的工作状态,取值范围{1,2,3}={正确执行,错误执行,未执行};变量“XXX_o”表示当前线程的输出状态,输入变量为上一个模块的输出变量,取值范围{1,2,3}={正确输出,错误输出,无输出};“XXX_F()”为过程模型函数,表示变量之间的变化关系,其中“XXX”为对应线程状态/位置的名称。

图6 基于时间自动机的DIMA动态重构模型Fig.6 DIMA dynamic reconfiguration model based on timed automata

3.4 时间自动机模型的仿真验证

模型转换工作完成后,利用UPPAAL工具中的模拟器对DIMA动态重构过程进行模拟仿真,生成的DIMA动态重构序列图遵循图3中通用系统管理在功能分区层级的工作流程,表明了模型语义转换的正确性。DIMA动态重构模拟仿真示例如图7所示。再利用巴科斯范式(backus-naur form, BNF)语句对模型需要验证的性质进行描述和验证,BNF是用来描述语法的一种形式体系,是一种典型的元语言,能够严格地表示语法规则,验证语句的含义如表4所示。

图7 DIMA动态重构模拟仿真示例(部分)Fig.7 Example of DIMA dynamic reconfiguration simulation (portion)

表4 BNF验证语句含义

首先验证的是目标模型的系统逻辑和时序正确性,若性质满足则说明GSM各功能性组件均能正常执行,验证结果如表5所示。

接下来,利用BNF语句验证是否存在一条转移路径使得不安全控制行为发生,若性质满足,说明控制行为会发生,反之亦然,以此判断不安全控制行为(unsafe control action, UCA)故障转移路径的可达性。下面以配置管理部分的“加载新配置”功能为例,使用STPA方法识别出了5条不安全控制行为,对其行为可达性进行验证后发现UCA5不满足可达性要求,即此类不安全控制行为不会发生。针对UCA的可达性验证也是对需求的验证,属于安全性工作的一部分,表明了本文的时间自动机DIMA动态重构模型进行STPA安全性分析的可行性,验证结果如表6所示。

表5 系统逻辑及时序正确性验证Table 5 Verification of system logic and time sequence correctness

表6 动态重构行为可达性验证Table 6 Reachability verification of dynamic reconfiguration behavior

4 结 论

本文在分析可重构DIMA软件体系的架构特征及层次化通用系统管理组件功能划分的基础上,利用AADL核心语言、ARINC653附件以及行为模型附件对可重构DIMA系统的架构和动态重构行为进行建模,通过一种形式化的模型转换规则生成了可执行仿真的动态重构时间自动机模型,对目标模型的逻辑及时序正确性和行为可达性的验证结果表明,本文所提方法针对DIMA系统设计初期的模型仿真与验证是可行且有效的。后续研究可将AADL错误模型附件加入到本文所建模型中,进一步展开STPA安全性分析和可靠性分析,对于复杂航电系统的安全性发展具有重要意义。