袁 翔,胡 軍,2,馬金晶,劉 雪

(1.南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,南京210016;

2.南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室,南京210093)

基于AADL的綜合航電分區(qū)系統(tǒng)可調(diào)度性判定

袁 翔1,胡 軍1,2,馬金晶1,劉 雪1

(1.南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,南京210016;

2.南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室,南京210093)

綜合模塊化航電(IMA)系統(tǒng)中的分區(qū)系統(tǒng)提高了其可靠性和安全性,但在系統(tǒng)設(shè)計(jì)和實(shí)現(xiàn)過程中,應(yīng)采用各種分析和驗(yàn)證方法確保系統(tǒng)的時(shí)間需求得到滿足。為此,針對(duì)符合ARINC653規(guī)范的IMA系統(tǒng),根據(jù)分區(qū)系統(tǒng)層級(jí)調(diào)度的特性,提出一種基于仿真的分區(qū)任務(wù)集可調(diào)度性判定方法。借助Cheddar工具及其自定義調(diào)度策略功能,使架構(gòu)分析和設(shè)計(jì)語言(AADL)具有對(duì)分區(qū)系統(tǒng)進(jìn)行建模的能力,并利用該工具對(duì)AADL模型進(jìn)行仿真以判定系統(tǒng)的可調(diào)度性。實(shí)例分析結(jié)果表明,該方法能自動(dòng)、準(zhǔn)確、快速地進(jìn)行可調(diào)度性判定,并以甘特圖的方式繪制任務(wù)調(diào)度過程,得到直觀、詳細(xì)的結(jié)果。

綜合模塊化航電;ARINC653系統(tǒng);分區(qū)系統(tǒng);架構(gòu)分析和設(shè)計(jì)語言;Cheddar工具;可調(diào)度性判定;仿真方法

1 概述

綜合模塊化航電(Integrated Modular Avionics, IMA)系統(tǒng)[1]是航空應(yīng)用領(lǐng)域中的一類重要系統(tǒng)結(jié)構(gòu)。ARINC653標(biāo)準(zhǔn)[2]定義了一種IMA軟件體系結(jié)構(gòu),制定了操作系統(tǒng)層和應(yīng)用軟件層之間的標(biāo)準(zhǔn)接口(APEX)。標(biāo)準(zhǔn)滿足ARINC653的IMA系統(tǒng)稱為ARINC653系統(tǒng)。

ARINC653系統(tǒng)提出了分區(qū)操作系統(tǒng)的概念,用來提高航空電子系統(tǒng)的可靠性、高安全性。為保障系統(tǒng)的安全性和可靠性,在系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)過程中,應(yīng)采用各種分析、建模及驗(yàn)證方法對(duì)系統(tǒng)進(jìn)行嚴(yán)格的檢驗(yàn),以保證系統(tǒng)在各種情況下的非功能需求和時(shí)間需求都能得到滿足。為了精確管理時(shí)間資源,以達(dá)到強(qiáng)實(shí)時(shí)性要求,對(duì)系統(tǒng)進(jìn)行可調(diào)度性分析相當(dāng)必要。

架構(gòu)分析和設(shè)計(jì)語言(Architecture Analysis and Design Language,AADL)[3]是一種針對(duì)嵌入式系統(tǒng)建模描述語言,可應(yīng)用于航空嵌入式系統(tǒng)(ARINC653系統(tǒng))的架構(gòu)設(shè)計(jì)建模及分析[4]。Cheddar是一款實(shí)時(shí)調(diào)度分析工具[5],可應(yīng)用于實(shí)時(shí)系統(tǒng)的時(shí)間性驗(yàn)證,同時(shí)支持對(duì)AADL模型表示的實(shí)時(shí)系統(tǒng)進(jìn)行可調(diào)度性分析。

鑒于ARINC653分區(qū)調(diào)度系統(tǒng)具有層級(jí)性(分為兩級(jí)調(diào)度),且目前支持多層級(jí)調(diào)度分析的方法和工具并不完善,本文提出一種基于AADL模型,使用Cheddar工具對(duì)ARINC653分區(qū)調(diào)度系統(tǒng)進(jìn)行可調(diào)度性判定的方法。首先利用AADL模型和Cheddar關(guān)于AADL的擴(kuò)展屬性對(duì)分區(qū)系統(tǒng)進(jìn)行建模,再通過Cheddar工具對(duì)生成的AADL模型進(jìn)行可調(diào)度性判定。

2 背景知識(shí)

2.1 ARINC653

ARINC653是一種IMA軟件體系結(jié)構(gòu),如圖1所示,它包括如下層次結(jié)構(gòu):應(yīng)用軟件層,ARINC653系統(tǒng)結(jié)構(gòu)層,實(shí)時(shí)操作系統(tǒng)層,硬件接口層和硬件層。系統(tǒng)的功能要求包括分區(qū)管理、進(jìn)程管理、時(shí)間管理、存儲(chǔ)器管理、分區(qū)內(nèi)通信、分區(qū)間通信及健康監(jiān)控等功能定義[2]。

圖1 ARINC653軟件體系結(jié)構(gòu)

本文的研究重點(diǎn)在應(yīng)用軟件層,它按資源分配和功能將系統(tǒng)劃分為數(shù)個(gè)模塊,模塊又劃分為數(shù)個(gè)分區(qū),分區(qū)內(nèi)包含具體的任務(wù)進(jìn)程。通過引入分區(qū)概念,將模塊分為若干個(gè)分區(qū),每個(gè)分區(qū)分配指定的內(nèi)存空間和處理器時(shí)間片。

關(guān)于分區(qū)的時(shí)間調(diào)度方面,一個(gè)ARINC653系統(tǒng)模塊中有若干分區(qū),每個(gè)分區(qū)下對(duì)應(yīng)著各自的任務(wù)集合。將系統(tǒng)處理器時(shí)間按時(shí)間片的方式分配給各個(gè)分區(qū),各個(gè)分區(qū)下的任務(wù)集合在相應(yīng)分派的時(shí)間片下運(yùn)行,當(dāng)時(shí)間片用完時(shí)暫停執(zhí)行,直到下一個(gè)時(shí)間片的到來。不同于普通的系統(tǒng)調(diào)度模型,分區(qū)調(diào)度模型包含兩級(jí)調(diào)度策略,如圖2所示。

圖2 ARINC653分區(qū)系統(tǒng)調(diào)度框架

(1)分區(qū)間調(diào)度。分區(qū)間的調(diào)度是第1級(jí)調(diào)度,調(diào)度周期是固定的。每個(gè)分區(qū)周期性地分配到處理器時(shí)間。

