安全關鍵異構軟件混合建模及代碼生成方法*

宗 喆 ,楊志斌 ,袁勝浩 ,周 勇 ,Jean-Paul BODELEIX ,Mamoun FILALI

1(南京航空航天大學 計算機科學與技術學院,江蘇 南京 211106)

2(高安全系統(tǒng)的軟件開發(fā)與驗證技術工信部重點實驗室(南京航空航天大學),江蘇 南京 211106)

3(IRIT-University of Toulouse,Toulouse 31062,France)

安全關鍵軟件(safety-critical software)[1]是指應用于航空、航天和核能等領域的安全關鍵系統(tǒng)中,且其運行失效會引起系統(tǒng)處于危險狀態(tài),從而導致人員傷害、重大財產損失或者環(huán)境破壞等災難性后果的一類軟件,它對功能正確性、實時性、安全性等性質有極高的要求.隨著系統(tǒng)復雜性的急劇增加,未來安全關鍵軟件越來越多地采用異構構件組合架構,即構件由不同供應商以OEM(original equipment manufacturer)方式提供,各構件可能具有不同特性,例如使用不同的計算模型(狀態(tài)機、同步數(shù)據(jù)流、異步執(zhí)行模型、連續(xù)時間模型等)或實現(xiàn)語言,使得整個軟件系統(tǒng)呈現(xiàn)異構性[2,3].異構軟件系統(tǒng)的執(zhí)行與交互語義也從完全同步發(fā)展到全局異步-局部同步GALS(globally asynchronous locally synchronous)方式,即不同構件具有各自的時鐘控制(稱為多時鐘,multirates),構件之間采用異步通信方式.

近年來,多范式建模方法MPM(multi-paradigm modeling)[4,5]已成為安全關鍵異構軟件設計的研究熱點.多范式建模方法可以通過模型轉換、模型組合、混合建模和混合仿真等方式對軟件系統(tǒng)中使用的不同領域知識、不同視圖以及不同抽象層次進行建模,充分發(fā)揮各種建模語言的描述能力.在安全關鍵系統(tǒng)領域,常用的建模語言主要包括Modelica[6]、SysML[7]、UML Marte[8]、AADL[9]、EAST-ADL[10]、SCADE[11]、Simulink[12]、Ptolemy II[13]等.其中,AADL(architecture analysis and design language)是由美國汽車工程師協(xié)會SAE 提出的面向安全關鍵系統(tǒng)的一種建模語言標準(SAE AS5506).AADL 以層次化構件的方式表達系統(tǒng)的軟硬件架構.一方面,AADL可以非常方便地表達多時鐘、GALS、異步通信等異構軟件特征;另一方面,AADL 提供定義新屬性集和附件(annex)等多種擴展方式,使得AADL 逐漸成為安全關鍵異構軟件多范式建模的重要選擇.

在支持多領域知識的多范式建模方面:Modelica 是一種面向對象的建模語言,用于對大型、復雜和異構系統(tǒng)進行建模,并支持多領域建模.例如,航空航天領域的安全關鍵異構系統(tǒng)涉及機械、電氣、液壓控制等多種領域模型.Sodja 等人[14]提出一種模型簡化技術,對基于Modelica 的信息物理融合系統(tǒng)CPS(cyber-physical system)多領域模型進行模型簡化,以降低基于Modelica 的異構模型的驗證與執(zhí)行過程的復雜性.

在不同抽象層次的多范式建模方面:Hugues 等人[15]提出一種基于SysML 和AADL 的安全關鍵系統(tǒng)設計、驗證及代碼生成方法.其中,SysML 主要用于系統(tǒng)高層建模與分析,當該系統(tǒng)分解給軟件來實現(xiàn)時,就轉換到AADL,用AADL 以逐步求精的方式進行軟件設計與實現(xiàn).Wang 和Hugues 等人[16]則進一步提出面向未來開放式航空電子系統(tǒng)的多范式建模方法,即SysML 用于系統(tǒng)工程建模,轉換到基于AADL 的軟件架構設計,并進一步轉換到基于FACE[17]的開放式航空電子系統(tǒng)架構實現(xiàn)和基于SCADE 的軟件構件功能實現(xiàn).

在支持多種功能行為表達的多范式建模方面:AADL 提供行為附件BA(behavior annex)[18]對基于控制流方式的構件功能行為進行表達;正在制定中的AADL Hybrid Annex[19]則支持基于Hybrid CSP(communicating sequential processes)對構件的連續(xù)行為模型進行構造;Zhan 和Zhan 等人[20]使用AADL 與Simulink 進行混合建模,擴展AADL 描述系統(tǒng)連續(xù)行為的表達能力;歐空局ESA 提出基于AADL、Simulink 和規(guī)范與描述語言SDL(specification and description language)[21,22]的多范式建模方法TASTE[23-25].TASTE 基于AADL 語言子集描述系統(tǒng)框架,并使用Simulink、SDL、C/Ada 等描述系統(tǒng)功能行為,目前,TASTE 主要支持串行Ada 代碼自動生成和集成.

隨著安全關鍵異構軟件對計算性能要求的不斷增加,使用多核處理器成為航空航天領域的迫切需求.我們提出AADL 及行為附件BA、同步語言SIGNAL、SDL、Simulink、C、Ada 的多范式建模方法:AADL 用于表達安全關鍵異構軟件架構,AADL 行為附件BA、同步語言SIGNAL、SDL、Simulink 分別支持狀態(tài)機、同步數(shù)據(jù)流、異步執(zhí)行模型、連續(xù)時間模型等多種計算模型,并基于抽象語法標記ASN.1(Abstract Syntax Notation One)[26,27]對異構模型間的交互數(shù)據(jù)建模.SDL 作為一種異步建模語言,其主要特征是:可以準確描述軟件的異步功能行為,用于表達安全關鍵軟件異步行為.我們在前期研究[28,29]中提出了同步語言SIGNAL 和AADL 的混合建模及多核代碼自動生成方法,本文則主要介紹AADL 和SDL 的混合建模(兩種語言的多范式建模,我們稱其為混合建模)及Ada 多任務代碼生成方法.兩者的區(qū)別在于:同步語言SIGNAL 主要基于數(shù)據(jù)流等式表達AADL構件的功能行為,側重于對數(shù)值計算相關的算法過程進行建模,例如GNC 系統(tǒng)中對地斜開關算法等;而SDL 則側重基于控制流方式表達構件功能行為,側重于對系統(tǒng)控制流程進行建模,如GNC 系統(tǒng)中的航天器三軸姿態(tài)角度修正控制模塊等.

AADL-SDL 混合建模過程可分為自頂向下和自底向上兩個方向:在自頂向下的建模過程中,首先,采用AADL 描述系統(tǒng)體系結構,并基于AADL 數(shù)據(jù)組件描述系統(tǒng)中涉及的數(shù)據(jù)類型;其次,對于具體功能行為采用SDL 模型進行描述,并給出AADL 數(shù)據(jù)組件到ASN.1 的轉換,以保證異構構件間交互數(shù)據(jù)的一致性.而在自底向上的建模過程中,首先,采用SDL 語言描述具體組件功能,并基于ASN.1 描述SDL 模型和外部環(huán)境(即其他組件或系統(tǒng)輸入/輸出)之間的交互;其次,基于AADL 描述系統(tǒng)體系結構,并通過屬性集擴展的方式規(guī)定AADL 體系結構模型和SDL 功能行為模型之間的調用關系和數(shù)據(jù)交換方式.例如,安全關鍵系統(tǒng)已經(jīng)存在多個功能模塊的SDL 模型,如何基于AADL 將這些不同功能模塊自底向上地集成起來,構成完整的系統(tǒng)體系結構模型.

本文考慮自底向上的AADL-SDL 混合建模過程,主要貢獻包括:

(1) 提出一種AADL 與SDL 混合建模方法,包括AADL-ASN.1 和AADL-SDL 擴展屬性集方法.其中,AADL-ASN.1 擴展屬性集主要用于描述混合模型中不同構件間的數(shù)據(jù)類型,AADL-SDL 屬性集用于支持在AADL 體系結構模型中集成SDL 模型對應的功能行為.

(2) 提出一種面向多核處理器的AADL-SDL 混合模型到Ada 多任務代碼生成方法.首先,基于AADL 體系結構模型生成Ada 框架代碼;其次,根據(jù)混合模型中的ASN.1 數(shù)據(jù)屬性生成Ada 數(shù)據(jù)類型代碼.然后,基于混合模型中的線程運行時屬性生成Ada 運行時代碼;最后,基于SDL 模型生成Ada 多任務代碼,并將所有生成代碼進行集成.

(3) 基于AADL 開源建模工具Osate[30,31]實現(xiàn)了AADL-SDL 混合建模工具ASCM(AADL and SDL comodeling tool)和多任務Ada 代碼生成工具AS2MTA(AADL and SDL to multi-task ada code generator),并使用實際工業(yè)案例AOCS 對本文所提方法的有效性進行了分析.

(4) 相較于前期工作,本文擴展了AADL 多范式建?？蚣軐浖刂屏鞒痰拿枋瞿芰?在支持狀態(tài)機、同步數(shù)據(jù)流、連續(xù)時間模型等多種計算模型的基礎上,增加了異步執(zhí)行模型的建模過程.生成的Ada 代碼相較于前期工作,增加了流程控制代碼的并發(fā)過程,提升了代碼的運行效率.

