面向IMA的AADL多范式建模及代碼自動生成方法

邱 寶，楊志斌，周 勇，謝 健，王鐵鑫，郭 鵬

1(南京航空航天大學 計算機科學與技術(shù)學院，南京 211106) 2(高安全系統(tǒng)的軟件開發(fā)與驗證技術(shù)工信部重點實驗室，南京 211106) 3(航空工業(yè)計算所，西安 710065)

1 引 言

安全關(guān)鍵系統(tǒng)(Safety-Critical System)[1]是指應用于航空、航天、交通、能源等領(lǐng)域的復雜嵌入式系統(tǒng)，且其運行情況可能引起系統(tǒng)處于危險狀態(tài)，從而導致重大財產(chǎn)損失、環(huán)境破壞或者人員傷害.航空電子系統(tǒng)就是一類典型的安全關(guān)鍵系統(tǒng).

航空電子系統(tǒng)經(jīng)歷了獨立式、聯(lián)邦式、綜合化(Integrated Modular Avionics，IMA)[2]以及近期提出的智能開放式(Future Airborne Capability Environment，F(xiàn)ACE)[3]等階段.隨著計算機硬件能力的提高，使得航空電子系統(tǒng)綜合化(IMA)成為可能.IMA是指在統(tǒng)一的硬件處理器上執(zhí)行所有航電功能，為了保證各個航電功能安全執(zhí)行，IMA 引入分區(qū)的概念，每個分區(qū)包含獨立的地址空間、上下文數(shù)據(jù)以及實時任務(wù)，一個分區(qū)的錯誤行為不能影響到其它分區(qū).為了支持在IMA架構(gòu)上的應用軟件開發(fā)，國際航空電子應用軟件接口標準ARINC653(Avionics Application Software Standard Interface)[4]定義了一個多分區(qū)的運行時環(huán)境，并給出了一套通用的航空電子應用軟件標準接口(APEX)以提高機載軟件的模塊化、可重用性和可移植性.目前，Wind River公司的VxWorks653[5]、LynuxWorks的LynxOS-178產(chǎn)品以及Green Hills公司的INTEGRITY-178B以及均采用了該標準，并通過DO178B的A級認證，為上層機載應用軟件提供了高可靠的ARINC653實時操作系統(tǒng).由DDC-I提出的Deos[6]操作系統(tǒng)，是第一個同時支持ARINC653和多核處理器的實時操作系統(tǒng)，并且通過了DO178C的A級認證.國內(nèi)方面，航空工業(yè)計算所設(shè)計與實現(xiàn)的天脈操作系統(tǒng)也能夠完整支持ARINC653標準.IMA存在分布式、異構(gòu)、計算資源和物理資源強耦合等特點，不同分區(qū)的應用功能(例如，大氣數(shù)據(jù)管理、飛行管理、飛控、火控等)可能需要不同的功能行為表達方式.

近年來，多范式建模方法(Multi-Paradigm Modeling，MPM)[7]已成為IMA設(shè)計的研究熱點.多范式建模方法提供了多視角(Multi-View)、多抽象層次(Multi-Abstraction)和多領(lǐng)域(Multi-Domain)異構(gòu)模型的組合與集成.多視角建模是指從系統(tǒng)的功能、非功能、數(shù)據(jù)、硬件、行為等多個視角為系統(tǒng)建模.多抽象層次建模指從需求層、邏輯架構(gòu)層、物理層、執(zhí)行平臺層和應用軟件運行層等不同的層次上從多方面描述正在設(shè)計的安全關(guān)鍵系統(tǒng)，從而支持包括需求分析、設(shè)計、實現(xiàn)、驗證和集成在內(nèi)的系統(tǒng)開發(fā)的過程階段.多領(lǐng)域建模指系統(tǒng)模型可以由不同領(lǐng)域?qū)W科的子系統(tǒng)模型組成，領(lǐng)域?qū)＜铱梢岳貌煌墓ぞ哌M行單獨的建模.

在安全關(guān)鍵系統(tǒng)領(lǐng)域，常用的建模語言主要包括Modelica[8]、SysML[9]、AADL[10]、Simulink、SDL等.其中AADL以層次化構(gòu)件的方式表達系統(tǒng)的軟硬件體系結(jié)構(gòu)，支持功能、非功能、執(zhí)行平臺等多視角建模.AADL 提供定義新屬性集和附件(Annex)等多種擴展方式，使得AADL 逐漸成為安全關(guān)鍵軟件多范式建模的重要選擇.

在AADL多范式建模方面研究主要有：AADL提供Behavior Annex[11]對基于控制流方式的構(gòu)件功能行為表達；正在制定中的AADL HyBrid Annex[12]則支持對構(gòu)件的連續(xù)行為模型進行構(gòu)造；Haolan Zhan 和Naijun Zhan等使用AADL 與Simulink 進行混合建模，擴展AADL 描述系統(tǒng)連續(xù)行為的表達能力[13]；歐空局ESA 提出AADL、Simulink、SDL 的多范式建模方法TASTE[14].

在基于AADL模型的代碼生成方面：Gilles Lasnier[15]等人提出了OCARINA工具，為AADL模型提供了面向IMA的ARINC653平臺相關(guān)的C、Ada代碼自動生成方法，其平臺相關(guān)部分的系統(tǒng)分區(qū)信息以及平臺接口等是通過代碼生成器硬編碼實現(xiàn).Ying Wang等人提出了一種基于ARINC653平臺的RT-Java代碼生成方法，用于復雜的多任務(wù)協(xié)同交互環(huán)境下的航空電子軟件[16].BaekGyu Kim等人提出了一種平臺相關(guān)的C代碼生成框架，使用AADL描述系統(tǒng)的軟硬件體系結(jié)構(gòu)，用代碼片段存儲庫存儲平臺相關(guān)的代碼片段[17].RAMSES[18]提出了一種基于軟件體系結(jié)構(gòu)描述逐級精化的模型驅(qū)動工程(MDE)方法，通過求精將抽象模型轉(zhuǎn)化為包含了執(zhí)行平臺的時序特性的更精確的模型，以方便做系統(tǒng)的可調(diào)度性分析和代碼生成.