(2)分區(qū)內(nèi)調(diào)度。分區(qū)內(nèi)調(diào)度是第2級(jí)調(diào)度,指分區(qū)內(nèi)進(jìn)程間的調(diào)度。分區(qū)內(nèi)調(diào)度是由操作系統(tǒng)根據(jù)分區(qū)的調(diào)度策略來對(duì)任務(wù)進(jìn)程集進(jìn)行時(shí)間分配。與分區(qū)間調(diào)度不同,它是可搶占式的調(diào)度策略,如最早截止期優(yōu)先(EDF)、空閑時(shí)間優(yōu)先(LLF)、速率單調(diào)調(diào)度(RMS)、截止時(shí)間單調(diào)調(diào)度(DMS)等。每個(gè)任務(wù)具體分配到的時(shí)間片是無法通過配置來指定的,因此,無法直接判定每個(gè)任務(wù)是否都能滿足它的可調(diào)度性。

在調(diào)度系統(tǒng)中,如果一個(gè)任務(wù)在每次到達(dá)之后都能在其截止時(shí)間限內(nèi)執(zhí)行完成,則判定該任務(wù)可調(diào)度,否則該任務(wù)不可調(diào)度。從而對(duì)任務(wù)可調(diào)度性的判定即對(duì)任務(wù)在截止時(shí)間期限內(nèi)是否執(zhí)行完成的判定。如果ARINC653分區(qū)系統(tǒng)中的所有任務(wù)都能在各自的截止時(shí)間限內(nèi)執(zhí)行完成,則判定分區(qū)系統(tǒng)可調(diào)度,否則,判定分區(qū)系統(tǒng)不可調(diào)度。本文即針對(duì)分區(qū)系統(tǒng)的可調(diào)度性判定方法進(jìn)行研究。

2.2 AADL

AADL用于設(shè)計(jì)和分析系統(tǒng)的軟硬件結(jié)構(gòu),包括獨(dú)立的組件和它們的交互,尤其適用于性能關(guān)鍵的實(shí)時(shí)嵌入式系統(tǒng)。AADL的組件包括軟件類、執(zhí)行平臺(tái)類和系統(tǒng)類。軟件類包含數(shù)據(jù)、子程序、線程、線程組、進(jìn)程5類組件;執(zhí)行平臺(tái)類包含處理器、存儲(chǔ)器、設(shè)備、總線4類組件;系統(tǒng)類的系統(tǒng)組件是作為軟件類組件和執(zhí)行平臺(tái)類組件的集成組件而設(shè)計(jì)的[3]。

本節(jié)將重點(diǎn)介紹AADL的線程、進(jìn)程和處理器組件,因?yàn)檫@些組件將運(yùn)用到ARINC653調(diào)度模型的建模。AADL的線程組件是一段執(zhí)行程序段,這些程序段可以使用Ada任務(wù)來表示。根據(jù)任務(wù)的激活模式,線程類型可以分為周期線程、非周期線程、零星線程。周期線程在固定的時(shí)間間隔下被激活,這個(gè)固定的時(shí)間間隔稱為周期,非周期線程在系統(tǒng)的任何時(shí)間被激活,沒有任何規(guī)律性,零星線程在一個(gè)最小的時(shí)間間隔下被激活。AADL的進(jìn)程組件提供了虛擬的時(shí)間和地址空間,每個(gè)進(jìn)程下的需求資源都是獨(dú)立和隔離的。AADL的處理器組件提供了線程運(yùn)行的需求資源。線程、進(jìn)程和處理器組件將用于對(duì)ARINC653系統(tǒng)分區(qū)調(diào)度中任務(wù)進(jìn)程、分區(qū)、模塊的建模。

AADL規(guī)范介紹了組件連接和組件屬性。組件連接對(duì)組件之間的關(guān)系進(jìn)行建模,如線程組件之間的時(shí)間同步、消息交互、共享數(shù)據(jù)訪問。組件屬性則存儲(chǔ)著組件自身的一些信息,這些屬性決定了組件在系統(tǒng)中的行為。組件屬性包含名字、值、類型3個(gè)部分,如線程組件有屬性Period,其值就是大于0的數(shù),類型是整型。這個(gè)屬性指明了周期線程的周期值。AADL包含標(biāo)準(zhǔn)的屬性,這些屬性不需要再進(jìn)行聲明。同時(shí),為了滿足特有的建模需求,允許第三方擴(kuò)展相應(yīng)的屬性。本文的研究就是基于Cheddar的擴(kuò)展屬性集(詳見文獻(xiàn)[6]),依賴于這些擴(kuò)展屬性集,使用AADL對(duì)ARINC653系統(tǒng)進(jìn)行建模,然后使用Cheddar工具對(duì)生成的模型進(jìn)行可調(diào)度性分析。

2.3 Cheddar

Cheddar是一個(gè)免費(fèi)的實(shí)時(shí)調(diào)度工具,專用于檢查實(shí)時(shí)系統(tǒng)中的任務(wù)時(shí)間約束[5]。借助于Ocarina[7],它可以用來分析AADL模型的可調(diào)度性。Cheddar提供了一套類Ada語言(Cheddar語言[6]),使用這個(gè)語言可以設(shè)計(jì)用戶自定義的調(diào)度策略。正是基于Cheddar的調(diào)度策略的可擴(kuò)展性,可以使用AADL對(duì)ARINC653分區(qū)調(diào)度系統(tǒng)進(jìn)行建模,同時(shí)使用Cheddar工具進(jìn)行分區(qū)調(diào)度的可調(diào)度性分析。

Cheddar提供2種調(diào)度分析功能:可行性測試和仿真?？尚行詼y試允許用戶不進(jìn)行調(diào)度模擬,根據(jù)已有的調(diào)度理論,研究實(shí)時(shí)應(yīng)用程序、系統(tǒng)是否可調(diào)度。相反,仿真首先進(jìn)行調(diào)度模擬,其次根據(jù)任務(wù)的約束屬性判斷任務(wù)的可調(diào)度性。可行性測試是簡單不復(fù)雜的,文獻(xiàn)[8]介紹了在幾種經(jīng)典調(diào)度策略下進(jìn)行可行性測試的方法。不過,由于多層級(jí)調(diào)度策略的復(fù)雜性,當(dāng)前還沒有相應(yīng)的可行性測試的方法。ARINC653系統(tǒng)是分區(qū)系統(tǒng),采用的是多層級(jí)的調(diào)度策略,本文根據(jù)自主設(shè)計(jì)的調(diào)度策略,通過仿真的方法對(duì)多層級(jí)調(diào)度系統(tǒng)進(jìn)行可調(diào)度性分析和判定。