本文第1 節(jié)介紹AADL、SDL 建模語言和ASN.1 標準的基本概念.第2 節(jié)概述面向安全關鍵異構軟件的AADL 多范式建?？蚣?第3 節(jié)對本文提出的AADL-SDL 混合建模方法進行詳細闡述.第4 節(jié)給出AADL-SDL混合模型到多任務Ada 代碼生成方法.第5 節(jié)介紹AADL-SDL 混合建模工具ASCM 和多任務Ada 代碼生成工具AS2MTA.第6 節(jié)通過對工業(yè)界案例導航、制導與控制系統(tǒng)GNC 建模與代碼生成進行分析并與部分前期研究進行比較,對本文所提方法及原型工具進行評估.第7 節(jié)對多范式建模、混合建模和代碼生成相關工作進行分析.第8 節(jié)總結全文,并對未來研究內容進行初步探討.

1 研究背景

1.1 體系結構分析與設計語言AADL

AADL 作為一種針對嵌入式系統(tǒng)的多范式建模語言,通過AADL 構件以及構件之間的連接,從軟件結構、軟件運行時環(huán)境和硬件結構這3 個方面對嵌入式系統(tǒng)體系結構進行建模描述.

1) 軟件結構:支持通過線程、線程組、進程、數(shù)據(jù)、子程序等構件以及連接對軟件的內部結構進行描述.通過上述構件的組合,建立具有層次化的軟件體系結構模型.

2) 軟件運行時環(huán)境:支持通過分發(fā)協(xié)議、通信協(xié)議、調度策略、模式變換協(xié)議以及分區(qū)機制等屬性對軟件執(zhí)行模型進行建模.

3) 硬件結構:支持通過處理器、虛擬處理器、存儲器、外設、總線、虛擬總線等構件以及連接對系統(tǒng)的硬件執(zhí)行平臺進行建模.

此外,AADL 支持基于自定義屬性集(property set)和基于附件的擴展.其中,基于自定義屬性集的擴展支持AADL 構件與多種異構模型之間通過自定義屬性進行關聯(lián),以實現(xiàn)AADL 模型與多種異構模型間的集成.基于附件的擴展支持在AADL 核心構件的基礎上通過增加附件的方式,提升AADL 建模語言的描述能力,例如:Behavior Annex 擴展基于控制流方式的構件功能行為表達能力;Hybrid Annex 擴展AADL 支持對構件的連續(xù)行為模型進行構造;Error Model Annex[32]擴展了AADL 描述系統(tǒng)故障行為的能力.AADL 核心構件、AADL 擴展屬性集和AADL 附件共同組成完整的AADL 模型.

1.2 規(guī)范與描述語言SDL

規(guī)范與描述語言SDL 支持使用半圖形、半文本的方式描述特定類型的嵌入式系統(tǒng)的功能行為.SDL 有圖形表示法GR(graphical representation)和文字短語表示法PR(phrase representation)兩種.其中,GR 用一系列的符號和圖形來描述系統(tǒng),比較直觀;PR 用語句來描述系統(tǒng),便于計算機處理.這兩種表示方法在語義上是等效的,它們之間可以互相轉換.SDL 建模元素主要分為結構元素、定義元素和行為元素.

結構元素:主要用來描述整個系統(tǒng)模型的分層結構,包括系統(tǒng)(system)、功能塊(block)、進程(process)和過程(procedure).圖1 給出了一個SDL 系統(tǒng)模型結構,其中,SDL 系統(tǒng)層包括兩個SDL 功能塊B1 和B2,B1、B2 分別通過SDL 信號c1、c3 與系統(tǒng)外界交互,B1、B2 之間則通過SDL 信號c2 進行交互.SDL 功能塊B1 中進程P1、P2 分別通過SDL 信號R1 和R2 與外界交互,P1 和P2 之間通過信號R3、R4 進行交互.SDL 進程P1 中描述了當前進程的行為,并且定義了SDL 過程Proc1,Proc1 對當前過程的功能行為進行建模.

Fig.1 An example of SDL system model structure圖1 SDL 系統(tǒng)模型結構示例

定義元素:對軟件中需要使用到的各種數(shù)據(jù)(data)、臨時變量(variable)和子功能模塊之間的信號(signal)進行建模描述.

行為元素:對進程(process)/過程(procedure)模塊中的功能行為進行建模.行為元素包括開始狀態(tài)(start)、狀態(tài)(state)、觸發(fā)器(trigger)、行為(action)、表達式(expression)等.其中,開始狀態(tài)和狀態(tài)用來基于自動機的方式對系統(tǒng)行為進行建模;觸發(fā)器包含輸入(input)和保存(save)元素,用來對子系統(tǒng)的中斷行為進行建模,通常與通信信道組合使用,描述中斷信號的傳入和相關數(shù)據(jù)的保存;行為包含輸出(output)、任務(task)過程調用(procedure call)、分支選擇(switch)和進程創(chuàng)建等,主要用來對具體功能行為中需要的輸出操作、順序流程、外部過程調用、分支選擇和進程創(chuàng)建等過程進行建模;表達式(expression)支持以偽代碼的形式對具體行為進行建模描述.

1.3 抽象語法標記ASN.1

ASN.1 作為一種國際標準,用于描述通過電信協(xié)議傳輸?shù)臄?shù)據(jù).ASN.1 提供了一種對數(shù)據(jù)進行表示、編碼、傳輸和解碼的標準格式,能夠有效地對異構系統(tǒng)之間的通信數(shù)據(jù)進行建模.在網(wǎng)絡管理、安全電子郵件、移動網(wǎng)絡和空中交通管制等領域有著廣泛的運用.國際電信聯(lián)盟ITU(International Telecommunication Union)也在標準ITU-T Z.105[33]中推薦在SDL 模型中使用ASN.1 描述數(shù)據(jù)類型.

ASN.1 中定義了整型(INTEGER)、布爾(BOOLEAN)、字符串(IA5String,UniveraslString,…)和位串(BIT STRING)等基本數(shù)據(jù)類型,并且支持有序集合(SEQUENCE)、有序數(shù)組(SEQUENCE OF)、無序集合(SET)和無序數(shù)組(SET OF)等復雜數(shù)據(jù)類型的構造.此外,ASN.1 還支持壓縮編碼規(guī)則PER(packed encoding rule)、可辨別編碼規(guī)則DER(distinguished encoding rule)和XML 編碼規(guī)則XER(XML encoding rule)等數(shù)據(jù)編碼、解碼規(guī)則的描述.因此,ASN.1 也廣泛應用于需要計算機通信和其他需要編碼數(shù)據(jù)的行業(yè).

2 安全關鍵異構軟件的AADL 多范式建?？蚣?/h2>

安全關鍵異構軟件的AADL 多范式建模框架如圖2 所示.核心思路是基于AADL 描述系統(tǒng)體系結構,基于AADL BA、同步語言SIGNAL、SDL、Simulink、C 和Ada 等描述功能行為,以及基于AADL 數(shù)據(jù)構件和ASN.1擴展屬性集描述異構模型間的交互數(shù)據(jù).

Fig.2 AADL multi-paradigm modeling framework圖2 AADL 多范式建模框架

本文主要給出AADL 和SDL 混合建模及面向多核處理器平臺的Ada 代碼自動生成方法,主要涉及圖2 中紅色虛線標注的部分.

(1) 提出一種自底向上的AADL 與SDL 混合建模方法.首先,為了保證AADL 模型與SDL 模型交互數(shù)據(jù)的一致性,提出AADL-ASN.1 擴展屬性集,以支持在AADL 模型中使用ASN.1 進行數(shù)據(jù)建模.其次,為了支持在AADL 模型中使用SDL 描述構件功能行為,提出AADL-SDL 擴展屬性集,主要包括AADL 模型與SDL 模型間的接口映射、多線程調度、線程分發(fā)策略等相關屬性,從而支持AADL 和SDL 的混合建模.

(2) 提出一種面向多核處理器平臺的AADL-SDL 混合模型到Ada 多任務代碼的生成方法.首先,基于AADL 體系結構模型生成對應的Ada 框架代碼;其次,基于AADL 數(shù)據(jù)構件與AADL-ASN.1 屬性集生成Ada數(shù)據(jù)類型代碼;然后,基于AADL 構件與AADL-SDL 屬性集生成Ada 運行時代碼;最后,基于SDL 行為模型生成Ada 多任務代碼,并將所有生成的代碼進行集成.

(3) 基于AADL 開源建模工具Osate 與SDL 開源建模工具OpenGEODE[34]實現(xiàn)了AADL-SDL 混合建模工具ASCM 和Ada 多任務代碼生成工具AS2MTA,并且使用實際的工業(yè)案例GNC 系統(tǒng)對本文所提方法進行評估.

3 AADL-SDL 混合建模方法

本節(jié)主要對AADL-SDL 混合建模方法的具體內容進行詳細介紹.首先,為了支持SDL 模型與AADL 模型間的數(shù)據(jù)交互建模,在第3.1 節(jié)給出AADL-ASN.1 交互數(shù)據(jù)屬性集擴展.其次,在第3.2 節(jié)給出AADL-SDL 混合建模屬性集擴展以支持將SDL 模型以自底向上的方式集成到AADL 架構模型中.

3.1 AADL-ASN.1交互數(shù)據(jù)屬性集擴展