本文提出一種面向IMA的AADL多范式建模及代碼自動生成方法——MPM4IMA，本文的研究框架如圖1所示.

圖1 研究框架圖

本文的主要貢獻是：

1)多范式建模方法：首先，AADL用于表達系統(tǒng)軟硬件架構(gòu)；其次，通過擴展屬性集MPM4IMA，使AADL模型能夠使用AADL行為附件BA、SDL[19](Specification and Description Language)和同步語言SIGNAL[20]描述構(gòu)件功能行為，分別支持狀態(tài)機、同步數(shù)據(jù)流、異步執(zhí)行模型等多種計算模型；最后，通過IMA屬性集求精的方式向模型中添加IMA屬性得到平臺相關(guān)的AADL模型.

2)代碼生成方法：給出面向IMA的代碼自動生成規(guī)則，涉及任務(wù)、分區(qū)、內(nèi)核3個層面的代碼自動生成，其中任務(wù)層是描述系統(tǒng)的功能行為，包含SDL、SIGNAL、BA和數(shù)據(jù)構(gòu)件的代碼生成；分區(qū)層主要是為任務(wù)分配資源，包含分區(qū)的初始化、分區(qū)任務(wù)代碼和分區(qū)部署；內(nèi)核層是管理分區(qū)和資源配置來實現(xiàn)安全性和可靠性需求，包含內(nèi)核服務(wù)和內(nèi)核配置文件.

3)工具實現(xiàn)：基于開源工具OSATE對本文所提方法進行原型工具實現(xiàn)，并以航空領(lǐng)域的飛機空氣增壓系統(tǒng)(Airplane Air Compressor System)作為案例，驗證所提方法的可行性和有效性.

本文的結(jié)構(gòu)如下.第2節(jié)介紹ARINC653標準、AADL、SDL和SIGNAL；第3節(jié)介紹面向IMA的AADL多范式建模方法；第4節(jié)介紹面向IMA的AADL模型的代碼生成方法；第5節(jié)介紹方法的原型工具；第6節(jié)基于飛機空氣增壓系統(tǒng)案例對工具進行應用驗證；第7節(jié)對已有的AADL建模和代碼生成相關(guān)工作進行介紹；最后第8節(jié)是對研究工作的總結(jié)和展望.

2 研究背景

2.1 ARINC653

ARINC653標準是一種航空電子應用軟件標準接口規(guī)范，主要定義了基于IMA平臺的應用軟件分區(qū)的操作環(huán)境，其目的是在航電分區(qū)操作系統(tǒng)與應用軟件之間定義一套通用的應用執(zhí)行接口(APEX).

在ARINC653規(guī)范中，每個分區(qū)由一個或多個并發(fā)執(zhí)行的進程組成，共享處理器資源.如圖2所示，ARINC653的體系結(jié)構(gòu)包括應用軟件層、APEX接口層、內(nèi)核軟件層、硬件層4個部分.其中應用軟件層由應用分區(qū)和系統(tǒng)分區(qū)(可選)組成，主要是描述分區(qū)內(nèi)的ARINC653應用進程的并發(fā)執(zhí)行.APEX接口層定義了標準服務(wù)接口以及接口行為，包含分區(qū)管理、進程管理、分區(qū)間通信、分區(qū)內(nèi)通信、健康監(jiān)控、時間管理等服務(wù).核心軟件層通過時間分區(qū)和空間分區(qū)為以上兩層提供安全隔離的分區(qū)運行時環(huán)境和基礎(chǔ)的APEX服務(wù)接口實現(xiàn).

圖2 ARINC653體系結(jié)構(gòu)圖

2.2 AADL

AADL是一種針對嵌入式實時系統(tǒng)的多范式建模語言.它是一種基于構(gòu)件的建模語言，通過軟件構(gòu)件，硬件構(gòu)件和復合構(gòu)件描述系統(tǒng)的軟硬件體系結(jié)構(gòu).其中軟件構(gòu)件用于軟件體系結(jié)構(gòu)建模，包括數(shù)據(jù)、子程序、線程、線程組、進程；硬件構(gòu)件方面，AADL通過處理器、虛擬處理器、存儲器、外設(shè)、總線、虛擬總線等構(gòu)件以及構(gòu)件間的連接來描述系統(tǒng)硬件組成部分的體系結(jié)構(gòu)；復合構(gòu)件指的是AADL的系統(tǒng)構(gòu)件，它組合軟硬件構(gòu)件，層次化地建立系統(tǒng)的體系結(jié)構(gòu).

在AADL核心構(gòu)件的基礎(chǔ)上，AADL還提供了兩種擴展機制，分別是自定義屬性集和擴展附件.自定義屬性集擴展允許為具體的應用或標準提供新的屬性集，例如表達ARINC653標準的分區(qū)屬性，AADL定義了ARINC653屬性集.為了方便表達構(gòu)件內(nèi)部的功能行為，法國IRIT實驗室提出了Behavior Annex(BA)對線程和子程序構(gòu)件的具體行為進行詳細描述[21].

2.3 SDL