3 相關(guān)工作

目前,安全關(guān)鍵系統(tǒng)已經(jīng)廣泛應(yīng)用于許多安全領(lǐng)域,如航空航天、汽車、醫(yī)藥等領(lǐng)域,同時(shí),這也導(dǎo)致系統(tǒng)越來越復(fù)雜。ARINC653就是一種航空電子設(shè)備標(biāo)準(zhǔn),它提供了一種時(shí)間和空間隔離的分區(qū)方式,來提高系統(tǒng)的安全性。

為避免系統(tǒng)中的錯(cuò)誤帶來嚴(yán)重的后果,文獻(xiàn)[9-10]介紹了幾種方法用來檢測安全關(guān)鍵系統(tǒng)的潛質(zhì)錯(cuò)誤。不過這些方法依賴于不同的符號(hào)和語言,在整個(gè)開發(fā)階段無法統(tǒng)一,所以基于模型驅(qū)動(dòng)的安全系統(tǒng)的分析方法被提出來[11]。使用模型驅(qū)動(dòng)的方法分析安全系統(tǒng)已經(jīng)被應(yīng)用在多個(gè)項(xiàng)目中(Flex-eWare[12], SAVI[13])。

關(guān)于安全關(guān)鍵系統(tǒng)的AADL模型的可調(diào)度性分析方面,本文所使用的Cheddar就是一款實(shí)現(xiàn)調(diào)度分析工具,它可以根據(jù)EDF或EMS等經(jīng)典調(diào)度策略公式,基于處理器利用率進(jìn)行可調(diào)性判定[14]。文獻(xiàn)[15]提出了使用進(jìn)程代數(shù)ACSR來對(duì)AADL模型元素的子集來進(jìn)行調(diào)度分析。由于ACSR方法的限制過多,其實(shí)用性并不高。TIMES[16]是基于任務(wù)自動(dòng)機(jī)的調(diào)度分析工具,由于它的非周期線程的定義與AADL中非周期線程的語義并不一致,因此不能用于分析包含非周期線程的 AADL模型。文獻(xiàn)[17]討論了AADL模型到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換,并提出了使用UPPAAL工具進(jìn)行可調(diào)度驗(yàn)證的方法。

針對(duì)分區(qū)系統(tǒng)的可調(diào)度判定的研究,文獻(xiàn)[18]在任務(wù)時(shí)間需求函數(shù)的基礎(chǔ)上,計(jì)算系統(tǒng)消耗時(shí)間,得出了系統(tǒng)可調(diào)度性的判定定理。文獻(xiàn)[19]分析了分區(qū)參數(shù)對(duì)任務(wù)調(diào)度實(shí)時(shí)性的影響,針對(duì)周期和零星任務(wù),通過計(jì)算任務(wù)的響應(yīng)時(shí)間上界,推導(dǎo)出分區(qū)調(diào)度下的任務(wù)可調(diào)度條件。文獻(xiàn)[20]設(shè)計(jì)并實(shí)現(xiàn)了時(shí)間分析工具IMATime,對(duì)分區(qū)系統(tǒng)FCOS進(jìn)行三級(jí)分析,同時(shí)提供分區(qū)周期和分區(qū)容限。

4 基于AADL的ARINC653分區(qū)系統(tǒng)建模方法

使用Cheddar對(duì)ARINC653分區(qū)系統(tǒng)進(jìn)行可調(diào)度分析前,必須先使用AADL對(duì)系統(tǒng)進(jìn)行建模,本節(jié)將介紹借助于Cheddar擴(kuò)展屬性,如何使用AADL對(duì) ARINC653分區(qū)系統(tǒng)進(jìn)行建模。為使AADL能對(duì)ARINC653系統(tǒng)進(jìn)行建模,必須找出AADL模型元素與ARINC653系統(tǒng)概念的對(duì)應(yīng)關(guān)系。本節(jié)將介紹調(diào)度方面的對(duì)應(yīng)規(guī)則以及Cheddar擴(kuò)展屬性的應(yīng)用,同時(shí)給出如何在Cheddar中自定義調(diào)度策略,并根據(jù)上述的對(duì)應(yīng)規(guī)則給出一個(gè)分區(qū)系統(tǒng)建模實(shí)例。

4.1 AADL與ARINC653的對(duì)應(yīng)規(guī)則

4.1.1 模塊對(duì)應(yīng)規(guī)則

考慮到ARINC653系統(tǒng)模塊包含一個(gè)或多個(gè)航空電子應(yīng)用軟件,并保證這些應(yīng)用軟件之間相互獨(dú)立運(yùn)行。系統(tǒng)將運(yùn)行在模塊上的多個(gè)應(yīng)用軟件按功能劃分為多個(gè)分區(qū),同時(shí)指明每個(gè)分區(qū)分配的系統(tǒng)資源和分區(qū)內(nèi)的調(diào)度信息。而AADL中的processor組件可以用來指明系統(tǒng)運(yùn)行時(shí)的執(zhí)行環(huán)境,包括CPU的調(diào)度分配、內(nèi)存分配、通信連接總線等。因此,可以使用AADL的processor組件表示ARINC653模塊概念,這個(gè)組件提供了模塊運(yùn)行時(shí)的資源需求以及空間和時(shí)間隔離。同時(shí),分區(qū)間的調(diào)度策略可以通過屬性Dispatch_Protocol定義。由于分區(qū)系統(tǒng)調(diào)度的復(fù)雜性,當(dāng)前并不存在一個(gè)已有的調(diào)度策略,因此需要借助于Cheddar屬性自定義調(diào)度策略。首先processor組件屬性Cheddar_Properties::Scheduling_Protocol需要賦值為AUTOMATA_USER_DEFINED_PROTOCOL,其次屬性Cheddar_Properties::Source_Text賦值為包含調(diào)度策略的文件名,最后屬性 Cheddar_Properties:: Automaton_Name賦值為調(diào)度策略所使用的時(shí)間自動(dòng)機(jī)的名字。具體的自定義調(diào)度策略的方法流程見本文4.2節(jié)和4.3節(jié)。

4.1.2 分區(qū)對(duì)應(yīng)規(guī)則