由于SDL 模型通過ASN.1 描述數(shù)據(jù)類型,在進行自底向上的AADL-SDL 混合建模的過程中,為了保證SDL模型與AADL 模型之間數(shù)據(jù)交互的一致性,本文提出AADL-ASN.1 交互數(shù)據(jù)屬性集擴展以支持在AADL 模型中使用ASN.1 進行數(shù)據(jù)建模.該屬性集主要包括對基本數(shù)據(jù)類型和復雜數(shù)據(jù)類型進行建模的相關屬性.其中,基本數(shù)據(jù)類型包括整型(INTEGER)、實數(shù)(REAL)、布爾(BOOLEAN)和字符串(IA5String,UniveraslString,…)等;而復雜數(shù)據(jù)類型包括有序集合(ASN1_Sequence)、有序數(shù)組(ASN1_Sequence_of)、無序集合(ASN1_Set)和無序數(shù)組(ASN1_Set_of)等.

AADL-ASN.1 屬性集擴展的主要屬性見表1.

Table 1 The ASN.1 data properties表1 ASN.1 數(shù)據(jù)性質

其中,屬性Is_Base_Type 支持與AADL 數(shù)據(jù)構件綁定,屬性值的類型為aadlboolean,用于描述當前AADL構件是否為基本數(shù)據(jù)類型.屬性的定義如下:

由于ASN.1 語法中支持通過數(shù)據(jù)范圍定義數(shù)據(jù)類型,因此,在AADL-ASN.1 擴展屬性集中增加了實數(shù)(浮點)取值范圍Real_Value_Range、整數(shù)取值范圍Integer_Value_Range、串長度String_Size、數(shù)組長度范圍Sequence 等屬性.具體定義如下:

ASN.1 支持的數(shù)據(jù)類型包括基本數(shù)據(jù)類型和復雜數(shù)據(jù)類型.具體定義如下:

屬性Support_Data_Type 的類型為枚舉類型,定義了AADL-ASN.1 屬性集支持的所有ASN.1 數(shù)據(jù)類型,作為屬性Data_Type 的屬性值,與Data_Type 組合使用描述數(shù)據(jù)類型.例如,使用Support_Data_Type 中的元素ASN1_Boolean 為Data_Type 賦值,Data_Type=＞ASN1_Boolean 定義了當前AADL 數(shù)據(jù)構件的類型為ASN.1 布爾類型.

除了使用Data_Type 定義數(shù)據(jù)類型,AADL-ASN.1 屬性集還支持對4 種復雜數(shù)據(jù)類型進行詳細描述.需要使用的屬性定義如下:屬性ASN1_Item 是一個record 類型,定義了復雜數(shù)據(jù)類型中的基本元素,即復雜數(shù)據(jù)類型中的成員變量.其中,ID_Value 定義的當前變量在有序集合(ASN1_Sequence)和有序數(shù)組(ASN1_Sequence_of)中的序號,如果是無序的結構,ID_Value 默認值為–1.Name_Value 定義當前變量的變量名,Type_Value 定義當前變量的類型,Default_Value 定義當前變量的默認值.屬性ASN1_Sequence、ASN1_Sequence_of、ASN1_Set 和ASN1_Set_of 分別定義上述4 種復雜數(shù)據(jù)類型.其中,ASN1_Sequence 和ASN1_Set 的屬性值的類型為list,list 中的元素為ASN1_Item.ASN1_Set_of 和ASN1_Sequence_of 的屬性值為record,record 的成員item 類型為list 定義數(shù)組中的元素,成員Type_Value 定義數(shù)組中元素的類型,成員Count 定義數(shù)組中元素的個數(shù),Type_Rename_To 定義引用類型.

3.2 AADL-SDL混合建模屬性集擴展

在第3.1 節(jié)中主要介紹了AADL-ASN.1 交互數(shù)據(jù)屬性集擴展,本節(jié)將給出AADL-SDL 混合建模屬性集擴展的主要內容.在AADL-SDL 混合模型中AADL 構件的功能行為使用SDL 模型表達,SDL 功能行為模型在執(zhí)行過程中的運行時屬性通過AADL-SDL 混合建模屬性集進行建模.屬性集中主要包括SDL 模型運行時的分發(fā)策略、分發(fā)周期等運行時屬性,數(shù)據(jù)構件的操作類型、訪問權限屬性,SDL 行為模型的相關屬性等.AADL-SDL混合建模屬性集擴展的主要內容見表2.

Table 2 Properties of the SDL model表2 SDL 模型相關屬性

屬性Connections_Types 定義AADL 構件間端口數(shù)據(jù)傳輸?shù)念愋?支持立即傳輸(immediate)和延遲傳輸(delay),屬性定義如下:

屬性Supported_Connection_Types 的類型為枚舉類型,定義了兩種支持的連接類型Immediate 和Delay,作為屬性Connection_Types 的屬性值.例如將Supported_Connection_Types 中的Immediate 賦值給屬性Connections_Types,Connections_Types=＞Immediate 定義立即傳輸?shù)臄?shù)據(jù)傳輸連接.

AADL-SDL 支持對周期(periodic)、偶發(fā)(sporadic)、非周期(aperiodic)等線程分發(fā)策略進行建模,具體使用到的屬性如下:

屬性Supported_Dispatch_Protocols 是枚舉類型,作為屬性Dispatch_Protocols 的屬性值支持上述3 種分發(fā)策略.例如,Supported_Dispatch_Protocols 中的Periodic 定義了周期分發(fā)策略,Dispatch_Protocols=＞Periodic 綁定的AADL 線程構件采用的就是周期分發(fā)策略.

屬性Deadline 繼承了AADL 的時間屬性Time,描述AADL 線程的最長執(zhí)行時間.例如,Deadline=＞500ms,當前線程構件的最長執(zhí)行時間為500ms.

屬性Dispatch_Period 描述不同分發(fā)策略下AADL 線程構件的需要描述的時間片段.例如,AADL 線程構件綁定Dispatch_Period=＞10ms,在周期分發(fā)策略下,定義了線程的分發(fā)周期為10ms.在偶發(fā)(sporadic)分發(fā)策略下,定義了相鄰觸發(fā)事件的最小時間間隔為10ms.

屬性Period_Offset 定義了采用周期分發(fā)策略的線程的啟動偏移時間.例如,在未設置當前屬性的周期線程中,默認在系統(tǒng)啟動時就啟動線程.Period_Offset=＞10ms 綁定的線程,在系統(tǒng)啟動后延遲10ms 啟動線程.

除了線程的分發(fā)過程,AADL-SDL 屬性集還支持對數(shù)據(jù)的操作與訪問類型.數(shù)據(jù)的操作類型包含保護數(shù)據(jù)(protected)與非保護數(shù)據(jù)(unprotected).數(shù)據(jù)的訪問類型包括只讀、只寫和讀寫.屬性的具體定義如下所示:

其中,屬性Support_Operation_Kinds 與Support_Permissions 是枚舉類型,分別定義屬性Data_Kind 與Access_Permission 的屬性值.例如,Data_Kind=＞Protected、Access_Permission=＞Read_Only 描述了當前AADL數(shù)據(jù)構件定義的數(shù)據(jù)為保護類型并且只讀.

AADL-SDL 屬性集定義了對SDL 模型的接口描述,以確保AADL 模型能夠與SDL 模型的接口兼容.使用到的主要屬性如下所示:

AADL-SDL 擴展屬性集支持通過SDL system 實現(xiàn)AADL 構件的功能行為,通過SDL signal 實現(xiàn)數(shù)據(jù)交互.其中,屬性Supported_Element_Types 定義了AADL 構件支持的SDL 元素,屬性Element_Name 描述當前AADL構件對應的SDL 實現(xiàn)的名稱,屬性Element_Type 定義了當前構件在SDL 中實現(xiàn)為signal 或system,屬性Source_Language 定義當前構件的具體實現(xiàn).此外,如果AADL 中的數(shù)據(jù)傳輸過程含有參數(shù),則使用屬性Signal_Type 描述參數(shù)的類型.

4 Ada 多任務代碼生成

AADL-SDL 混合模型的Ada 多任務代碼生成主要包括兩個部分:AADL 體系結構模型到Ada 多任務代碼的生成和SDL 功能行為模型到Ada 多任務代碼的生成.本節(jié)將詳細介紹上述代碼生成方法的具體內容.

4.1 AADL模型到Ada多任務代碼生成方法

AADL 模型到Ada 多任務代碼的生成方法主要包括3 個部分.(1) AADL 結構模型到Ada 框架代碼的生成方法;(2) AADL 數(shù)據(jù)構件到Ada 數(shù)據(jù)類型代碼的生成方法;(3) AADL 線程構件到Ada 運行時代碼的生成方法.

4.1.1 AADL 結構模型到Ada 框架代碼的生成方法

AADL 結構模型主要由系統(tǒng)構件、進程構件、線程構件和子程序構件等多種構件組成.AADL 結構模型生成的Ada 框架代碼主要包含多個Ada 過程(procedure)、函數(shù)(function)、任務(task)以及相互之間的調用過程.AADL 系統(tǒng)構件與進程構件對應Ada 代碼中的過程,系統(tǒng)構件和進程構件中的特征(feature)、數(shù)據(jù)子構件(data subcomponent)和連接(connection)分別對應Ada 過程的形參、局部變量和保護對象.AADL 線程構件和子程序構件分別對應Ada 代碼中的任務和函數(shù).Ada 框架代碼中每個Ada 過程、函數(shù)、任務只包含輸入輸出參數(shù)、局部變量聲明與調用關系,不包含軟件功能行為代碼.