規(guī)范與描述語言SDL[19，22]支持使用半圖形、半文本的方式描述特定類型的嵌入式系統(tǒng)的功能行為.SDL 建模元素主要分為結(jié)構(gòu)、定義和行為.結(jié)構(gòu)：主要用來描述整個系統(tǒng)模型的分層結(jié)構(gòu)，包括系統(tǒng)、功能塊、進程和過程.定義：對軟件中需要使用到的各種數(shù)據(jù)、臨時變量和子功能模塊之間的信號進行建模描述.行為：對進程/過程模塊中的功能行為進行建模，包括開始狀態(tài)、狀態(tài)、觸發(fā)器、行為(Action)、表達式等.

2.4 SIGNAL

SIGNAL[20，23]是一種聲明式數(shù)據(jù)流同步語言.基于同步假設(shè)理論，SIGNAL定義了一類對象，稱為信號(Signal)，它是一種帶類型的無限長的值序列.在給定邏輯時刻下，信號可以是“存在”狀態(tài)并具有對應的數(shù)值，或者是“缺失”狀態(tài)，記為⊥.信號處于存在狀態(tài)時，對應邏輯時刻組成的集合構(gòu)成信號對應的邏輯時鐘.在SIGNAL中，兩個信號同步當且僅當其邏輯時鐘相同[22].

SIGNAL 語言通過數(shù)據(jù)流等式進行建模，它提供4 類基本的數(shù)據(jù)流等式結(jié)構(gòu)：1)瞬時函數(shù)(y：=f(x1，x2，…，xn))；2)延遲(y：=x1 MYM init c)；3)條件采樣(y：=x1 when x2)；4)確定性合并(y：=x1 default x2).此外，按照時鐘關(guān)系劃分，4類基本結(jié)構(gòu)可以被分為單時鐘操作(瞬時函數(shù)和延遲)和多時鐘操作(條件采樣和確定性合并)：前者要求所有信號都是同步的，而后者允許信號可以不同步.例如，在確定性合并中，給定邏輯時刻下x1 或者x2 處于存在狀態(tài)即可以保證y 處于存在狀態(tài).

3 面向IMA的AADL多范式建模方法

面向IMA的AADL多范式建模方法主要包含多范式功能建模和IMA屬性集求精兩個部分組成，總體框架如圖3所示.第一部分用AADL表達系統(tǒng)軟硬件架構(gòu)，用BA、SIGNAL及SDL對構(gòu)件功能行為進行表達，第2部分是IMA屬性集求精.

圖3 多范式建模方法框架圖

3.1 多范式功能建模

多范式功能建模主要包括兩個步驟.首先，通過AADL表達IMA的軟硬件架構(gòu)模型；其次，擴展AADL屬性集以支持基于BA、SIGNAL、SDL對構(gòu)件功能行為進行表達.其中，BA是基于控制流方式對線程和子程序構(gòu)件的具體行為進行詳細描述；同步語言SIGNAL是一種聲明式數(shù)據(jù)流同步語言，擅長對系統(tǒng)的同步數(shù)據(jù)流建模，例如用數(shù)學公式所表達的應用功能(傅里葉變換、歐拉角計算等)往往可以通過同步語言來建模；SDL 作為一種異步建模語言，其主要特征是可以準確描述軟件的異步功能行為.

AADL表達IMA的軟硬件架構(gòu)模型，即IMA內(nèi)核層、分區(qū)層和任務(wù)層.內(nèi)核層：用AADL的System構(gòu)件來表達IMA系統(tǒng)；AADL 的Processor構(gòu)件和Memory構(gòu)件分別代表IMA的處理器和內(nèi)存；IMA的分區(qū)間通信有兩種方式采樣和隊列，分別用AADL的Data Port和Event Data Port表示.分區(qū)層：AADL的Process構(gòu)件用于表達IMA分區(qū)的軟件部分，AADL的Virtual Processor表達IMA的分區(qū)運行時(硬件部分)；AADL的Thread表達IMA的任務(wù)，IMA的分區(qū)內(nèi)通信有4種方式即緩沖區(qū)、黑板、信號量和事件，其中緩沖區(qū)用同一進程內(nèi)的Event Data Port表示，黑板用兩個線程共享的Data表示，信號量用Data Access表示，事件用Event Port表示.任務(wù)層：AADL的Subprogram和BA用于表達IMA任務(wù)的功能行為.

定義AADL擴展屬性集MPM4IMA以支持基于SIGNAL和SDL對任務(wù)的功能行為進行表達，如下MPM4IMA屬性集所示.Supported_Languages表示AADL支持的語言擴展；Source_Language表示子程序?qū)崿F(xiàn)的語言類型；Source_Text表示SIGNAL或SDL源文件名；Source_Location表示源文件的路徑.我們給出一個Signal建模示例，如下subprogram所示，表示子程序example.impl的功能行為是用signal實現(xiàn)的，存儲在名為example.sig的文件中，文件的位置在當前目錄的上一級目錄下.

property setMPM4IMAis

Supported_Languages：type enumeration(Ada95，Ada2005，C，Simulink_6_5，Signal，SDL)；

Source_Language：inherit list of MPM4IMA：：Supported_Languages applies to(subprogram，data，thread，thread group，process，system，bus，device)；

Source_Text：aadlstring applies to(subprogram，data，thread，thread group，process，system)；

Source_Location：aadlstring applies to(subprogram，data，thread，thread group，process，system)；

end MPM4IMA；

subprogram implementation example.impl

properties

MPM4IMA：：Source_Language=>(Signal)；

Source_Text=> “example.sig”；

Source_Location=> “..”；

end example.impl

3.2 IMA屬性集求精