ARINC653分區(qū)包含了一組任務(wù)集合,它在時(shí)間和空間上是隔離的,不同分區(qū)的任務(wù)的運(yùn)行是不受影響的。分區(qū)可以擁有不同的關(guān)鍵級(jí)別來保證分區(qū)間的數(shù)據(jù)流通的安全性。在模塊的總時(shí)間框架內(nèi),分區(qū)被調(diào)度的周期和被分配的時(shí)間片是固定的,同時(shí),基于空間隔離的需求,分區(qū)被分配在不同的地址空間里?？紤]到AADL中的virtual processor組件可以用來構(gòu)建一個(gè)邏輯資源,概念上是processor組件的一個(gè)子組件,可以將processor組件指明的運(yùn)行環(huán)境分成多個(gè)互不影響的區(qū)域。每個(gè)邏輯資源可以單獨(dú)指明相應(yīng)的調(diào)度信息以及內(nèi)存分配情況等。此外,AADL另一組件類型process組件,它指明了具體的執(zhí)行條件,程序段和交互數(shù)據(jù),它包含一個(gè)thread組件來表示執(zhí)行的動(dòng)作。因此,可以用AADL中的以上2種組件來表示ARINC653模塊中分區(qū)概念,其中virtual processor組件指明分區(qū)運(yùn)行時(shí)資源的分配(任務(wù)調(diào)度,分區(qū)資源等),而process組件指明了分區(qū)包含的內(nèi)容(線程、數(shù)據(jù)等)。這2種組件之間的關(guān)聯(lián)通過 AADL屬性 Actual_Processor_ Binding定義。processor組件包含一組 virtual processor組件,如同模塊包含一組分區(qū)。

分區(qū)內(nèi)調(diào)度策略的定義方法與上述介紹的模塊下分區(qū)間調(diào)度策略類似,本文不再詳述。

4.1.3 進(jìn)程對(duì)應(yīng)規(guī)則

ARINC653進(jìn)程是系統(tǒng)執(zhí)行主體,它包含了執(zhí)行代碼、執(zhí)行數(shù)據(jù)和堆棧區(qū)域等。一個(gè)分區(qū)可以包含多個(gè)進(jìn)程,來實(shí)現(xiàn)相應(yīng)的應(yīng)用功能。分區(qū)通過指明進(jìn)程的調(diào)度策略、搶占策略、最大響應(yīng)時(shí)間、內(nèi)存分配情況等信息來控制進(jìn)程的執(zhí)行。而AADL中的thread組件是系統(tǒng)最基本的調(diào)度執(zhí)行單元,通過時(shí)間周期或者外部事件來執(zhí)行線程。線程間的通信可以通過端口連接、子程序調(diào)用和共享數(shù)據(jù)來實(shí)現(xiàn)。因此,可以使用AADL的thread組件表示ARINC653進(jìn)程概念,因?yàn)樗鼈冇邢嗤母拍?執(zhí)行主體。執(zhí)行主體所需要的特征可以用AADL屬性來定義,包括執(zhí)行周期、執(zhí)行截止時(shí)間、執(zhí)行時(shí)間和調(diào)度策略等。AADL中的thread組件包含在process組件中就像ARINC653中的進(jìn)程包含在分區(qū)中一樣。thread組件屬性Dispatch_Protocol定義線程類型即激活模式(如周期、非周期、零星等),Compute_Execution_ Time定義線程的執(zhí)行時(shí)間,Period定義周期線程的周期值,Deadline定義線程最壞響應(yīng)時(shí)間。

圖3總結(jié)了上述的對(duì)應(yīng)規(guī)則,即給出了使用AADL中的哪些組件和屬性對(duì)ARINC653系統(tǒng)分區(qū)調(diào)度信息進(jìn)行建模。比如使用AADL中的處理器組件給ARINC653中的模塊建模,其中使用組件屬性Thread_Properties::Scheduling_Protocol表示模塊下分區(qū)所采用的調(diào)度策略。依賴于表格中的AADL標(biāo)準(zhǔn)屬性和以Cheddar_Properties::開頭的Cheddar擴(kuò)展屬性生成的AADL模型,Cheddar工具就可以進(jìn)一步進(jìn)行可調(diào)度性分析和判定。

圖3 AADL與ARINC653對(duì)應(yīng)規(guī)則

4.2 Cheddar自定義調(diào)度策略

使用Cheddar語言定義一個(gè)新的調(diào)度策略,它由兩部分組成:類Ada語言程序段和時(shí)間自動(dòng)機(jī)。類Ada語言程序段用來進(jìn)行仿真計(jì)算,同時(shí)它也提供了必要的仿真數(shù)據(jù)(如任務(wù)周期、任務(wù)喚醒時(shí)間、任務(wù)優(yōu)先級(jí)、任務(wù)截止時(shí)間等)。程序段被分為多個(gè)部分,分別在仿真的不同階段進(jìn)行模擬計(jì)算,這些部分包括:start_section,包含變量的聲明和初始化; priority_section,在每個(gè)單元時(shí)間片分配前,計(jì)算每個(gè)任務(wù)的優(yōu)先級(jí);election_section,指定下一個(gè)單元時(shí)間片分配給的任務(wù)。

使用Cheddar語言定義的調(diào)度策略Ada程序段如下:

上述3個(gè)程序段都有相應(yīng)的命名。首先在start_ section片段內(nèi)定義了一個(gè)數(shù)組dynamic_priority,系統(tǒng)初始化時(shí),創(chuàng)建大小是任務(wù)個(gè)數(shù)的數(shù)組。再在priority_section片段內(nèi)將上述數(shù)組賦值為任務(wù)集的周期值數(shù)組,那么在時(shí)間片分配前,dynamic_priority數(shù)組保存著當(dāng)前任務(wù)集的周期值,最后在election_ section片段內(nèi)返回dynamic_priority數(shù)組中值最小的索引,即返回周期值最短的任務(wù)索引(min_to_ index是Cheddar工具自帶的內(nèi)嵌函數(shù),用來返回?cái)?shù)組中值最小的索引)。根據(jù)上述定義的調(diào)度策略,它與RMS調(diào)度策略比較相似,周期值越小的任務(wù)優(yōu)先分配到時(shí)間片。

時(shí)間自動(dòng)機(jī)用來表示線程狀態(tài)的時(shí)間轉(zhuǎn)換情況,可以用實(shí)時(shí)系統(tǒng)驗(yàn)證工具UPPAAL生成。使用時(shí)間自動(dòng)機(jī)的節(jié)點(diǎn),時(shí)間約束和變量值表示系統(tǒng)的狀態(tài)。每個(gè)時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換可以是獨(dú)立的,也可以與其他的時(shí)間自動(dòng)機(jī)同步進(jìn)行狀態(tài)轉(zhuǎn)換。使用時(shí)間自動(dòng)機(jī)來表示任務(wù)的運(yùn)行和切換,使用時(shí)間約束來控制狀態(tài)轉(zhuǎn)換過程。Cheddar使用時(shí)間自動(dòng)機(jī)對(duì)線程調(diào)度進(jìn)行建模,并運(yùn)行上述的類Ada語言程序段,讀寫仿真數(shù)據(jù)。