4.1.2 AADL 數(shù)據(jù)構件到Ada 數(shù)據(jù)類型代碼的生成方法

AADL 數(shù)據(jù)構件生成Ada 數(shù)據(jù)類型代碼的過程包括如下步驟:首先,AADL 數(shù)據(jù)構件通過綁定AADLASN.1 屬性集對AADL-SDL 混合模型中使用的ASN.1 數(shù)據(jù)類型進行建模,得到AADL 數(shù)據(jù)模型;其次,通過AADL2ASN1 轉換算法生成ASN.1 數(shù)據(jù)文件;然后,通過ASN.1 編譯工具Asn1Scc[35]讀取ASN.1 數(shù)據(jù)文件,并生成對應的Ada 數(shù)據(jù)類型代碼.AADL 數(shù)據(jù)模型到ASN.1 數(shù)據(jù)文件的轉換算法如下所示:

算法輸入為AADL 數(shù)據(jù)模型AADL_Data,輸出為ASN.1 數(shù)據(jù)ASN1_Data.首先獲取AADL 數(shù)據(jù)模型中的全部屬性data_properties(第4 行).通過函數(shù)setConfig 和setType 分別從屬性中解析出ASN.1 數(shù)據(jù)的名稱、ASN.1數(shù)據(jù)文件路徑等配置信息和ASN.1 數(shù)據(jù)的類型,并賦值給ASN1_Data(第5 行～第6 行);其次,通過函數(shù)getIs_Base_Type 獲取屬性Is_Base_Type 的值(第7 行),判斷當前數(shù)據(jù)是否為基本數(shù)據(jù)類型(第8 行).如果是基本數(shù)據(jù)類型,則通過函數(shù)setID、setRange 和setValue 分別獲取ASN.1 數(shù)據(jù)的編號、范圍和默認值,并賦值給ASN1_Data(第8 行～第11 行).如果不是基本數(shù)據(jù)類型,則通過函數(shù)getSubDatas 獲取復雜數(shù)據(jù)類型所有的成員變量,并存入鏈表subdatas 中,遍歷鏈表subdatas,對鏈表中每個元素遞歸調用算法AADL2ASN1,并將返回值添加到ASN1_Data 的成員變量中(第12 行～第18 行).最后,返回ASN.1 數(shù)據(jù)ASN1_Data.

4.1.3 AADL 線程構件到Ada 運行時代碼的生成方法

AADL 線程構件生成的Ada 代碼主要包括兩部分:Ada 運行時代碼和Ada 任務執(zhí)行代碼.其中,Ada 任務執(zhí)行代碼通過SDL 行為模型生成(詳見第5.2 節(jié)),因此本節(jié)主要介紹Ada 運行時代碼的生成.

根據(jù)第4.4 節(jié)中對AADL-SDL 屬性集的介紹,本文提出的AADL-SDL 混合建模方法中,主要支持AADL周期調度、偶發(fā)調度和非周期調度這3 種線程調度策略.

Ada 運行時代碼生成主要采用Ada 語言提供的generic 機制,即提供一種參數(shù)化模板的方式來定義Ada 運行時代碼模板.本節(jié)主要考慮Ada 運行時代碼的生成過程,具體任務功能通過調用SDL 模型生成的SDL_procedure 來實現(xiàn).

AADL 周期線程調度策略生成對應的Ada 周期任務代碼模板APTCT(Ada periodic task code template)見表3.AADL 線程通過屬性 Dispatch_Protocols=＞Periodic 定義當前線程的分發(fā)策略為周期性分發(fā),通過屬性Dispatch_Period=＞TIME(ms)定義當前線程的周期.TIME 用來表示時間數(shù)值.例如,綁定屬性Dispatch_Protocols=＞Periodic 與Dispatch_Period=＞20ms 的AADL 線程對應的Ada 任務通過時間觸發(fā)執(zhí)行,以20ms 為周期,每隔20ms 觸發(fā)1 次.

周期性任務代碼模板的主要參數(shù)包括變量與過程.例如,變量Task_Period 表示任務執(zhí)行周期.過程SDL_procedure 為SDL 行為模型生成的Ada 任務執(zhí)行過程代碼,通過關鍵字in/out 設置Ada 任務執(zhí)行過程的傳入傳出參數(shù).

Table 3 Ada periodic task code template (APTCT)表3 Ada 周期任務代碼模板

AADL 偶發(fā)線程調度策略對應的Ada 偶發(fā)任務代碼模板見表4.AADL 線程通過屬性Dispatch_Protocols=＞Sporadic 定義當前線程的分發(fā)策略為偶發(fā),通過屬性 Dispatch_Period=＞TIME(ms);規(guī)定了任務連續(xù)分發(fā)(dispatch)的最小時間間隔為TIME(ms).例如,綁定屬性Dispatch_Protocols=＞Sporadic 與Dispatch_Period=＞20ms的AADL 線程對應的Ada 任務通過接收外部參數(shù)或者隊列內參數(shù)觸發(fā)執(zhí)行,即如果隊列不為空,那么讀取隊列內數(shù)據(jù)并觸發(fā)過程;如果隊列為空,接收到外部數(shù)據(jù),那么讀取外部數(shù)據(jù)并觸發(fā)任務.并且,由于屬性Dispatch_Period=＞20ms 規(guī)定了觸發(fā)最小時間間隔為20ms,即每次任務執(zhí)行結束后,需要等待20ms 才能從隊列或者外部讀取下一個數(shù)據(jù)并觸發(fā)任務.

Ada 偶發(fā)任務代碼模板ASTCT(Ada sporadic task code template)與Ada 周期任務代碼模板不同,首先,Ada偶發(fā)任務的阻塞發(fā)生在任務體中,通過調用函數(shù)Wait_For_Incoming_Events 監(jiān)聽端口是否有事件到達;其次,計算最小到達間隔時間Minimal_Inter_Arrival 來確保相連相鄰任務分發(fā)之間存在最小時間間隔.

Table 4 Ada sporadic task code template (ASTCT)表4 Ada 偶發(fā)任務代碼模板

AADL 非周期線程調度策略對應的Ada 非周期任務代碼模板AATCT(Ada aperiodic task code template)見表5.

Table 5 Ada aperiodic task code template (AATCT)表5 Ada 非周期任務代碼模板

AADL 線程通過綁定屬性Dispatch_Protocols=＞Aperiodic 定義當前線程的分發(fā)策略為非周期,非周期調度沒有時間屬性.例如,綁定屬性Dispatch_Protocols=＞Aperiodic 的AADL 線程對應的Ada 任務在執(zhí)行過程中通過接收外部參數(shù)或者隊列內參數(shù)觸發(fā)執(zhí)行,通過參數(shù)觸發(fā)執(zhí)行的過程與偶發(fā)調度相同,不同的是偶發(fā)調度設置了觸發(fā)最小時間間隔,而非周期調度沒有.非周期任務只要接收外部參數(shù)或者隊列不為空就會觸發(fā)執(zhí)行.

Ada 非周期任務模板和偶發(fā)任務模板的主要區(qū)別是,前者生成的代碼中沒有最小到達間隔時間Minimal_Inter_Arrival 的限制,當Wait_For_Incoming_Events 監(jiān)聽到事件時,就觸發(fā)當前線程,執(zhí)行當前線程的功能任務.

通過對上述Ada 任務代碼模板設置不同的參數(shù),實現(xiàn)Ada 任務代碼的生成,對于多個任務間的數(shù)據(jù)交互,使用Ada 隊列代碼模板AQCT(Ada queue code template)實現(xiàn)不同任務間的數(shù)據(jù)交互,將隊列創(chuàng)建為Ada 保護類型(protected),以支持多任務調用,Ada 隊列對應的代碼模板聲明如下所示:

其中,queue_size 定義當前隊列容量;Signal_Type 通過參數(shù)化的方式定義隊列中元素的類型;通過進入點put,get 實現(xiàn)入隊出隊操作,put 和get 參數(shù)s為隊列中的元素,t為入隊出隊延遲時間,通過設置參數(shù)t的值,支持在周期不同的任務之間進行數(shù)據(jù)交互;Initialize 實現(xiàn)隊列的初始化操作;Size 獲取當前隊列中的元素個數(shù).

4.2 SDL模型到多任務Ada代碼生成

歐空局ESA 開發(fā)的OpenGEODE 開源工具支持從SDL 模型中生成串行Ada 代碼,在此基礎上,我們提出面向多核的SDL 多任務代碼生成方法.如圖3 所示,首先,將SDL 系統(tǒng)結構(system 和block)轉換為Ada 多任務框架代碼;其次,將SDL 塊結構(block)之間的異步通信(無延遲/延遲)轉換為基于Ada 非延遲/延遲隊列的通信機制,從而支持目標多任務通信;最后,基于分別編譯技術,利用OpenGEODE 將SDL 塊中的進程和過程層編譯為目標Ada 代碼.

首先,圖3 深色部分給出了SDL 系統(tǒng)結構到Ada 多任務框架內代碼的生成.如表6 所示,SDL system 構件轉換為Ada procedure,其中,SDL 模型與環(huán)境的交互轉換為procedure 中的參數(shù),以支持被AADL 模型生成的Ada線程所調用.而SDL 中層次化的Block 結構,將轉換為對應的嵌套Ada Task 結構.