通過多范式功能建模構(gòu)造平臺無關(guān)的AADL模型，需要進一步求精為平臺相關(guān)模型.因此提出一種IMA屬性集求精方法，求精的內(nèi)容主要分為3個部分：調(diào)度、分區(qū)通信和任務(wù)運行時屬性.

調(diào)度：在AADL模型中，我們使用處理器和虛擬處理器來分別表示IMA系統(tǒng)運行時及分區(qū)運行時.因此，這里將IMA調(diào)度屬性以求精的方式添加到模型中.IMA系統(tǒng)包括兩條屬性即分區(qū)調(diào)度總時長和分區(qū)調(diào)度窗口，分別對應Processor的兩條屬性：Module_Major_Frame和Module_Schedule；IMA分區(qū)包括分區(qū)調(diào)度協(xié)議、分區(qū)名、分區(qū)ID，分別對應AADL的Virtual Processor的3條屬性：Scheduling_Protocol、Partition_Name、Partition_Identifier.

分區(qū)通信：分區(qū)通信屬性主要包括分區(qū)間通信和分區(qū)內(nèi)通信屬性.分區(qū)間通信：IMA的分區(qū)間通信有兩種方式：隊列和采樣，其中，隊列包含隊列大小、延遲屬性，分別對應AADL的Queue_Size、Timeout屬性；采樣包含端口刷新周期、端口方向和最長消息大小，分別對應AADL的Refresh_Period、in/out、MAX_Message_Size屬性；分區(qū)內(nèi)通信：IMA的分區(qū)內(nèi)通信有4種方式：緩沖區(qū)、信號量、黑板和事件，其中緩沖區(qū)包含的屬性有緩沖區(qū)大小、緩沖區(qū)讀取規(guī)則，分別對應AADL的Queue_Size、Queueing_Discipline屬性；信號量、事件、黑板包含的屬性有延遲，對應AADL的Timeout屬性.我們將這些屬性以求精的方式添加到AADL模型中.

任務(wù)運行時屬性：主要考慮分區(qū)內(nèi)的任務(wù)的相關(guān)屬性，主要包括任務(wù)分發(fā)協(xié)議、任務(wù)周期、任務(wù)優(yōu)先級、任務(wù)的時間容量等，對應AADL線程構(gòu)件的Dispatch_Protocol、Period、Priority、Time_Capacity屬性等.

IMA屬性集求精得到AADL平臺相關(guān)模型，它作為代碼生成器的輸入，接下來介紹代碼生成方法.

4 面向IMA的AADL模型的代碼生成方法

IMA的代碼結(jié)構(gòu)由任務(wù)層、分區(qū)層和內(nèi)核層3個部分組成，結(jié)構(gòu)框架如圖4所示.任務(wù)層是主要是分區(qū)應用，即分區(qū)的功能行為代碼和數(shù)據(jù)結(jié)構(gòu).分區(qū)層主要是為任務(wù)分配資源；內(nèi)核層主要是為分區(qū)分配資源，并對分區(qū)進行調(diào)度.

4.1 任務(wù)層

任務(wù)層代碼生成規(guī)則主要包括BA、SIGNAL、SDL和數(shù)據(jù)構(gòu)件的生成規(guī)則.在我們的前期研究中[24]，給出了同步語言SIGNAL的代碼自動生成方法和工具.因此，本文主要給出BA、SDL的代碼生成規(guī)則.

4.1.1 數(shù)據(jù)構(gòu)件代碼生成規(guī)則

將數(shù)據(jù)構(gòu)件的數(shù)據(jù)類型映射為相應的C語言數(shù)據(jù)類型，數(shù)據(jù)類型分為簡單數(shù)據(jù)類型和數(shù)據(jù)結(jié)構(gòu).

規(guī)則1.AADL簡單的數(shù)據(jù)類型映射到C語言簡單數(shù)據(jù)類型.數(shù)據(jù)標識符轉(zhuǎn)化為相應的C語言變量標識符.表1為簡單數(shù)據(jù)類型的映射示例.

表1 基本類型映射示例

規(guī)則2.AADL數(shù)據(jù)結(jié)構(gòu)映射為C語言的結(jié)構(gòu)體.將數(shù)據(jù)構(gòu)件名稱、數(shù)據(jù)子構(gòu)件名稱和數(shù)據(jù)子構(gòu)件類型映射為結(jié)構(gòu)體名稱、內(nèi)部成員名稱、內(nèi)部成員類型.表2是一個AADL數(shù)據(jù)結(jié)構(gòu)轉(zhuǎn)換示例.

表2 結(jié)構(gòu)體映射示例

4.1.2 BA代碼生成規(guī)則

BA是由局部變量、狀態(tài)和變遷3個部分組成.局部變量映射為C語言函數(shù)的局部變量，具體規(guī)則參照數(shù)據(jù)構(gòu)件映射規(guī)則，狀態(tài)映射為C語言中的枚舉類型，變遷映射為C語言中的switch-case語句.

規(guī)則3.AADL狀態(tài)映射為C語言的枚舉類型，并且給初始狀態(tài)、當前狀態(tài)賦值.

規(guī)則4.AADL變遷映射為switch-case結(jié)構(gòu)，每個狀態(tài)映射為一個case，每個變遷映射為一個if-else結(jié)構(gòu)，變遷的條件守衛(wèi)映射為if-else的條件判斷部分，變遷的行為動作映射為if-else的操作部分.

4.1.3 SDL代碼生成規(guī)則

SDL的代碼生成分為以下3個部分：SDL的結(jié)構(gòu)轉(zhuǎn)換為C語言的功能函數(shù)框架；定義轉(zhuǎn)換為C語言的變量；行為轉(zhuǎn)換為C語言的具體功能行為.

規(guī)則5.