在Cheddar中定義的一個(gè)時(shí)間自動(dòng)機(jī)的代碼示例如下:

首先定義一個(gè)狀態(tài)Ready,即自動(dòng)機(jī)的初始化狀態(tài),再定義一個(gè)狀態(tài)遷移關(guān)系,從狀態(tài)Ready遷移到狀態(tài)Ready,即系統(tǒng)都處在狀態(tài)Ready。狀態(tài)轉(zhuǎn)換包含3個(gè)部分:變量更新,判定條件,同步信號(hào),該示例中變量更新和判定條件是沒有的,不過存在一個(gè)同步信號(hào)。當(dāng)處在Ready狀態(tài)的線程接收到election_ name同步信號(hào)(上文Ada程序段中election_section調(diào)度完畢后系統(tǒng)會(huì)發(fā)出election_name信號(hào))時(shí),會(huì)發(fā)生狀態(tài)遷移,狀態(tài)再次遷移到Ready。

針對(duì)分區(qū)調(diào)度系統(tǒng),通過定義2種不同的調(diào)度策略,一種用于分區(qū)間調(diào)度,另一種用于分區(qū)內(nèi)任務(wù)調(diào)度。2種調(diào)度策略之間通過同步信號(hào)來同步和交互,完成多層級(jí)調(diào)度,具體見下節(jié)的建模實(shí)例分析。

4.3 建模實(shí)例分析

本節(jié)將給出一個(gè)建模的例子,介紹如何借助于Cheddar擴(kuò)展屬性,使用AADL對(duì)ARINC653系統(tǒng)的分區(qū)調(diào)度模型進(jìn)行建模,建模流程如圖4所示。首先根據(jù)系統(tǒng)的調(diào)度信息,使用Cheddar設(shè)計(jì)相應(yīng)的調(diào)度策略,其次依賴于 4.1節(jié)介紹的 AADL與ARINC653的對(duì)應(yīng)規(guī)則和調(diào)度策略,分別使用AADL的thread組件、process組件和processor組件對(duì)系統(tǒng)中的進(jìn)程、分區(qū)、模塊建模,同時(shí),將設(shè)計(jì)好的調(diào)度策略賦予組件屬性。

圖4 ARINC653分區(qū)系統(tǒng)建模過程

表1是ARINC653系統(tǒng)分區(qū)間和分區(qū)內(nèi)的調(diào)度信息,詳細(xì)描述了一個(gè)總時(shí)間框架下(時(shí)間片大小是10 ms)分區(qū)集和各分區(qū)任務(wù)集的調(diào)度情況。系統(tǒng)包含有2個(gè)分區(qū)(partion1和partion2),每個(gè)分區(qū)包含有2個(gè)任務(wù),調(diào)度策略分別是DMS和RMS。

表1 ARINC653系統(tǒng)調(diào)度信息 ms

使用AADL對(duì)上述ARINC653分區(qū)系統(tǒng)調(diào)度信息進(jìn)行建模,得到模型如下:

AADL的 processor組件(arinc.Impl)表示ARINC653系統(tǒng)分區(qū)運(yùn)行所在的模塊(arinc),2個(gè)AADL的 process組件(partition1.Impl和 partition2. Impl)表示ARINC653系統(tǒng)中的2個(gè)分區(qū)(partiton1和partition2),4個(gè)AADL的thread組件表示ARINC653系統(tǒng)中的4個(gè)任務(wù)進(jìn)程。每個(gè)分區(qū)分別包含2個(gè)任務(wù)進(jìn)程(partition1包含T1和T2,partition2包含T3和T4),Actual_Processor_Binding屬性將進(jìn)程組件與處理器組件綁定,指明進(jìn)程所在的處理器組件。進(jìn)程partition1和partition2所在的執(zhí)行組件都是arinc.Impl,即ARINC653系統(tǒng)中2個(gè)分區(qū)同在arinc模塊中。

AADL屬性Compute_Execution_Time,Dispatch_ Protocol、Period、Deadline等指明了ARINC653系統(tǒng)任務(wù)的調(diào)度信息,其中,Compute_Execution_Time, Dispatch_Protocol、Period、Deadline等是AADL的標(biāo)準(zhǔn)屬性,指明了任務(wù)的執(zhí)行時(shí)間、任務(wù)的類型、周期任務(wù)的周期時(shí)間、任務(wù)的截止時(shí)間等。

AADL擴(kuò)展屬性Cheddar_Properties::Scheduling_ Protocol指明調(diào)度策略,例子中處理器和2個(gè)進(jìn)程組件都有獨(dú)立的調(diào)度策略,分別定義了模塊下分區(qū)間的調(diào)度策略和分區(qū)partion1和partion2內(nèi)的調(diào)度策略。模型中arinc.Impl處 理器 組 件 的 Cheddar_Properties:: Scheduling_Protocol屬性值是AUTOMATA_USER_ DEFINED_PROTOCOL指明了分區(qū)間的調(diào)度策略是Cheddar自定義的時(shí)間自動(dòng)機(jī),使用時(shí)間自動(dòng)機(jī)表示線程的狀態(tài)轉(zhuǎn)移情況。Cheddar_Properties::Source_Text屬性值指明了時(shí)間自動(dòng)機(jī)所在的文件名,arinc_ processor.sc包含了分區(qū)間調(diào)度的Cheddar程序段和時(shí)間自動(dòng)機(jī)。partition1和partition2進(jìn)程組件屬性值與處理器組件相同,不過調(diào)度策略所在的文件不同。arinc_ partition1.sc和arinc partition2.sc文件分別包含了這2個(gè)分區(qū)的調(diào)度策略。