Table 6 Ada code generated from SDL system structure表6 SDL 系統(tǒng)結構生成方法

其次,SDL 異步通信轉換方法包括非延遲通信和延遲通信(如圖3 紅色部分所示).對于SDL 非延遲通信,本文采用Ada 隊列的方式實現(xiàn)SDL 不同塊間采用異步通信機制,具體實現(xiàn)見表7:異步隊列(asyn_queue)定義為保護類型,以保證并發(fā)調用入隊/出隊(put/get)操作過程的正確性.

對于延遲通信,由于實際的延遲取決于真實物理環(huán)境(網(wǎng)絡、線路)中的約束,因此僅定義出隊和入隊操作.為了方便后續(xù)案例的分析與實驗,本文通過對出隊操作進行隨機設置延遲時間訪問,從而實現(xiàn)仿真延遲通信.具體實現(xiàn)見表7,包含參數(shù)傳入和隨機值設置兩種方式,其中,RandomGenerator 函數(shù)用于生成隨機延遲時間(默認范圍為0～10s),delay 表達式用于設置延遲出隊操作.

Fig.3 Ada multi-task code generated from SDL圖3 SDL 到Ada 多任務代碼生成

Table 7 Ada queue code template表7 Ada 隊列代碼模板

最后,對于 SDL 模型中的功能行為(由 process 和 procedure 組成,如圖 3 青色部分所示),本文利用OpenGEODE 已有串行Ada 代碼生成功能,自動生成對應的Ada procedure,并根據(jù)通信類型將其對應接口和異步通信隊列操作相關聯(lián),其中,輸入對應出隊操作,輸出對應入隊操作.

5 原型工具

原型工具主要包含兩部分:AADL+SDL 混合建模工具ASCM(AADL and SDL co-modeling tool)和多任務Ada 代碼生成工具AS2MTA(AADL and SDL to multi-task Ada code generator).

5.1 AADL-SDL混合建模工具ASCM

ASCM 支持AADL+ASN.1 和AADL+SDL 的混合建模功能,支持ASN.1 數(shù)據(jù)文件的生成.ASCM 工具整體框架如圖4 所示.

Fig.4 The structure of ASCM圖4 ASCM 工具結構

ASCM 支持AADL 軟件體系結構建模、ASN.1 數(shù)據(jù)建模和SDL 功能行為建模,并通過ASN.1 屬性集和SDL屬性集實現(xiàn)AADL 體系結構模型、ASN.1 數(shù)據(jù)模型和SDL 功能行為模型這3 種模型的集成,最終實現(xiàn)AADLSDL 的混合建模.其中,對于AADL 體系結構建模ASCM 使用RNL2AADL[36]支持從RNL(restricted natural language)到AADL 架構模型的自動生成.

5.2 Ada多任務代碼生成工具AS2MTA

AS2MTA 支持AADL 模型到Ada 代碼框架的生成、SDL 模型到Ada 行為代碼的生成以及Ada 代碼框架與Ada 行為代碼的集成,AS2MTA 工具的整體框架如圖5 所示.

AS2MTA 主要分為5 個部分.

1) AADL2Ada:基于Ada 代碼生成工具AADL2Ada,AS2MTA 支持AADL 軟件體系結構模型生成Ada 代碼框架.

2) ASN2Ada:基于開源ASN.1 編譯工具Asn1Scc,AS2MTA 支持ASN.1 數(shù)據(jù)類型生成Ada 數(shù)據(jù)定義代碼.

3) SDL2Ada:基于開源SDL 建模工具OpenGEODE,AS2MTA 支持SDL 模型到Ada 任務行為代碼的生成.

4) AS2MTA 支持ASN.1 屬性集與AADL 數(shù)據(jù)構件生成Ada 數(shù)據(jù)訪問接口,以支持Ada 數(shù)據(jù)定義代碼的外部調用.

5) AS2MTA 支持SDL 屬性集與AADL 構件生成Ada 運行時代碼,以支持Ada 框架代碼對多個Ada 任務行為代碼的多任務調度.

Fig.5 The structure of AS2MTA圖5 AS2MTA 工具結構

ASCM 與AS2MTA 通過Java 實現(xiàn),工具的具體模塊與代碼規(guī)模見表8.

Table 8 Statistics of tool implementation表8 工具實現(xiàn)數(shù)據(jù)統(tǒng)計

工具的主要特點包括:

(1) 建模方面:ASCM 工具基于AADL 開源建模工具Osate 進行功能擴展,集成了SDL 開源建模工具OpenGEODE,提供了AADL-SDL 混合建模平臺;擴展了AADL-ASN.1 屬性集和AADL-SDL 屬性集,并集成到ASCM 工具中,支持ASN.1 屬性集與AADL 數(shù)據(jù)構件到ASN.1 數(shù)據(jù)文件的自動生成與同步,簡化了ASN.1 數(shù)據(jù)模型的建模過程,并保證AADL 模型與SDL 模型交互數(shù)據(jù)的一致性.

(2) 代碼生成方面:AS2MTA 基于Ada 代碼生成工具AADL2Ada 進行功能擴展,集成了ASN.1 開源編譯器Asn1Scc 與SDL 開源建模工具OpenGEODE,支持AADL-SDL 混合模型到多任務Ada 代碼的生成.

(3) 系統(tǒng)應用方面:與實際工業(yè)界合作,使用ASCM 工具對GNC 系統(tǒng)進行了AADL-SDL 混合建模,并使用AADL-SDL 混合模型通過AS2MTA 工具生成對應的多任務Ada 代碼.

6 案例分析與方法對比

本節(jié)將使用AADL-SDL 混合建模工具ASCM 和多任務Ada 代碼生成工具AS2MTA 對實際的工業(yè)界案例進行AADL-SDL 混合建模與多任務Ada 代碼生成.并且,在仿真環(huán)境下對生成的多任務Ada 代碼進行運行測試,并與前期研究進行對比分析.最后,結合對比分析結果對本文方法的有效性進行分析評估.

6.1 姿態(tài)軌道控制系統(tǒng)AOCS

導航、制導與控制系統(tǒng)GNC(guidance navigation &control)主要負責航天器姿態(tài)和軌道確定與控制.GNC由導航傳感器(例如,導航相機、星敏傳感器、陀螺儀和加速度計)、姿態(tài)軌道控制系統(tǒng)AOCS(attitude and orbit control system)和執(zhí)行器(例如,反作用飛輪、噴嘴和發(fā)動機)組成.其中,AOCS 主要負責執(zhí)行軌道確定、軌道控制、姿態(tài)確定和姿態(tài)控制等任務.此外,通常需要在導航傳感器和AOCS 之間添加一個數(shù)據(jù)處理單元DPU(data processing unit),用來對導航傳感器發(fā)送的數(shù)據(jù)進行預處理.圖6 所示為GNC 系統(tǒng)的簡化框圖.

Fig.6 GNC system structure圖6 GNC 系統(tǒng)結構

為了方便介紹本文所提出的方法,我們主要以AOCS 為例,詳細介紹AADL-SDL 混合建模方法和Ada 多任務代碼生成方法.AOCS 系統(tǒng)主要包括姿態(tài)確定、姿態(tài)控制、軌道計算和軌道控制等9 個模塊,總計124 個子模塊和21 種計算模式.

6.2 AADL-SDL混合建模

AADL-SDL 混合建模過程主要分為4 個部分.

(1) 基于SDL 對子系統(tǒng)的功能行為建模.

(2) 基于AADL-ASN.1 交互數(shù)據(jù)屬性集對系統(tǒng)中的交互數(shù)據(jù)進行建模.

(3) 基于AADL 對系統(tǒng)體系結構進行建模.

(4) 基于AADL-SDL 混合建模屬性集將SDL 功能行為模型與對應的AADL 構件進行集成.

6.2.1 基于SDL 的功能行為建模

以AOCS 系統(tǒng)中軌道計算模塊的軌道根數(shù)計算(Orbital_Elements_Calculation)為例,詳細介紹SDL 功能行為建模過程.軌道根數(shù)計算的輸入?yún)?shù)包括軌道傾角、軌道角速度、航天器當前時鐘、地面注入時間、軌道遞推初始值等,其計算過程包括長期項計算(Long_Term_Calculation)、短周期項計算(Short_Period_Term_Calculation)、平根數(shù)計算(Mean_Orbit_Elements_Calculation)和瞬根數(shù)計算(Instantaneous_Elements_Calculation)等.對應的SDL 模型結構如圖7 所示.

首先,使用ASN.1 標準對軌道根數(shù)計算過程的數(shù)據(jù)進行建模,以軌道傾角i_0 為例,軌道傾角的數(shù)據(jù)類型為浮點數(shù),范圍為0～180 的閉區(qū)間.因此,定義范圍在0～180 之間的浮點數(shù)類型FLOAT_::=REAL(0..180),并使用該浮點數(shù)類型定義軌道傾角i_0:=FLOAT_.其次,使用SDL 信號(signal)將軌道傾角數(shù)據(jù)從SDL 系統(tǒng)傳遞到SDL功能塊中.軌道傾角的SDL 信號的定義為signal i_0(FLOAT_),參數(shù)的類型與軌道傾角的類型相同.然后,定義讀取軌道傾角并進行相關數(shù)值計算的SDL 功能塊roq,并將signal i_0(FLOAT_)作為roq 功能塊的輸入信號之一.最后,在roq 功能塊內定義roq 參數(shù)計算的SDL 進程,并在SDL 進程內部定義具體計算行為.