1)結(jié)構(gòu)：SDL中系統(tǒng)轉(zhuǎn)換為<系統(tǒng)名.c>和<系統(tǒng)名.h>文件，功能塊轉(zhuǎn)換為C語言中對應的函數(shù).

2)定義：SDL的聲明的元素轉(zhuǎn)換為C語言中的全局變量；SDL的局部聲明的變量轉(zhuǎn)換為C語言的局部變量.

3)行為：SDL的狀態(tài)代碼生成規(guī)則和BA的狀態(tài)代碼生成規(guī)則一致.

4.2 分區(qū)層

分區(qū)層主要是為任務(wù)分配資源，主要由分區(qū)初始化、分區(qū)任務(wù)代碼和分區(qū)部署文件組成.

4.2.1 分區(qū)初始化

分區(qū)初始化包含任務(wù)的初始化等.IMA的分區(qū)和任務(wù)分別對應AADL的進程構(gòu)件和線程構(gòu)件，本文主要關(guān)注IMA 周期性和非周期性任務(wù)的初始化，對應AADL是周期性和非周期性線程構(gòu)件的代碼生成規(guī)則.

AADL線程根據(jù)dispatch_Protocol屬性區(qū)分線程的類型：Periodic代表周期性線程；Aperiodic代表非周期性線程.

規(guī)則6.周期性任務(wù)的初始化函數(shù)映射為APEX API對應的任務(wù)初始化函數(shù)，周期性任務(wù)的初始化數(shù)據(jù)結(jié)構(gòu)PeriodProcessInit如下，任務(wù)初始化函數(shù)利用PeriodProcessInit數(shù)據(jù)結(jié)構(gòu)對周期性任務(wù)進行初始化.

typedefstruct ProcessInit{

char *threadname；

int *enter_point；

int deadline；

int period；

int time_capacity；

} PeriodProcessInit；

其數(shù)據(jù)結(jié)構(gòu)中的各項分別為任務(wù)名稱、任務(wù)入口地址、任務(wù)截止時間、任務(wù)周期、任務(wù)執(zhí)行時間.

規(guī)則7.非周期性任務(wù)的初始化函數(shù)映射為APEX API對應的任務(wù)初始化函數(shù)，非周期性任務(wù)的初始化數(shù)據(jù)結(jié)構(gòu)AperiodProcessInit如下，任務(wù)初始化函數(shù)利用AperiodProcessInit數(shù)據(jù)結(jié)構(gòu)對非周期性任務(wù)進行初始化.

typedefstruct ProcessInit{

char *threadname；

int *enter_point；

int deadline；

int time_capacity

} AperiodicProcessInit；

其數(shù)據(jù)結(jié)構(gòu)中的各項分別為任務(wù)名稱、任務(wù)入口地址、任務(wù)截止時間、任務(wù)執(zhí)行時間.

4.2.2 分區(qū)任務(wù)代碼

分區(qū)任務(wù)代碼主要IMA任務(wù)的功能映射.

規(guī)則8.針對一個AADL周期性構(gòu)件，入口函數(shù)用<線程實例名_period_jod>來命名，周期性線程的循環(huán)過程映射為入口函數(shù)的while(1)循環(huán)，線程周期性等待映射為wait_next_period()函數(shù)，并把它置于while循環(huán)的末尾.表3是一個周期性任務(wù)的功能映射示例.

表3 周期性任務(wù)的功能映射示例

規(guī)則9.針對一個AADL非周期性構(gòu)件，入口函數(shù)用<線程實例名_aperiodic_job>來命名，在端口捕獲事件映射為wait_Dispatch()函數(shù).表4是一個非周期性任務(wù)的功能映射示例.

表4 非周期性任務(wù)的功能映射示例

4.2.3 分區(qū)部署文件

由于IMA系統(tǒng)每個分區(qū)都是相對的獨立，因此，每個分區(qū)必須保存當前分區(qū)的信息，部署信息會保存在分區(qū)部署文件中.

規(guī)則10.分區(qū)部署文件中包含當前分區(qū)的部署信息，如表5所示，左邊是IMA分區(qū)實體，包含分區(qū)ID、分區(qū)名、分區(qū)調(diào)度策略、任務(wù)總數(shù)、通信端口數(shù)，對應右邊AADL的Partition_Identifier、Partition_Name、Scheduling_Protocol、線程總數(shù)、端口總數(shù)等屬性.

表5 分區(qū)部署信息映射表

4.3 內(nèi)核層

內(nèi)核層的主要功能是管理分區(qū)和資源配置，分為內(nèi)核服務(wù)和內(nèi)核配置文件.

4.3.1 內(nèi)核服務(wù)

IMA的內(nèi)核服務(wù)主要包含分區(qū)管理和分區(qū)間通信.

規(guī)則11.分區(qū)管理主要是獲取當前分區(qū)狀態(tài)，分區(qū)狀態(tài)的結(jié)構(gòu)體如下，包括當前分區(qū)的調(diào)度周期、分區(qū)ID、當前分區(qū)的運行時長，對應AADL的Module_Schedule和Partition_Identifier屬性.

typedefstruct partition{

system_time_type period；

partition_id_type partition_id；

system_time_type duration；

} partition_status_type；

分區(qū)間通信包括采樣和隊列這兩種方式，下面分別介紹采樣和隊列的映射規(guī)則.

規(guī)則12.采樣通信對應AADL的Process構(gòu)件間的Data Port通信，它的結(jié)構(gòu)體如下，包含采樣通信的端口大小、端口方向、刷新頻率屬性，分別對應AADL的MAX_Message_Size、in/out、Refresh_period.

typedefstruct sampling