arinc_partition1.sc文件包含了圖5(a)所描述的時(shí)間自動(dòng)機(jī)。partition1_capacity變量指明分區(qū)partition1在一個(gè)總時(shí)間框架內(nèi)被分配到的時(shí)間片大小,partition1_duration變量指明分區(qū)已經(jīng)執(zhí)行的時(shí)間片大小。在程序段election_section內(nèi),根據(jù)DMS調(diào)度策略的定義,指定下個(gè)時(shí)間片將分配給截止時(shí)間最小的任務(wù)。這里調(diào)用了Cheddar內(nèi)嵌函數(shù)min_to_ index來獲取當(dāng)前處于等待狀態(tài)并擁有最小截止時(shí)間的任務(wù),文獻(xiàn)[6]詳細(xì)介紹了Cheddar的內(nèi)嵌函數(shù)。arinc_partition2.sc文件包含了圖5(b)所描述的時(shí)間自動(dòng)機(jī),變量定義也是一樣的。由于調(diào)度策略的不同,這個(gè)分區(qū)使用的是RMS調(diào)度策略。在程序段priority_section內(nèi),根據(jù)RMS調(diào)度策略的定義,指定下個(gè)時(shí)間片將分配給周期最小的任務(wù)。arinc_ processor.sc文件包含了圖5(c)所描述的分區(qū)間調(diào)度時(shí)間自動(dòng)機(jī),指明在10 ms總時(shí)間框架下先分配6 ms給分區(qū)partition1,再分配4 ms給分區(qū)partition2,如此周期性的時(shí)間片分配。

圖5 調(diào)度時(shí)間自動(dòng)機(jī)

文本內(nèi)容基本相似,本文不再贅述。

5 基于Cheddar的可調(diào)度性判定

本文針對(duì)含有純周期任務(wù)的分區(qū)系統(tǒng)的可調(diào)度性判定問題,提出一種基于仿真方法實(shí)現(xiàn)的可調(diào)度性判定方法,具體流程如圖6所示。該方法通過設(shè)定時(shí)鐘變量來模擬任務(wù)調(diào)度過程中的系統(tǒng)時(shí)鐘,在時(shí)鐘變量值增長過程中,根據(jù)任務(wù)優(yōu)先級(jí)從高到低的順序分析各個(gè)任務(wù)約束屬性的滿足情況,判定任務(wù)的可調(diào)度性,從而判定分區(qū)系統(tǒng)的可調(diào)度性。

圖6 可調(diào)度性判定流程

由于分區(qū)系統(tǒng)下調(diào)度模型的多樣性,以及本文提出的可調(diào)度性分析方法的局限性,需要對(duì)調(diào)度模型進(jìn)行限制。下文將介紹可進(jìn)行可調(diào)度判定的分區(qū)調(diào)度模型和進(jìn)行可調(diào)度性判定方法的理論依據(jù),并給出基于上述描述的分區(qū)系統(tǒng)進(jìn)行可調(diào)度性判定的實(shí)例。

5.1 ARINC653分區(qū)系統(tǒng)的調(diào)度模型

ARINC653分區(qū)系統(tǒng)相應(yīng)調(diào)度模型描述如下: (1)系統(tǒng)中有若干個(gè)分區(qū),分區(qū)間可以進(jìn)行通信,但分區(qū)之間在時(shí)間和空間上彼此獨(dú)立。

(2)系統(tǒng)為各分區(qū)分派時(shí)間片,各分區(qū)的時(shí)間片都有時(shí)間片開始時(shí)間(offset)和時(shí)間片大小(duration)2個(gè)參數(shù),系統(tǒng)周期性地為分區(qū)分派時(shí)間片。

(3)系統(tǒng)可為各分區(qū)設(shè)定相互獨(dú)立的分區(qū)內(nèi)任務(wù)集調(diào)度策略。

(4)各分區(qū)內(nèi)的任務(wù)集在各自分區(qū)分派的時(shí)間片內(nèi)按照相應(yīng)的調(diào)度策略調(diào)度執(zhí)行,不受其他分區(qū)任務(wù)的干擾,任務(wù)集在執(zhí)行過程中遇到時(shí)間片用完時(shí),暫停執(zhí)行過程,等待下一個(gè)時(shí)間片的到達(dá)。

(5)分區(qū)下的所有任務(wù)都是周期任務(wù),且任務(wù)的周期等于任務(wù)的截止時(shí)間,具有硬實(shí)時(shí)系統(tǒng)的強(qiáng)時(shí)間限定,即必須在各任務(wù)的截止時(shí)間內(nèi)完成,否則分區(qū)任務(wù)集不可調(diào)度。

(6)調(diào)度中忽略任務(wù)間切換的時(shí)間。

(7)分區(qū)下的任務(wù)是可搶占的,且在同一處理器下運(yùn)行。

(8)只針對(duì)時(shí)間約束分析,默認(rèn)任務(wù)所需的其他非時(shí)間資源都滿足要求。任務(wù)的可調(diào)度性判定等價(jià)于判定任務(wù)的時(shí)間約束是否滿足。

5.2 理論依據(jù)

針對(duì)非分區(qū)系統(tǒng)的調(diào)度模型,任務(wù)集下的所有任務(wù)都是周期任務(wù),且各個(gè)任務(wù)的分派到達(dá)僅依賴于其相應(yīng)的周期。因此,任務(wù)第一次到達(dá)以后的所有到達(dá)時(shí)刻都是確定的,用設(shè)定系統(tǒng)時(shí)鐘變量來模擬調(diào)度過程的方法是可行的。

假設(shè)任務(wù)集s含有n個(gè)周期任務(wù),設(shè)定n個(gè)任務(wù)都在0時(shí)刻到達(dá),這n個(gè)任務(wù)下一次同時(shí)到達(dá)的時(shí)刻為此n個(gè)任務(wù)周期值的最小公倍數(shù)的時(shí)刻。n個(gè)周期任務(wù)的到達(dá)在整體上也呈周期性,且周期值為所有任務(wù)周期值的最小公倍數(shù),文獻(xiàn)[21]給出了相關(guān)證明。

針對(duì)分區(qū)系統(tǒng)和上述限定的調(diào)度模型,分區(qū)周期性獲得系統(tǒng)分派的時(shí)間片。各分區(qū)下任務(wù)集中所有任務(wù)都是周期任務(wù),因此,所有任務(wù)的觸發(fā)到達(dá)呈周期性。在分區(qū)調(diào)度模型中,所有任務(wù)的到達(dá)執(zhí)行與所在分區(qū)的時(shí)間片分派情況整體上呈周期性,周期值為所有任務(wù)周期值與分區(qū)獲得時(shí)間片的周期值的最小公倍數(shù)。