6.6.2 基于AADL-ASN.1 交互數(shù)據(jù)屬性集的交互數(shù)據(jù)建模

在AADL-SDL 混合建模過程中,通過AADL-ASN.1 交互數(shù)據(jù)屬性集描述異構模型間的交互數(shù)據(jù).本節(jié)以AOCS 控制系統(tǒng)中的軌道根數(shù)為例,詳細介紹AADL-SDL 混合模型中數(shù)據(jù)類型的建模過程.軌道根數(shù)主要包含軌道傾角(Orbital_Inclination)、升交點黃經(jīng)(Longitude_Of_The_Ascending_Node)、離心率(eccentricity)、近日點輻角(Argument_Of_Perihelion)、半長軸(Semi_Major_Axis)和平近點角(Mean_Anomaly)這6 個必要參數(shù).其中,軌道傾角、升交點黃經(jīng)、近日點幅角和平點近角描述的數(shù)據(jù)使用ASN1_Real 進行建模,其角度范圍為0～180的閉區(qū)間.以軌道傾角數(shù)據(jù)為例,對應的AADL 數(shù)據(jù)構件定義如下所示:

離心率對應的數(shù)據(jù)構件的數(shù)據(jù)類型為浮點數(shù),使用ASN1_Real 進行建模,且離心率的范圍為0～1.因此,為屬性Asn1_Properties::Real_Value_Range 賦值為0.0..1.0.半長軸對應飛行器運行軌道的半長軸,數(shù)據(jù)類型也為浮點數(shù).離心率和半長軸對應的AADL 數(shù)據(jù)構件定義如下:

軌道根數(shù)數(shù)據(jù)構件(Orbital_Elements)的類型為包含6 個元素的無序集合,通過綁定屬性Asn1_Properties::Base_Type=＞ASN1_Set 與Asn1_Properties::ASN1_Set 對Orbital_Elements 的內部結構進行建模,對應的AADL數(shù)據(jù)構件定義如下:

6.2.3 基于AADL 的系統(tǒng)體系結構建模

本節(jié)主要介紹AOCS 系統(tǒng)的AADL 體系結構模型,如圖8 所示.

Fig.8 AADL architecture model of AOCS system圖8 AOCS 系統(tǒng)體系結構模型

AOCS 系統(tǒng)的體系結構模型包括AADL 系統(tǒng)構件(AOCS_Init).在AOCS_Init 構件中定義姿態(tài)確定子系統(tǒng)構件(Pose_Check_Init)、姿態(tài)控制子系統(tǒng)構件(Pose_Control_Init)、軌道計算子系統(tǒng)構件(Orbit_Calculate_Init)和軌道控制子系統(tǒng)構件(Orbit_Control_Init).Orbit_Calculate_Init 構件中定義軌道根數(shù)計算對應的AADL 線程構件Orbital_Elements_Calculation;然后,使用AADL 數(shù)據(jù)構件與AADL-ASN.1 屬性集擴展對各個子系統(tǒng)間的交互數(shù)據(jù)進行建模(見第4.2 節(jié));最后,使用AADL-SDL 屬性集擴展將Orbital_Elements_Calculation與軌道根數(shù)計算過程的SDL 模型進行關聯(lián)(見第4.3 節(jié)).

此外,AOCS 系統(tǒng)的各個子系統(tǒng)構件中的不同功能模塊可采用不同計算模型表達功能行為,并通過擴展屬性集的方式實現(xiàn)多種異構構件與AADL 體系結構模型的集成.例如,針對具有較多數(shù)據(jù)流計算特征的構件使用同步語言SIGNAL 建模(如,姿態(tài)控制子系統(tǒng)中的消除偏模塊[28,29]);針對具有較多控制流特征的構件,可以使用AADL Behavior Annex 的狀態(tài)機進行描述;對于部分構件,可以重用已有的C/Ada 代碼描述;對于具有異步行為特征的構件,可以使用SDL 進行建模(如,軌道根數(shù)計算模塊).

6.2.4 AADL-SDL 模型集成

本節(jié)以AOCS 系統(tǒng)的軌道根數(shù)計算過程為例詳細闡述基于AADL-SDL 混合建模屬性集的AADL-SDL 模型集成過程.首先,通過需求文檔獲取軌道根數(shù)的計算過程的相關參數(shù)與具體的計算行為細節(jié);其次,以第4.3 節(jié)中的軌道根數(shù)數(shù)據(jù)構件Orbital_Elements 作為軌道根數(shù)計算過程的輸入?yún)?shù),對航天器運行過程中的軌道瞬根數(shù)、平根數(shù)等參數(shù)進行周期性的迭代計算,平均執(zhí)行周期為1.5s.

其中,AADL 子程序構件OE_Msg 用來描述軌道根數(shù)計算構件與其他AADL 線程構件間的數(shù)據(jù)交互.交互數(shù)據(jù)的類型為Orbital_Elements,屬性Source_Language=＞SDL 和Element_Type=＞signal 定義當前subprogram 構件對應SDL 模型中的signal.OE_Msg 定義如下:

軌道根數(shù)計算過程對應的AADL構件Orbital_Elements_Calculation 其主要結構如下所示.首先,子程序構件OE_Msg 定義了Orbital_Elements_Calculation 的輸入輸出端口in_msg 和out_msg;其次,屬性Signal_Name 描述了對應的SDL 行為模型的輸入輸出端口為OEC_In 與OEC_Out;然后,屬性dispatch_Protocols=＞Periodic 和Dispatch_Period=＞1500ms 描述了當前線程為周期線程,周期大小為1 500ms.Orbital_Elements_Calculation 的詳細定義如下所示:

6.3 Ada多任務代碼生成

6.3.1 Ada 框架代碼和數(shù)據(jù)類型代碼的生成

首先,基于Ada 代碼生成工具AADL2Ada 生成對應的Ada 代碼框架.然后,基于ASN.1 開源編譯工具Asn1Scc 生成Ada 數(shù)據(jù)類型代碼.AOCS 系統(tǒng)對應的代碼整體結構如圖9 所示,其中,system_satellite_attitude_orbit_control_init_impl 為頂層系統(tǒng),包含功能函數(shù)庫(system_commonfunc_init)、主控系統(tǒng)(system_ctrl_process_init)、軌道計算(system_obtcalmain_init)、軌道控制(system_obtctrl_init)、姿態(tài)確定(system_poscheck_init)和姿態(tài)控制(system_posctrl_init)這6 個子系統(tǒng)和數(shù)據(jù)類型定義(dataview-uniq).其中,主控系統(tǒng)(system_ctrl_process_init)中還包含8 個子功能模塊.

Fig.9 Ada framework code for AOCS圖9 AOCS 系統(tǒng)Ada 框架代碼

6.3.2 Ada 運行時代碼生成

本節(jié)結合第4.1.3 節(jié)給出的Ada 運行時代碼的生成過程,以Orbital_Elements_Calculation 為例進行AADLSDL 混合模型到多任務Ada 代碼的生成.軌道根的計算過程屬于周期執(zhí)行過程,因此,AS2MTA 選用第4.1.3 節(jié)中提到的Ada 代碼模板APTCT 進行代碼生成工作,由于軌道根計算過程的執(zhí)行周期為1 500ms,因此,APTCT的參數(shù)設置可見表9.

Table 9 The parameters of Ada runtime code template in Orbital_Elements_Calculation表9 軌道根計算過程的Ada 運行時代碼模板參數(shù)設置

通過Ada 代碼模板生成對應的運行時代碼,通過隊列模板生成各個任務間的交互代碼.圖10 展示了多個Ada 任務通過Ada 隊列代碼進行任務間的交互過程,AADL 模型中包括軌道根數(shù)計算線程在內一共n個線程構件.以Orbital_Elements_Calculation 線程構件與T2 線程構件為例,Orbital_Elements_Calculation 構件通過Ada周期任務代碼模板APTCT 生成對應的Ada 周期任務代碼Orbital_Elements_Calculation_a.T2 構件生成對應Ada周期任務代碼T2_a.Orbital_Elements_Calculation 構件與T2 構件之間的交互數(shù)據(jù)OE_Msg 通過Ada 隊列代碼模板AQCT 生成Orbital_Elements_Calculation_a 與T2_a 進行交互的隊列代碼OEC_2_T2_Queue.

Fig.10 Ada runtime code圖10 Ada 運行時代碼

6.3.3 SDL 模型到多任務代碼生成

本節(jié)以第6.2.1 節(jié)軌道根數(shù)計算SDL 行為模型為例,詳細介紹SDL 行為模型到Ada 多任務代碼的生成過程.軌道根數(shù)計算SDL 行為模型分別對應于編譯后的部分目標Ada 代碼,見表10.

Table 10 Multi-tasking Ada code from SDL表10 SDL 多任務Ada 代碼