{

port_size size；//采樣端口大小

port_direction direction；//端口方向

int refresh；//刷新頻率

} port_sampling_status；

規(guī)則13.隊列通信對應AADL的Process構(gòu)件間的Event Data Port通信，它的結(jié)構(gòu)體如下，包含隊列端口方向、消息數(shù)量、隊列大小屬性，對應AADL的in/out、Nb_Message、MaxMessageSize屬性.

typedefstruct queueing

{

port_direction direction；//端口方向

int nb_messages；//消息數(shù)量

port_size size；//隊列大小

} port_queueing_status；

4.3.2 內(nèi)核配置文件

IMA的系統(tǒng)的內(nèi)核配置文件由一個IMA的XML系統(tǒng)配置表組成，系統(tǒng)配置表主要包含以下4個主要元素：分區(qū)表、分區(qū)調(diào)度表、通信表及內(nèi)存分配表.

規(guī)則14.分區(qū)表主要是保存分區(qū)的具體信息，包含分區(qū)名、分區(qū)ID，以及每個分區(qū)里包含的端口的信息，對應AADL的PartitionName、PartitionID、PortName、Direction.

規(guī)則15.分區(qū)調(diào)度表主要是保存分區(qū)的調(diào)度框架，包含一個主時間框架、分區(qū)名、分區(qū)ID、分區(qū)周期、分區(qū)持續(xù)時間、窗口開始的時間，窗口ID，分別對應AADL的Module_Schedule、PartitionName、PartitionID、Module_Schedule.其中Module_Schedule 中包含PeriodSeconds、PeriodDurationSeconds、WindowStartSeconds、WindowID等屬性.

規(guī)則16.通信表主要保存分區(qū)間通信信息，包含端口名稱、端口所在分區(qū)名、端口方向，對應AADL的PortName，PartitionName和端口方向.

規(guī)則17.內(nèi)存分配表主要是保存各分區(qū)的內(nèi)存分配，包含分區(qū)名、分區(qū)ID、分區(qū)內(nèi)存大小，對應AADL的PartitionName、PartitionID、Memory_requirement.

本節(jié)提出IMA的AADL模型到C語言的代碼生成規(guī)則，下面將介紹MPM4IMA工具的具體實現(xiàn).

5 原型工具

5.1 總體框架

MPM4IMA的工具是基于開源工具OSATE開發(fā)的插件項目，借助于OSATE工具的AADL語法分析功能等對AADL模型進行解析，使用Xtend語言模板技術(shù)實現(xiàn)工具.

MPM4IMA的工具分為兩個部分：多范式建模工具和代碼生成工具，圖4是工具的總體框架圖.

圖4 MPM4IMA工具框架

5.2 多范式建模工具

多范式建模工具分為4個部分，如圖5所示：1)AADL模型的樹形結(jié)構(gòu)：首先，用OSATE將模型實例化，然后將實例化模型轉(zhuǎn)換為樹狀結(jié)構(gòu)，并在展示；2)IMA屬性集精化：基于ARINC653屬性集將系統(tǒng)屬性分為調(diào)度、分區(qū)通信和任務(wù)運行時屬性3個部分，并通過手動選擇，為AADL構(gòu)件選擇適當?shù)膶傩裕?)多范式功能建模：選擇BA，SDL或SIGNAL，建模AADL線程和子程序的具體功能行為，所建模型保存在項目的根目錄下；4)操作的結(jié)果展示：2，3的操作步驟的結(jié)果會展示在4里.表6是工具的代碼統(tǒng)計.

圖5 多范式建模工具界面

表6 多范式建模工具數(shù)據(jù)統(tǒng)計

5.3 代碼生成工具

通過OSATE提供的AADL文件解析模塊對文件實例化為aaxl文件，并解析包裝成類，然后借助Xtend提供的模板功能表達AADL到C代碼代碼生成規(guī)則的映射，對文件中的SDL和SIGNAL模型，調(diào)用相應的工具實現(xiàn)代碼生成.表7展示了該原型工具代碼規(guī)模.

表7 代碼生成工具數(shù)據(jù)統(tǒng)計

6 案例分析

6.1 飛機空氣增壓系統(tǒng)簡介

飛機空氣增壓系統(tǒng)(Airplane Air Compressor System，AACS)，是保障飛機正常運行的核心系統(tǒng)，它為飛機供氣增壓，最核心的部件是空氣增壓控制器(Air Compressor Controller，ACC)，它將機上的270V高壓直流電源，采用無刷方式轉(zhuǎn)換成方波或正弦波交流電源，用于驅(qū)動電機運轉(zhuǎn)，從而帶動空壓機工作.

AACS主要功能包括初始化功能、供電功能、控制功能、自檢功能、故障處理功能、存儲功能、輸入功能和輸出功能等7個功能模塊.其中：

?初始化功能，對電路進行初始化和軟件的全局變量進行初始化；

?控制功能主要控制電機，電磁閥和加熱器，將三者的控制指令通過輸出功能傳輸給對應的設(shè)備；

?自檢(BIT)功能由上電BIT和周期BIT組成，上電BIT主要執(zhí)行芯片、處理器、傳感器狀態(tài)等信息的自檢，周期BIT主要執(zhí)行電流，溫度等信息自檢.其中上電BIT在上電時自檢，周期BIT在正常工作、安全保護或失效保護時自檢；

?輸入功能，是將飛行器管理計算機(vehicle management computer，VMC)的指令、溫度傳感器采集的溫度、壓力傳感器采集的壓力還有旋轉(zhuǎn)變壓器采集的角速度和角位置等信息進行接收；