依據(jù)上述周期最小公倍數(shù)理論可知,任務(wù)的執(zhí)行過程呈周期性往復(fù)執(zhí)行,因此本文在用仿真方法模擬任務(wù)調(diào)度過程判定任務(wù)集的可調(diào)度性的實(shí)現(xiàn)過程中,將系統(tǒng)時(shí)鐘設(shè)定為一個(gè)周期值的時(shí)鐘區(qū)域,分析任務(wù)集在此周期內(nèi)的調(diào)度情況,從而等價(jià)描述系統(tǒng)時(shí)鐘中剩余時(shí)間區(qū)域的可調(diào)度情況。因?yàn)槿蝿?wù)執(zhí)行過程中的確定性和周期性,所以系統(tǒng)時(shí)鐘的選取是確定的有窮的時(shí)鐘區(qū)域,因此,用仿真方法判定分區(qū)調(diào)度模型的可調(diào)度性是可行的。

5.3 仿真實(shí)例分析

表1描述了分區(qū)系統(tǒng)的任務(wù)調(diào)度信息,系統(tǒng)包含4個(gè)周期任務(wù)且周期等于截止時(shí)間。調(diào)度信息滿足上述的可進(jìn)行可調(diào)度性判定的調(diào)度模型。這4個(gè)周期任務(wù)的周期分別是10 ms,5 ms,20 ms,10 ms,最小公倍數(shù)是20 ms,分區(qū)獲得時(shí)間片的周期是10 ms,所以所有任務(wù)周期與分區(qū)獲得時(shí)間片的周期的最小公倍數(shù)是20 ms,即仿真時(shí)長是20 ms。

根據(jù)第4節(jié)介紹的內(nèi)容,將包含表1分區(qū)調(diào)度信息的AADL模型作為Cheddar工具的輸入,同時(shí),編輯好自定義的調(diào)度策略,設(shè)置好仿真時(shí)長,調(diào)度結(jié)果如圖7所示。

圖7 調(diào)度仿真結(jié)果

可調(diào)度性判定結(jié)果分為上下2個(gè)部分,上面是任務(wù)在仿真時(shí)長內(nèi)的調(diào)度甘特圖,下面是判定結(jié)果。調(diào)度圖中的一小格代表一個(gè)時(shí)間片,在本例中是1 ms。分區(qū)獲得時(shí)間的周期是10 ms,分區(qū)partition1包含任務(wù)T1和T2,它被首先分配到6 ms的系統(tǒng)時(shí)鐘,此時(shí)分區(qū)partition2中任務(wù)是空閑不運(yùn)行的。由于分區(qū)partition1的調(diào)度策略是DMS,任務(wù)的截止時(shí)間與優(yōu)先級(jí)成反比,而任務(wù)T1的截止時(shí)間大于T2的,所以T2的優(yōu)先級(jí)大于T1。T2優(yōu)先獲得系統(tǒng)時(shí)鐘,當(dāng)T2完成它的任務(wù)后(執(zhí)行時(shí)間1 ms),T1再獲得系統(tǒng)時(shí)鐘。當(dāng)T1完成它的任務(wù)(執(zhí)行時(shí)間3 ms),分區(qū)partiton1共執(zhí)行了4 ms的時(shí)間,在之后的一個(gè)時(shí)間片上,由于partiton1里沒有任務(wù)可運(yùn)行,partiton2還沒有被分配到系統(tǒng)時(shí)鐘,系統(tǒng)處于空閑狀態(tài)。在第6 ms時(shí)刻,周期為5 ms的任務(wù)T1再次被分配到1 ms的時(shí)間片。當(dāng)T1執(zhí)行完這個(gè)時(shí)間片后,分區(qū)partiton1的執(zhí)行時(shí)間達(dá)到了6 ms,系統(tǒng)將把下一個(gè)時(shí)間片分配給分區(qū)partiton2。分區(qū)partition2包含任務(wù)T3和T4,由于分區(qū)partition2的調(diào)度策略是RMS,任務(wù)的優(yōu)先級(jí)跟任務(wù)的周期成反比。T3的周期大于T4的周期,因此T4的優(yōu)先級(jí)大于T3的優(yōu)先級(jí)。T4將會(huì)先被分配到系統(tǒng)時(shí)鐘,執(zhí)行完任務(wù)后(執(zhí)行時(shí)間2 ms),T3再獲得系統(tǒng)時(shí)鐘,也執(zhí)行完任務(wù)(執(zhí)行時(shí)間2 ms)。分區(qū)partition2共執(zhí)行了4 ms時(shí)間,此時(shí)系統(tǒng)執(zhí)行時(shí)間達(dá)到10 ms,下個(gè)時(shí)間片,系統(tǒng)再次將系統(tǒng)時(shí)鐘分配給分區(qū)partiton1。不過在這個(gè)周期內(nèi),由于T3的周期是20 ms,它將不會(huì)被激活和分配系統(tǒng)時(shí)間片。綜上所述,系統(tǒng)將以20 ms為周期,周期性地進(jìn)行時(shí)間片的分配。

調(diào)度結(jié)果圖中下半部分給出了可調(diào)度性判定,判定結(jié)果是可調(diào)度的,同時(shí)列出了每個(gè)任務(wù)的最壞響應(yīng)時(shí)間,滿足任務(wù)的截止時(shí)間要求。

6 結(jié)束語

為滿足航空電子系統(tǒng)高可靠性、高安全性的需求,ARINC組織發(fā)布了航空電子應(yīng)用軟件標(biāo)準(zhǔn)接口ARINC653。目前ARINC653標(biāo)準(zhǔn)中提出的分區(qū)操作系統(tǒng)架構(gòu)已經(jīng)成為航空電子系統(tǒng)的新標(biāo)準(zhǔn)。航空電子系統(tǒng)對(duì)實(shí)時(shí)性要求極高,因此,對(duì)系統(tǒng)進(jìn)行時(shí)間調(diào)度驗(yàn)證是有必要的。針對(duì)ARINC653系統(tǒng)的分區(qū)概念的特性,本文提出了一種對(duì)分區(qū)任務(wù)集進(jìn)行可調(diào)度性判定的方法。本文使用建模語言AADL對(duì)ARINC653系統(tǒng)進(jìn)行建模,通過Cheddar擴(kuò)展屬性和自定義調(diào)度策略,使得Cheddar具有對(duì)分區(qū)系統(tǒng)進(jìn)行可調(diào)度性判定的能力。Cheddar提供了一種類Ada語言(Cheddar語言),通過一組程序段和時(shí)間自動(dòng)機(jī)來設(shè)計(jì)分區(qū)調(diào)度策略,再通過仿真的方式模擬系統(tǒng)時(shí)鐘的執(zhí)行,根據(jù)仿真結(jié)果判定系統(tǒng)的可調(diào)度性。在使用本文方法對(duì)分區(qū)系統(tǒng)進(jìn)行可調(diào)度性判定時(shí),對(duì)分區(qū)下的任務(wù)有許多限制。任務(wù)必須是周期線程,且周期值等于截止時(shí)間等一些限定條件,限制了本文方法的使用場景。對(duì)于帶有非周期性任務(wù)的分區(qū),即不滿足限定條件的任務(wù),如何進(jìn)行可調(diào)度性判定是下一步的研究方向。