其中,Ada 過程Orbital_Elements_Calculation 根據(jù)SDL 模型中system 組件生成,其參數(shù)列表根據(jù)SDL 模型與環(huán)境交互方向分別使用關鍵字in 和out 進行標注.Orbital_Elements_Calculation 過程中包括25 個Ada task,分別根據(jù)源SDL 模型中的block 組件生成.對于不同塊之間的異步通信,根據(jù)輸入信號對應的塊名聲明對應的延遲隊列.對于塊中的具體功能,基于OpenGEODE 生成對應的Ada 目標代碼.以AQ 塊與U_塊為例,U_過程為U_task 的計算部分,由OpenGEODE 生成.此外,U_task 中還包括兩類特殊的Ada 過程:RI_U_和PI_AQ,其中,PI_U_負責從DP 塊對應的延遲隊列中取數(shù)據(jù),而RI_AQ 負責將計算結果放入AQ 塊對應的延遲隊列中.

6.4 AADL-SDL混合模型分析與評估

首先,使用SDL 對AOCS 系統(tǒng)的軟件功能模塊內部行為進行建模.SDL 模型的統(tǒng)計數(shù)據(jù)見表11.

Table 11 SDL model statistics of AOCS system表11 AOCS 系統(tǒng)SDL 模型統(tǒng)計

其次,使用限定自然語言生成AADL 工具RNL2AADL[36],通過自然語言需求模板對AOCS 系統(tǒng)自然需求文本中的軟件架構信息進行抽取,并通過抽取的軟件架構信息生成AADL 系統(tǒng)體系結構模型,體系結構模型主要包括4 個主系統(tǒng)和309 個軟硬件構件,其中主要包括1 個頂層系統(tǒng)構件、4 個一級子系統(tǒng)構件、125 個二級子系統(tǒng)構件、72 個3 級子系統(tǒng)構件、259 個子程序構件、632 個線程構件.除了描述系統(tǒng)結構的構件外,還包括148 個數(shù)據(jù)構件,主要對整個系統(tǒng)中各個構件之間進行通信交互的數(shù)據(jù)報文建模;1 146 個數(shù)據(jù)訪問連接;902 個外部過程訪問連接.AADL 軟件體系結構模型的統(tǒng)計數(shù)據(jù)見表12.

Table 12 The statistical data AADL model of AOCS system表12 AOCS 系統(tǒng)AADL 模型統(tǒng)計

最后,通過AADL-SDL 擴展屬性集實現(xiàn)上述SDL 功能行為與AADL 體系結構模型的集成.

在第2 節(jié)中,我們提出了AADL 及行為附件BA、同步語言Signal、SDL、Simulink、C、Ada 的多范式建模總體框架,本文主要研究AADL 和SDL 混合建模方法.通過和工業(yè)界的合作與確認,這里選用適用范圍、生成代碼特征等指標對AADL-SDL、AADL-BA[37]、AADL-Signal[28,29]這3 種混合建模方法進行評價,分析結果見表13.

Table 13 The comparison and evaluation of AADL-BA,AADL-Signal,AADL-SDL表13 AADL-BA、AADL-Signal、AADL-SDL 混合模型對比評估結果

如表13 所示,AADL-BA、AADL-Signal 與AADL-SDL 混合建模方法的對比分析結果如下.

(1) 適用范圍:在通過混合模型進行代碼生成的過程中,AADL-BA 通過自動機模型生成代碼,代碼生成過程采用的編程策略以系統(tǒng)的狀態(tài)變化為核心,生成代碼適用于需要進行頻繁狀態(tài)切換的反應式系統(tǒng).AADLSignal 通過數(shù)據(jù)流等式描述數(shù)值的計算過程,具有同步并發(fā)的描述語義,適用于對系統(tǒng)中數(shù)值計算的算法與同步調度算法進行建模與代碼生成.如航天嵌入式系統(tǒng)中的軌道計算、姿態(tài)計算等相關算法.AADL-SDL 側重于描述系統(tǒng)實現(xiàn)過程的流程控制與異步行為,可以清晰地展示出系統(tǒng)不同功能模塊間的流程劃分,實現(xiàn)代碼的解耦,提升各部分代碼的復用性.

(2) 生成代碼特征:針對AADL-BA 混合建模,由于BA 將系統(tǒng)行為抽象為狀態(tài)與狀態(tài)遷移.生成代碼中引入了狀態(tài)機結構,適合對軟件行為中的狀態(tài)變換行為進行建模.針對AADL-Signal 混合建模,Signal 采用數(shù)據(jù)流等式的方式進行建模,模型抽象程度較高,適用于對軟件行為中數(shù)值計算相關的算法內容進行建模.針對AADLSDL 混合建模,SDL 支持對系統(tǒng)行為中的業(yè)務流程與異步控制進行建模.可以準確、清晰地描述出軟件行為中的流程控制行為.

對比分析結果,正是體現(xiàn)了安全關鍵異構軟件系統(tǒng)需要進行多范式建模的必要性.AADL-BA、AADLSignal 及AADL-SDL 混合建模方法能夠較完整地支持安全關鍵異構軟件系統(tǒng)的建模要求.

6.5 生成代碼分析與評估

6.5.1 與AOCS 已有代碼對比分析

首先,針對AOCS 系統(tǒng)AADL-SDL 混合模型,基于AS2MTA 進行多任務的Ada 代碼生成,并且,選取生成代碼規(guī)模和代碼運行時間兩個指標來對本文所提出的方法進行評估.針對這兩個指標,我們分別選取AOCS 系統(tǒng)源代碼和AS2MTA 生成代碼在多核仿真環(huán)境下進行實驗結果統(tǒng)計,其中,AOCS 系統(tǒng)源代碼的相關實驗由實際工業(yè)界進行,并為我們提供處理后實驗結果數(shù)據(jù).實驗具體結果見表14.

通過表14 中的數(shù)據(jù)可知,AS2MTA 生成的代碼規(guī)模比AOCS 系統(tǒng)源碼要大,主要原因包括:(1) 生成多任務運行時;(2) 本文的代碼生成方法還未包含編碼策略的優(yōu)化等過程.

Table 14 The test results of generated code (I)表14 生成代碼運行測試結果(I)

AS2MTA 生成的代碼的平均執(zhí)行時間與AOCS 系統(tǒng)源碼的平均執(zhí)行時間的數(shù)據(jù)統(tǒng)計情況如圖10 所示.

Fig.11 Average code execution time圖11 代碼平均執(zhí)行時間統(tǒng)計

通過分析表14 和圖10,我們得出AS2MTA 生成的代碼的平均執(zhí)行時間與AOCS 系統(tǒng)源碼的平均執(zhí)行時間對比分析結果.相較于單核仿真環(huán)境下AS2MTA 的生成代碼,多核仿真環(huán)境下的生成代碼平均執(zhí)行時間有所提升.但是,與AOCS 系統(tǒng)源碼相比,在運行代碼體量較大的情況下,AS2MTA 生成多任務代碼的運行時間較短.但在運行代碼體量較小的情況下,AOCS 系統(tǒng)源碼的執(zhí)行時間較短.造成這種現(xiàn)象的主要原因可能是,雖然并發(fā)運行多任務代碼會提升運行速率,但是創(chuàng)建多任務的過程會占用部分時間,在運行代碼體量較小的情況下,創(chuàng)建多任務的時間占用了大部分的運行時間,描述功能邏輯的代碼實際運行時間只占用了運行時間的一小部分,代碼的并行執(zhí)行對代碼運行效率產生的提升效果無法彌補創(chuàng)建任務對代碼運行效率產生的降低效果,導致多任務代碼的運行效率低于AOCS 系統(tǒng)源代碼的運行效率.在運行代碼體量較大的情況下,描述功能邏輯的代碼實際運行時間遠大于任務創(chuàng)建時間,則創(chuàng)建任務對代碼運行效率產生的影響就可以忽略不計,并行代碼的運行效率就會高于源代碼的運行效率.未來,我們將對AS2MTA 的生成代碼進行優(yōu)化.

6.5.2 與AADL-BA、AADL-Signal 生成代碼對比分析

本節(jié)針對代碼規(guī)模和代碼運行時間兩個指標,分別選取前期研究中 AADL-BA 混合模型生成代碼與AADL-Signal 混合模型生成代碼和AS2MTA 生成代碼在仿真環(huán)境下進行實驗.實驗具體結果見表15.

Table 15 The test results of generated code (II)表15 生成代碼運行測試結果(II)

AADL-BA 生成代碼、AADL-Signal 生成代碼的平均執(zhí)行時間與AS2MTA 生成代碼的平均執(zhí)行時間的數(shù)據(jù)統(tǒng)計情況如圖11 所示.

Fig.12 Average code execution time圖12 代碼平均執(zhí)行時間統(tǒng)計

通過分析表15 和圖11,AS2MTA 生成的代碼的平均執(zhí)行時間與AADL-BA 和AADL-Signal 生成代碼的平均執(zhí)行時間對比分析結果如下.

1) 單核仿真環(huán)境下的平均執(zhí)行時間:AS2MTA 生成代碼相較于AADL-BA 與AADL-Signal 的生成代碼的平均執(zhí)行時間,是最短的.在單核仿真環(huán)境下運行,多任務并發(fā)對代碼執(zhí)行效率的提升影響較低,影響代碼運行效率的主要因素為代碼結構.AADL-BA 為所有生成代碼引入狀態(tài)機結構,對于功能行為中的狀態(tài)變換,通過狀態(tài)機代碼可以提升運行效率,對于不適用狀態(tài)機的功能行為,則由于狀態(tài)機代碼的結構復雜而降低了代碼的執(zhí)行效率,因此,AADL-BA 的平均執(zhí)行時間最長.AADL-Signal 側重于考慮數(shù)值計算行為中的并發(fā),運行測試也只針對于數(shù)據(jù)計算的代碼實現(xiàn)過程,因此,相較于AADL-BA 代碼的平均執(zhí)行時間有所降低.AADL-SDL 側重于多個控制流程間的并發(fā),在單核仿真環(huán)境下,AADL-Signal 與AADL-SDL 生成代碼的平均執(zhí)行時間沒有明顯差距,AADL-SDL 相較于AADL-BA,由于代碼生成結構的優(yōu)化,縮短了代碼的平均執(zhí)行時間.