?輸出功能是將周期自檢信息或者將上電自檢信息進行接收，準備傳輸給VMC.將存儲在存儲器中的信息下載到地面檢測設(shè)備中，將控制功能中傳輸過來的控制指令傳輸?shù)酵獠吭O(shè)備，電機，電磁閥，加熱器中從而控制電機的轉(zhuǎn)速，電磁閥的開關(guān)和加熱器的開關(guān)，將接收到的周期自檢或上電自檢信息或者故障情況傳輸給 VMC；

?存儲模式，將電磁閥的開關(guān)次數(shù)，電機壽命，電磁閥壽命，電流等信息進行存儲；

?故障處理，基于不同類別的故障處理指令進行處理.

6.2 飛機空氣增壓系統(tǒng)建模

基于AACS的系統(tǒng)需求，本文將空壓機系統(tǒng)建模分為7個分區(qū)，分別是：自檢(BIT)、輸入、輸出、故障處理、控制、存儲和監(jiān)控.圖6給出了AADL架構(gòu)圖.

圖6 飛機空氣增壓系統(tǒng)的AADL模型

本小節(jié)以飛機空氣增壓系統(tǒng)控制模塊為例介紹多范式建模方法，總體功能結(jié)構(gòu)如圖7所示.控制模塊主要有3個部分組成：電機控制、電磁閥控制和溫度傳感器控制，基于VMC指令的不同，輸入模塊向控制模塊發(fā)出不同的控制指令.本文分別用SIGNAL、SDL、BA對其功能行為建模.

圖7 控制模塊流程圖

當控制模塊接收到溫度傳感器控制的信號，獲取當前溫度傳感器的溫度，如果溫度<4度，依次打開3個加熱器，如果溫度在4度到15度之間，發(fā)出不做溫度調(diào)控操作指令，如果溫度>15，則關(guān)閉3個加熱器，并置加熱器未打開.下面給出溫度傳感器控制模塊的BA建模示例.傳感器控制模塊建模為AADL線程solenoid_value_cmd，BA的局部變量temperature值為傳感器的溫度，然后基于溫度的大小調(diào)用相應的操作.

annex behavior_specification {**

variables

temperature：Base_Types：：Integer；

states

s0：initial state；

s1：final state；

s2：final state；

s3：final state；

transitions

t1：s0-[]→ s0 {temperature：= heater_re_data }；

t2：s0-[temperature<4]→s1{sub1!(heater_func1)}；

t3：s0-[4<=temperature and temperature<=15]→

s2{sub2!(heater_func1)}；

t4：s0-[temperature>15]→s3{sub3!(heater_func1)}；

**}；

當控制模塊接收到電機控制指令時，獲取時間計數(shù)器計數(shù)，通過PID算法得到當前的電機轉(zhuǎn)速并輸出.下面是其SIGNAL模型，2-3行分別是輸入信號t，輸出信號u；第5到7行分別代表比例調(diào)節(jié)函數(shù)、積分調(diào)節(jié)函數(shù)和微分調(diào)節(jié)函數(shù)；第8行是計算電機轉(zhuǎn)速函數(shù)；第10行是局部聲明.

1. process PID=

2. (? integer t；

3. ！integer u；

4. )

5. (|u1：=err(t)；

6. |u2：=f(t)；

7. |u3：=g(t)；

8. |u：=F(u1，u2，u3)；

9. )

10. where integer u1，u2，u3；

11. end；

當控制模塊接收到電磁閥控制指令時，獲取電磁閥的指令，判斷電壓是否是12V，然后向外發(fā)出電磁閥開關(guān)命令.電磁閥控制模塊的SDL模型的block部分如下所示.

BLOCK solenoid_value_cmd；

SIGNALROUTE r

FROM ENV TO solenoid_value_cmd WITH vmc_cmd；

FROM solenoid_value_cmd TO ENV WITH cmd；

CONNECT c AND r；

PROCESS solenoid_value_cmd；

--Text area for declarations and comments

dcl Vol INTEGER；

STATE control；

INPUT VMc_cmd；

CALL get_solenoidcmd；

DECISION Vol=12；

(True)：CALL OPEN；

(False)：CALL CLOSE；

ENDDECISION；

OUTPUT cmd；

NEXTSTATE-；

ENDSTATE；

ENDPROCESS

solenoid_value_cmd；ENDBLOCK；

6.3 代碼生成

AACS系統(tǒng)建模完成得到平臺相關(guān)的AADL模型后，通過OSATE對模型實例化得到aaxl文件，輸入代碼生成工具，可以得到AACS系統(tǒng)的C語言代碼，表8是C代碼的代碼統(tǒng)計.下面的代碼塊是控制模塊的功能行為代碼，包括BA、SIGNAL、SDL生成的代碼.

表8 AACS系統(tǒng)代碼統(tǒng)計

7 相關(guān)工作

7.1 多范式建模

AADL 目前支持Behavior Annex[11]通過基于自動機模型對軟件行為中的狀態(tài)控制進行描述；Hybird Annex[12]通過集成Hybrid CSP 對系統(tǒng)物理層的連續(xù)行為進行描述.

文獻[13]提出AADL 與Simulink/Stateflow 混合建模方法，使用Simulink/Stateflow描述AADL 系統(tǒng)體系結(jié)構(gòu)模型中物理層的連續(xù)行為，通過contract對AADL物理層構(gòu)件進行約束.

struct pid SIGNAL

{

float SetSpeed；

float ActualSpeed；

float err；

float err_last；

float Kp，Ki，Kd；

float voltage；

float integral；

}pid；

int pid_calculate(int t)

{

int count=0；

pid_value_init()；

while(count < 1000)

{

float speed=PID_realize(200.0)；

cout <<"value is " <<

speed<

count++；

}

system("pause")；

}