[1] 易建平,韓 慶.飛機(jī)綜合模塊化航電系統(tǒng)總體設(shè)計(jì)研究[J].科學(xué)技術(shù)與工程,2010,10(19):2709-2714.

[2] AeronauticalRadio,Inc..ARINC Specification 653 Avionics Application Software Standard Interface[Z]. 1997.

[3] AADL Portal at Telecom ParisTech(AADL)[EB/OL]. (2009-07-14).http://aadl.telecom-paristech.fr/.

[4] Delange J,Gilles O.Model-Based Engineering for the Development of ARINC653 Architectures[J].SAE International Journal of Aerospace,2009,3(1):79-86.

[5] Singhoff F,Legrand J,Nana L.Cheddar:A Flexible Real Time Scheduling Framework[C]//Proc.of International ACM SIGAda Conference.Atlanta,USA:[s.n.],2004: 1-10

[6] Singhoff F.Cheddar Release 2.x User’s Guide[R]. Technical Report:singhoff-01-07,2007.

[7] TELECOM ParisTech,Inc..Ocarina User Guide[Z]. 2005.

[8] Stankovic J A,Spuri M,Natale D M,et al.Implications of Classical Scheduling Results For Real Time Systems [J].IEEE Computer,1995,28(6):16-25.

[9] Atchison B,Lindsay P.Safety Validation of Embedded Control Software Using Z Animation[C]//Proc.of the 5th IEEE International Symposium on High Assurance Systems Engineering.Albuquerque,USA:IEEE Press, 2000:228-237.

[10] Conmy P,Nicholson M,McDermid J.Safety Assurance Contracts for Integrated Modular Avionics[C]//Proc.of the 8th Australian Workshop on Safety Critical Systems and Software.Canberra,Australian:[s.n.],2003:6978.

[11] Kashi R N,Amarnathan M.Perspectives on the Use of Model Based Development Approach for Safety Critical Avionics Software Development[C]//Proc. of International Conference on AerospaceScience and Technology.Bangaloire,India:[s.n.],2008.

[12] Delange J,Hugues J,Pautet L,et al.Code Generation strategies from AADL Architectural Descriptions Targeting the High Integrity Domain[C]//Proc of the 4th EuropeanCongressERTSEmbeddedReal-time Software.Toulouse,France:[s.n.],2008.

[13] Chilenski J. Aerospace Vehicle Systems Institute Systems and Software Integration Verification Overview [C]//Proc.of AADL Safety and Security Modeling Meeting.[S.l.]:IEEE Press,2007.

[14] Singhoff F,Legrand J,Nana L.Scheduling and Memory Requirements Analysis with AADL[J].Ada Letters, 2005,25(4):1-10.

[15] Bremond G P,Choi J Y,Clarke D,et al.A Process Algebra to the Schedulability Analysis of Real-time Systems[M].Norwell,USA:KluwerAcademic Publishers,1998.

[16] Amnell T,Fersman E,Mokrushin L,et al.TIMES——A Tool for Modeling and Implementation of Embedded Systems[C]//Proc.of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.London,UK:Springer-Verlag, 2002:460-464.

[17] 李振松,顧 斌.基于UPPAAL的AADL行為模型驗(yàn)證方法研究[J].計(jì)算機(jī)科學(xué),2012,39(2):159-161.

[18] 何 峰,宋麗茹,熊華鋼.航空電子雙層任務(wù)分區(qū)調(diào)度設(shè)計(jì)[J].北京航空航天大學(xué)學(xué)報(bào),2008,34(11): 1364-1368.

[19] 周天然,熊華鋼.航空電子系統(tǒng)混合實(shí)時(shí)任務(wù)的雙層調(diào)度[J].航空學(xué)報(bào),2011,32(6):1067-1074.

[20] 湯小明,張新國.基于分區(qū)的安全關(guān)鍵軟件體系及其時(shí)間分析研究[J].系統(tǒng)仿真學(xué)報(bào),2013,25(7): 1704-1709.

[21] Leung J,Merrill M L.A Note on Preemptive Scheduling of Periodic Real-time Tasks[J].Information Processing Letters,1980,11(3):115-118.

編輯 金胡考

Schedulability Determination of Integrated Modular Avionics Partitioned System Based on AADL

YUAN Xiang1,HU Jun1,2,MA Jin-jing1,LIU Xue1
(1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;
2.State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China)

Integrated Modular Avionics(IMA)partitioned system is put forward to improve the reliability and security of the system,but in the process of system design and implementation,analysis and validation should be used to ensure that the system time requirements are met.In allusion to IMA system which meets ARINC653 specification,according to the characteristics of hierarchy scheduling partitioned system,this paper proposes a schedulability determination method based on simulation method.With the aid of Cheddar tool and the function of custom scheduling strategy,Architecture Analysis and Design Language(AADL)has the ability of modeling partitioned system,then the tool operates on the generated AADL model to determine the system schedulable.Example analysis result shows that the tool has automatic, accurate and fast advantages to describe task scheduling process by Gantt chart and the result is accurate and detailed.

Integrated Modular Avionics(IMA);ARINC653 system;partitioned system;Architecture Analysis and Design Language(AADL);Cheddar tool;schedulability determination;simulation method

1000-3428(2014)10-0052-09

A

TP311

10.3969/j.issn.1000-3428.2014.10.011

國家自然科學(xué)基金資助項(xiàng)目(61272083);江蘇省普通高校研究生科研創(chuàng)新計(jì)劃基金資助項(xiàng)目(CXZZ11_0218)。

袁 翔(1987-),男,碩士研究生,主研方向:嵌入式軟件建模與分析;胡 軍,副教授、CCF會(huì)員;馬金晶、劉 雪,碩士研究生。

2013-08-27

2013-11-08E-mail:yuanxiangnuaa@163.com

中文引用格式:袁 翔,胡 軍,馬金晶,等.基于AADL的綜合航電分區(qū)系統(tǒng)可調(diào)度性判定[J].計(jì)算機(jī)工程, 2014,40(10):52-60.

英文引用格式:Yuan Xiang,Hu Jun,Ma Jinjing,et al.Schedulability Determination of Integrated Modular Avionics Partitioned System Based on AADL[J].Computer Engineering,2014,40(10):52-60.