2) 多核仿真環(huán)境下的平均執(zhí)行時間:相較于單核仿真環(huán)境,多核仿真環(huán)境下3 種建模方法的生成代碼運行效率都有所提升.與前期研究相比,AS2MTA 生成代碼的平均執(zhí)行時間最短,運行效率最高.并且,通過分析圖10可知,AADL-Signal 側重于數(shù)據(jù)計算過程的并發(fā)行為,姿態(tài)確定和軌道計算兩個模塊的主要內容是航天器各種姿態(tài)參數(shù)與軌道參數(shù)的計算過程.因此,在姿態(tài)確定和軌道計算兩個模塊中,AADL-Signal 生成代碼的運行效率較高,AS2MTA 生成代碼的運行效率沒有明顯提升.但是,姿態(tài)控制與軌道控制模塊的主要職責是根據(jù)參數(shù)對航天器的姿態(tài)與軌道進行調整,代碼結構以流程控制為主,因此,相較于AADL-Signal,使用AS2MTA 生成代碼的執(zhí)行效率有明顯提升,代碼平均執(zhí)行時間大幅度縮短.

7 相關工作

本文的相關工作主要包括3 個方面:多范式建模、混合建模和基于模型的代碼生成.

7.1 多范式建模相關工作

Vangheluwe 在文獻[4]中介紹了多范式建模與仿真,并將多范式建模的研究方向分為3 個部分:(1) 多形式化建模,涉及到描述的不同形式化模型之間的耦合和轉換.(2) 模型抽象,涉及到不同抽象級別上模型之間的關系.(3) 元建模,描述模型的模型.

Mosterman 在文獻[5]中將Vangheluwe 描述的多范式建模方法的3 個研究方向抽象為多范式建模的3 個維度:多抽象、多形式化和元模型.并且,基于這3 個維度引入了領域獨立的多范式建模框架,通過一個混合動力系統(tǒng)的案例,描述了多范式建模方法的統(tǒng)一框架.

Morozov 將多范式建模方法應用在信息物理系統(tǒng)CPS(cyber-physical systems)中[38],使用UML 定義了CPS系統(tǒng)的元模型,并使用汽車噴漆的案例概述了元模型的使用過程.

Blouin 提出了一種對嵌入式系統(tǒng)架構模型進行定量分析的多范式建模語言QAML(quantitative analysis modeling language)[39],QAML 通過利用AADL、SysML、MARTE、AUTOSAR 等多領域建模語言對嵌入式系統(tǒng)架構模型進行定量分析.

Blouin 和Borde 在文獻[40]中提出AADL 作為一種多范式建模語言,由于具有可以擴充其他形式語義的特性,因此可以作為系統(tǒng)多范式建模方法的核心.同時,介紹了ADL 在MPM4CPS 中的應用,并使用一個機器人案例說明AADL 多范式建模的具體用法,描述了自頂向下以AADL 架構模型為中心組合使用SysML、MARTE和UML 等模型,從需求分析開始,然后進行系統(tǒng)設計、設計分析和驗證,最后自動生成代碼的設計流程.

SysML[7]作為一種針對系統(tǒng)工程領域的圖形化建模語言,側重于復雜系統(tǒng)的整體架構.適合在系統(tǒng)開發(fā)生命周期的初期對系統(tǒng)進行需求捕獲、邊界定義、邏輯架構設計等,由于缺乏形式語義,在系統(tǒng)詳細設計與實現(xiàn)階段的應用較少.AADL 基于構件對軟件體系結構進行建模,提供進程、線程、子程序、處理器、外部設備等多種構件,適合在系統(tǒng)開發(fā)生命周期后面的階段進行詳細的設計和具體實現(xiàn).本文提出的混合建模方法主要面向多任務Ada 代碼生成工作,需要對系統(tǒng)詳細設計以及實現(xiàn)細節(jié)進行建模,因此,本文使用AADL 對系統(tǒng)體系結構進行建模.

7.2 混合建模以及代碼生成相關工作

多領域的模型集成作為一種多范式建模方法,不同領域建模語言之間的混合建模過程是多領域的模型集成的重要組成部分.AADL 主要通過擴展附件和混合建模實現(xiàn)多領域的模型集成.

AADL 目前支持Behavior Annex[18]通過集成時間自動機模型對軟件行為中的狀態(tài)控制進行描述;BLESS Annex[41]則在Behavior Annex 的基礎上為自動機添加BLESS Assertions,使其支持自動化的推理證明.Error Model Annex[32]通過集成故障屬性、故障概率等故障模型對軟件行為中的失效事件進行描述;Hybird Annex[19]通過集成Hybrid CSP 對系統(tǒng)物理層的連續(xù)行為進行描述.

Zhan 提出了AADL 與Simulink/Stateflow 混合建模方法[20],相較于Hybrid Annex 對系統(tǒng)物理層連續(xù)行為的描述,Zhan 使用Simulink/Stateflow 描述AADL 系統(tǒng)體系結構模型中物理層的連續(xù)行為,通過contract 對AADL物理層構件進行約束.

Ouni 使用AADL 與Capella 進行混合建模[42],通過INGEQUIP 保持交互信息在不同模型間的一致,通過Capella 描述系統(tǒng)設計初期的功能需求、非功能需求以及平臺約束,并將Capella 模型集成到AADL 模型中,組合兩種模型進行調度分析、行為驗證、結構驗證等工作.

歐空局ESA 提出AADL、Simulink、SDL 的多范式建模方法TASTE[23-25],TASTE 通過AADL 部分子集描述系統(tǒng)體系結構,并通過TASTE 擴展屬性集將AADL 系統(tǒng)體系結構模型與Simulink、SDL 等行為模型進行集成.通過集成代碼生成工具Ocarina[43]進行基于AADL 模型的代碼生成.通過集成Simulink Coder、Qgen、OpenGEODE 等工具實現(xiàn)Simulink、SDL 等行為模型代碼的生成.TASTE 基于OpenGEODE 實現(xiàn)SDL 模型到Ada 代碼的生成,目前主要支持串行Ada 代碼自動生成和集成.本文結合TASTE 的工作,使用分別編譯技術實現(xiàn)了SDL 行為模型到多任務Ada 代碼的自動生成與調度,并且支持與AADL 模型生成Ada 代碼進行集成.

Baouyaa 使用TASTE 工具集對火車控制系統(tǒng)進行建模[44],使用AADL 描述系統(tǒng)體系結構,使用SDL 描述系統(tǒng)行為,并對鐵路系統(tǒng)的相關性質進行了驗證.

在面向安全關鍵軟件的AADL 多范式建模的前期研究中[28,29],我們基于同步語言Signal 對AADL 語義進行了擴展,使用Signal 對AADL 模型中的并發(fā)行為進行了描述,并支持AADL-Signal 混合模型到多任務代碼的生成.本文基于SDL 進一步擴展了AADL 語義,對軟件系統(tǒng)中的異步行為進行了描述,并且實現(xiàn)了AADL-SDL到多任務Ada 代碼的生成.

8 總結與未來工作

本文提出一種AADL 和SDL 混合建模方法,支持以自底向上的方式對安全關鍵軟件系統(tǒng)進行混合建模,并給出面向多核處理器平臺的代碼自動生成方法.首先,提出AADL 與SDL 混合建模方法,包括AADL-ASN.1和AADL-SDL 擴展屬性集方法.其中,AADL-ASN.1 擴展屬性集主要用于描述混合模型中不同構件間的數(shù)據(jù)類型,AADL-SDL 屬性集用于支持在AADL 體系結構模型中集成SDL 模型對應的功能行為.其次,提出面向多核處理器的AADL-SDL 混合模型到Ada 多任務代碼生成方法,包括框架代碼、數(shù)據(jù)類型代碼、運行時代碼以及多任務功能代碼的自動生成.然后,基于AADL 開源建模工具Osate 實現(xiàn)了AADL-SDL 混合建模工具ASCM 和多任務Ada 代碼生成工具AS2MTA,并且使用實際工業(yè)案例對本文所提方法的有效性進行了分析.

在未來的工作中,我們將進一步開展以下3 個方面的研究工作.

1) 工具擴展方面:目前的代碼生成工作依賴于開源SDL建模工具OpenGEODE,因此,AADL-SDL 混合模型中采用的SDL 標準與OpenGEODE 工具保持一致,SDL 標準目前已經(jīng)更新到SDL 2010,未來考慮開發(fā)支持SDL 2010 標準的SDL 建模工具,并實現(xiàn)ASCM 和AS2MTA 到SDL 2010 的移植.

2) 組合驗證方面:研究AADL-SDL 混合模型的形式化組合驗證方法.由于混合模型中存在異步通信,因此需考慮與異步通信有關的形式化驗證.

3) 生成代碼的智能優(yōu)化方面:面對復雜編程場景有時需要依靠編程人員的經(jīng)驗靈活選擇編程策略,未來將研究基于人工智能的編程策略自動優(yōu)化.