float PID_realize(float speed)

{

pid.SetSpeed=speed；

pid.err=pid.SetSpeed-pid.Actual-

Speed；

pid.integral+=pid.err；

pid.voltage=pid.Kp * pid.err

+pid.Ki*pid.integral+pid.Kd*(pid.err-pid.err_last)；

pid.err_last=pid.err；

pid.ActualSpeed=pid.voltage*1.0；

return pid.ActualSpeed； int heater(Cmd heater_re_data){ BA

int temperature；

enum State{s0，s1，s2，s3}；

enum State initialState=s0；

enum State finalState=s3；

enum State current_state=initial

State；

while(1){

switch(current_state){

case s0：

temperature=heater

_re_data.temperature；

break；

case s1：

if(temperature<4){ heater_func1()；

}

break；

case s2：

if(4≤temperature≤15){

heater_func2()；

}

break；

case s3：

if(temperature>15){

heater_func3()；

}

break；

default：

break；

}

}

}

Int control(Cmd vmc_cmd){ SDL

enum states_t{running，wait}；

enum State initialState=running；

enum State finalState=wait；

enum State current_state=initialState；

int result=0；

int vol=vmc_cmd.vol；

while(1){

switch(current_state){

case running：

vol=get_solenoidcmd()；

if(vol==12)

open()；

else

{

close()；

}

break；

case wait：

return；

default：

return-1；

}

}

result=control_solenoidcmd()；

return result；

}

文獻[14]歐空局ESA 提出AADL、Simulink、SDL 的多范式建模方法TASTE，TASTE 通過AADL 部分子集描述系統(tǒng)體系結(jié)構(gòu)，并通過TASTE 擴展屬性集將AADL 系統(tǒng)體系結(jié)構(gòu)模型與Simulink、SDL 等行為模型進行集成.通過集成代碼生成工具Ocarina進行基于AADL 模型的代碼生成.通過集成Simulink Coder、Qgen、OpenGEODE等工具實現(xiàn)Simulink、SDL 等行為模型代碼的生成.

7.2 代碼生成相關(guān)

文獻[15]是法國ENST開發(fā)的OCARINA工具，它實現(xiàn)了從AADL模型自動生成代碼.該工具中使用的代碼生成算法針對的是單一平臺POLYORB和POLYORB-HI，方法是將編程接口和平臺相關(guān)的代碼硬連接到生成算法中.因此，高級模型和源代碼之間存在較大的語義上的差異.

文獻[16]提出一種基于ARINC653架構(gòu)的AADL模型的自動RT-Java代碼生成方法，該方法將AADL模型映射為RT-Java編程模型，并給出了一種適用于多任務(wù)協(xié)作的RT-Java代碼生成算法.

文獻[17]提出一種AADL模型和代碼片段存儲庫顯式指定目標平臺的平臺相關(guān)特性的代碼生成框架，該框架提供選擇不同目標平臺的靈活性.但該方法只能保證模型功能性的正確性，在早期模型分析階段并不能保證其非功能性質(zhì)的驗證.

RAMSES[18]提出一種基于軟件體系結(jié)構(gòu)描述逐級精化的模型驅(qū)動工程(MDE)方法，首先提出一種模型精化和時序分析框架，主要是通過求精將抽象模型轉(zhuǎn)化為包含了執(zhí)行平臺的時序特性的更精確的模型，以方便做系統(tǒng)的可調(diào)度性分析和代碼生成.

Le Sergent等人提出的SCADE是目前國內(nèi)外工業(yè)界使用最廣泛的模型驅(qū)動工具之一，其對功能模塊強大的建模描述能力得到了廣泛的認可，并且該工具支持將其工具上設(shè)計的模型自動轉(zhuǎn)換到Ada、C代碼，不過其生成的代碼并不包含平臺相關(guān)信息，不具備靈活性，需要工程師后期手動將代碼集成到執(zhí)行代碼中[25].

8 結(jié)束語

本文提出了一種面向IMA的AADL多范式建模及代碼自動生成方法.首先，提出面向IMA的AADL多范式建模方法，包括：

1)使用AADL表達系統(tǒng)軟硬件體系結(jié)構(gòu)；

2)通過擴展屬性集，以支持基于BA、SIGNAL、SDL對構(gòu)件功能行為進行表達；

3)通過IMA屬性集求精的方式向模型中添加IMA屬性得到平臺相關(guān)的AADL模型.其次，提出面向IMA的AADL代碼自動生成方法，包括3個層次的代碼轉(zhuǎn)換：

1)任務(wù)層是描述系統(tǒng)的功能行為，包含SDL、SIGNAL、BA和數(shù)據(jù)構(gòu)件的代碼生成；

2)分區(qū)層是為任務(wù)分配資源，包含分區(qū)的初始化、分區(qū)任務(wù)代碼、分區(qū)部署；

3)內(nèi)核層是管理分區(qū)和資源配置來實現(xiàn)安全性和可靠性需求，包含內(nèi)核服務(wù)和內(nèi)核配置文件.最后，基于開源工具OSATE對本文所提方法進行原型工具實現(xiàn)，并以航空領(lǐng)域的飛機空氣增壓系統(tǒng)(Airplane AirCompressor System)作為案例，驗證所提方法的可行性和有效性.

在未來的工作中，我們將進一步考慮IMA系統(tǒng)的健康監(jiān)控功能，IMA的健康監(jiān)控功能是處理系統(tǒng)發(fā)生的錯誤，以后可以考慮通過AADL的error model表達健康監(jiān)控功能.另外，我們正在研究面向IMA系統(tǒng)的AADL模型組合驗證方法.