基于AADL的綜合航電分區系統可調度性判定

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

(1.南京航空航天大學計算機科學與技術學院,南京210016;

2.南京大學計算機軟件新技術國家重點實驗室,南京210093)

基于AADL的綜合航電分區系統可調度性判定

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

(1.南京航空航天大學計算機科學與技術學院,南京210016;

2.南京大學計算機軟件新技術國家重點實驗室,南京210093)

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

綜合模塊化航電;ARINC653系統;分區系統;架構分析和設計語言;Cheddar工具;可調度性判定;仿真方法

1 概述

綜合模塊化航電(Integrated Modular Avionics, IMA)系統[1]是航空應用領域中的一類重要系統結構。ARINC653標準[2]定義了一種IMA軟件體系結構,制定了操作系統層和應用軟件層之間的標準接口(APEX)。標準滿足ARINC653的IMA系統稱為ARINC653系統。

ARINC653系統提出了分區操作系統的概念,用來提高航空電子系統的可靠性、高安全性。為保障系統的安全性和可靠性,在系統的設計和實現過程中,應采用各種分析、建模及驗證方法對系統進行嚴格的檢驗,以保證系統在各種情況下的非功能需求和時間需求都能得到滿足。為了精確管理時間資源,以達到強實時性要求,對系統進行可調度性分析相當必要。

架構分析和設計語言(Architecture Analysis and Design Language,AADL)[3]是一種針對嵌入式系統建模描述語言,可應用于航空嵌入式系統(ARINC653系統)的架構設計建模及分析[4]。Cheddar是一款實時調度分析工具[5],可應用于實時系統的時間性驗證,同時支持對AADL模型表示的實時系統進行可調度性分析。

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

2 背景知識

2.1 ARINC653

ARINC653是一種IMA軟件體系結構,如圖1所示,它包括如下層次結構:應用軟件層,ARINC653系統結構層,實時操作系統層,硬件接口層和硬件層。系統的功能要求包括分區管理、進程管理、時間管理、存儲器管理、分區內通信、分區間通信及健康監控等功能定義[2]。

圖1 ARINC653軟件體系結構

本文的研究重點在應用軟件層,它按資源分配和功能將系統劃分為數個模塊,模塊又劃分為數個分區,分區內包含具體的任務進程。通過引入分區概念,將模塊分為若干個分區,每個分區分配指定的內存空間和處理器時間片。

關于分區的時間調度方面,一個ARINC653系統模塊中有若干分區,每個分區下對應著各自的任務集合。將系統處理器時間按時間片的方式分配給各個分區,各個分區下的任務集合在相應分派的時間片下運行,當時間片用完時暫停執行,直到下一個時間片的到來。不同于普通的系統調度模型,分區調度模型包含兩級調度策略,如圖2所示。

圖2 ARINC653分區系統調度框架

(1)分區間調度。分區間的調度是第1級調度,調度周期是固定的。每個分區周期性地分配到處理器時間。

(2)分區內調度。分區內調度是第2級調度,指分區內進程間的調度。分區內調度是由操作系統根據分區的調度策略來對任務進程集進行時間分配。與分區間調度不同,它是可搶占式的調度策略,如最早截止期優先(EDF)、空閑時間優先(LLF)、速率單調調度(RMS)、截止時間單調調度(DMS)等。每個任務具體分配到的時間片是無法通過配置來指定的,因此,無法直接判定每個任務是否都能滿足它的可調度性。

在調度系統中,如果一個任務在每次到達之后都能在其截止時間限內執行完成,則判定該任務可調度,否則該任務不可調度。從而對任務可調度性的判定即對任務在截止時間期限內是否執行完成的判定。如果ARINC653分區系統中的所有任務都能在各自的截止時間限內執行完成,則判定分區系統可調度,否則,判定分區系統不可調度。本文即針對分區系統的可調度性判定方法進行研究。

2.2 AADL

AADL用于設計和分析系統的軟硬件結構,包括獨立的組件和它們的交互,尤其適用于性能關鍵的實時嵌入式系統。AADL的組件包括軟件類、執行平臺類和系統類。軟件類包含數據、子程序、線程、線程組、進程5類組件;執行平臺類包含處理器、存儲器、設備、總線4類組件;系統類的系統組件是作為軟件類組件和執行平臺類組件的集成組件而設計的[3]。

本節將重點介紹AADL的線程、進程和處理器組件,因為這些組件將運用到ARINC653調度模型的建模。AADL的線程組件是一段執行程序段,這些程序段可以使用Ada任務來表示。根據任務的激活模式,線程類型可以分為周期線程、非周期線程、零星線程。周期線程在固定的時間間隔下被激活,這個固定的時間間隔稱為周期,非周期線程在系統的任何時間被激活,沒有任何規律性,零星線程在一個最小的時間間隔下被激活。AADL的進程組件提供了虛擬的時間和地址空間,每個進程下的需求資源都是獨立和隔離的。AADL的處理器組件提供了線程運行的需求資源。線程、進程和處理器組件將用于對ARINC653系統分區調度中任務進程、分區、模塊的建模。

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

2.3 Cheddar

Cheddar是一個免費的實時調度工具,專用于檢查實時系統中的任務時間約束[5]。借助于Ocarina[7],它可以用來分析AADL模型的可調度性。Cheddar提供了一套類Ada語言(Cheddar語言[6]),使用這個語言可以設計用戶自定義的調度策略。正是基于Cheddar的調度策略的可擴展性,可以使用AADL對ARINC653分區調度系統進行建模,同時使用Cheddar工具進行分區調度的可調度性分析。

Cheddar提供2種調度分析功能:可行性測試和仿真。可行性測試允許用戶不進行調度模擬,根據已有的調度理論,研究實時應用程序、系統是否可調度。相反,仿真首先進行調度模擬,其次根據任務的約束屬性判斷任務的可調度性。可行性測試是簡單不復雜的,文獻[8]介紹了在幾種經典調度策略下進行可行性測試的方法。不過,由于多層級調度策略的復雜性,當前還沒有相應的可行性測試的方法。ARINC653系統是分區系統,采用的是多層級的調度策略,本文根據自主設計的調度策略,通過仿真的方法對多層級調度系統進行可調度性分析和判定。

3 相關工作

目前,安全關鍵系統已經廣泛應用于許多安全領域,如航空航天、汽車、醫藥等領域,同時,這也導致系統越來越復雜。ARINC653就是一種航空電子設備標準,它提供了一種時間和空間隔離的分區方式,來提高系統的安全性。

為避免系統中的錯誤帶來嚴重的后果,文獻[9-10]介紹了幾種方法用來檢測安全關鍵系統的潛質錯誤。不過這些方法依賴于不同的符號和語言,在整個開發階段無法統一,所以基于模型驅動的安全系統的分析方法被提出來[11]。使用模型驅動的方法分析安全系統已經被應用在多個項目中(Flex-eWare[12], SAVI[13])。

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

針對分區系統的可調度判定的研究,文獻[18]在任務時間需求函數的基礎上,計算系統消耗時間,得出了系統可調度性的判定定理。文獻[19]分析了分區參數對任務調度實時性的影響,針對周期和零星任務,通過計算任務的響應時間上界,推導出分區調度下的任務可調度條件。文獻[20]設計并實現了時間分析工具IMATime,對分區系統FCOS進行三級分析,同時提供分區周期和分區容限。

4 基于AADL的ARINC653分區系統建模方法

使用Cheddar對ARINC653分區系統進行可調度分析前,必須先使用AADL對系統進行建模,本節將介紹借助于Cheddar擴展屬性,如何使用AADL對 ARINC653分區系統進行建模。為使AADL能對ARINC653系統進行建模,必須找出AADL模型元素與ARINC653系統概念的對應關系。本節將介紹調度方面的對應規則以及Cheddar擴展屬性的應用,同時給出如何在Cheddar中自定義調度策略,并根據上述的對應規則給出一個分區系統建模實例。

4.1 AADL與ARINC653的對應規則

4.1.1 模塊對應規則

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

4.1.2 分區對應規則

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

分區內調度策略的定義方法與上述介紹的模塊下分區間調度策略類似,本文不再詳述。

4.1.3 進程對應規則

ARINC653進程是系統執行主體,它包含了執行代碼、執行數據和堆棧區域等。一個分區可以包含多個進程,來實現相應的應用功能。分區通過指明進程的調度策略、搶占策略、最大響應時間、內存分配情況等信息來控制進程的執行。而AADL中的thread組件是系統最基本的調度執行單元,通過時間周期或者外部事件來執行線程。線程間的通信可以通過端口連接、子程序調用和共享數據來實現。因此,可以使用AADL的thread組件表示ARINC653進程概念,因為它們有相同的概念:執行主體。執行主體所需要的特征可以用AADL屬性來定義,包括執行周期、執行截止時間、執行時間和調度策略等。AADL中的thread組件包含在process組件中就像ARINC653中的進程包含在分區中一樣。thread組件屬性Dispatch_Protocol定義線程類型即激活模式(如周期、非周期、零星等),Compute_Execution_ Time定義線程的執行時間,Period定義周期線程的周期值,Deadline定義線程最壞響應時間。

圖3總結了上述的對應規則,即給出了使用AADL中的哪些組件和屬性對ARINC653系統分區調度信息進行建模。比如使用AADL中的處理器組件給ARINC653中的模塊建模,其中使用組件屬性Thread_Properties::Scheduling_Protocol表示模塊下分區所采用的調度策略。依賴于表格中的AADL標準屬性和以Cheddar_Properties::開頭的Cheddar擴展屬性生成的AADL模型,Cheddar工具就可以進一步進行可調度性分析和判定。

圖3 AADL與ARINC653對應規則

4.2 Cheddar自定義調度策略

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

使用Cheddar語言定義的調度策略Ada程序段如下:

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

時間自動機用來表示線程狀態的時間轉換情況,可以用實時系統驗證工具UPPAAL生成。使用時間自動機的節點,時間約束和變量值表示系統的狀態。每個時間自動機的轉換可以是獨立的,也可以與其他的時間自動機同步進行狀態轉換。使用時間自動機來表示任務的運行和切換,使用時間約束來控制狀態轉換過程。Cheddar使用時間自動機對線程調度進行建模,并運行上述的類Ada語言程序段,讀寫仿真數據。

在Cheddar中定義的一個時間自動機的代碼示例如下:

首先定義一個狀態Ready,即自動機的初始化狀態,再定義一個狀態遷移關系,從狀態Ready遷移到狀態Ready,即系統都處在狀態Ready。狀態轉換包含3個部分:變量更新,判定條件,同步信號,該示例中變量更新和判定條件是沒有的,不過存在一個同步信號。當處在Ready狀態的線程接收到election_ name同步信號(上文Ada程序段中election_section調度完畢后系統會發出election_name信號)時,會發生狀態遷移,狀態再次遷移到Ready。

針對分區調度系統,通過定義2種不同的調度策略,一種用于分區間調度,另一種用于分區內任務調度。2種調度策略之間通過同步信號來同步和交互,完成多層級調度,具體見下節的建模實例分析。

4.3 建模實例分析

本節將給出一個建模的例子,介紹如何借助于Cheddar擴展屬性,使用AADL對ARINC653系統的分區調度模型進行建模,建模流程如圖4所示。首先根據系統的調度信息,使用Cheddar設計相應的調度策略,其次依賴于 4.1節介紹的 AADL與ARINC653的對應規則和調度策略,分別使用AADL的thread組件、process組件和processor組件對系統中的進程、分區、模塊建模,同時,將設計好的調度策略賦予組件屬性。

圖4 ARINC653分區系統建模過程

表1是ARINC653系統分區間和分區內的調度信息,詳細描述了一個總時間框架下(時間片大小是10 ms)分區集和各分區任務集的調度情況。系統包含有2個分區(partion1和partion2),每個分區包含有2個任務,調度策略分別是DMS和RMS。

表1 ARINC653系統調度信息 ms

使用AADL對上述ARINC653分區系統調度信息進行建模,得到模型如下:

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

AADL屬性Compute_Execution_Time,Dispatch_ Protocol、Period、Deadline等指明了ARINC653系統任務的調度信息,其中,Compute_Execution_Time, Dispatch_Protocol、Period、Deadline等是AADL的標準屬性,指明了任務的執行時間、任務的類型、周期任務的周期時間、任務的截止時間等。

AADL擴展屬性Cheddar_Properties::Scheduling_ Protocol指明調度策略,例子中處理器和2個進程組件都有獨立的調度策略,分別定義了模塊下分區間的調度策略和分區partion1和partion2內的調度策略。模型中arinc.Impl處 理器 組 件 的 Cheddar_Properties:: Scheduling_Protocol屬性值是AUTOMATA_USER_ DEFINED_PROTOCOL指明了分區間的調度策略是Cheddar自定義的時間自動機,使用時間自動機表示線程的狀態轉移情況。Cheddar_Properties::Source_Text屬性值指明了時間自動機所在的文件名,arinc_ processor.sc包含了分區間調度的Cheddar程序段和時間自動機。partition1和partition2進程組件屬性值與處理器組件相同,不過調度策略所在的文件不同。arinc_ partition1.sc和arinc partition2.sc文件分別包含了這2個分區的調度策略。

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

圖5 調度時間自動機

文本內容基本相似,本文不再贅述。

5 基于Cheddar的可調度性判定

本文針對含有純周期任務的分區系統的可調度性判定問題,提出一種基于仿真方法實現的可調度性判定方法,具體流程如圖6所示。該方法通過設定時鐘變量來模擬任務調度過程中的系統時鐘,在時鐘變量值增長過程中,根據任務優先級從高到低的順序分析各個任務約束屬性的滿足情況,判定任務的可調度性,從而判定分區系統的可調度性。

圖6 可調度性判定流程

由于分區系統下調度模型的多樣性,以及本文提出的可調度性分析方法的局限性,需要對調度模型進行限制。下文將介紹可進行可調度判定的分區調度模型和進行可調度性判定方法的理論依據,并給出基于上述描述的分區系統進行可調度性判定的實例。

5.1 ARINC653分區系統的調度模型

ARINC653分區系統相應調度模型描述如下: (1)系統中有若干個分區,分區間可以進行通信,但分區之間在時間和空間上彼此獨立。

(2)系統為各分區分派時間片,各分區的時間片都有時間片開始時間(offset)和時間片大小(duration)2個參數,系統周期性地為分區分派時間片。

(3)系統可為各分區設定相互獨立的分區內任務集調度策略。

(4)各分區內的任務集在各自分區分派的時間片內按照相應的調度策略調度執行,不受其他分區任務的干擾,任務集在執行過程中遇到時間片用完時,暫停執行過程,等待下一個時間片的到達。

(5)分區下的所有任務都是周期任務,且任務的周期等于任務的截止時間,具有硬實時系統的強時間限定,即必須在各任務的截止時間內完成,否則分區任務集不可調度。

(6)調度中忽略任務間切換的時間。

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

(8)只針對時間約束分析,默認任務所需的其他非時間資源都滿足要求。任務的可調度性判定等價于判定任務的時間約束是否滿足。

5.2 理論依據

針對非分區系統的調度模型,任務集下的所有任務都是周期任務,且各個任務的分派到達僅依賴于其相應的周期。因此,任務第一次到達以后的所有到達時刻都是確定的,用設定系統時鐘變量來模擬調度過程的方法是可行的。

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

針對分區系統和上述限定的調度模型,分區周期性獲得系統分派的時間片。各分區下任務集中所有任務都是周期任務,因此,所有任務的觸發到達呈周期性。在分區調度模型中,所有任務的到達執行與所在分區的時間片分派情況整體上呈周期性,周期值為所有任務周期值與分區獲得時間片的周期值的最小公倍數。

依據上述周期最小公倍數理論可知,任務的執行過程呈周期性往復執行,因此本文在用仿真方法模擬任務調度過程判定任務集的可調度性的實現過程中,將系統時鐘設定為一個周期值的時鐘區域,分析任務集在此周期內的調度情況,從而等價描述系統時鐘中剩余時間區域的可調度情況。因為任務執行過程中的確定性和周期性,所以系統時鐘的選取是確定的有窮的時鐘區域,因此,用仿真方法判定分區調度模型的可調度性是可行的。

5.3 仿真實例分析

表1描述了分區系統的任務調度信息,系統包含4個周期任務且周期等于截止時間。調度信息滿足上述的可進行可調度性判定的調度模型。這4個周期任務的周期分別是10 ms,5 ms,20 ms,10 ms,最小公倍數是20 ms,分區獲得時間片的周期是10 ms,所以所有任務周期與分區獲得時間片的周期的最小公倍數是20 ms,即仿真時長是20 ms。

根據第4節介紹的內容,將包含表1分區調度信息的AADL模型作為Cheddar工具的輸入,同時,編輯好自定義的調度策略,設置好仿真時長,調度結果如圖7所示。

圖7 調度仿真結果

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

調度結果圖中下半部分給出了可調度性判定,判定結果是可調度的,同時列出了每個任務的最壞響應時間,滿足任務的截止時間要求。

6 結束語

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

[1] 易建平,韓 慶.飛機綜合模塊化航電系統總體設計研究[J].科學技術與工程,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行為模型驗證方法研究[J].計算機科學,2012,39(2):159-161.

[18] 何 峰,宋麗茹,熊華鋼.航空電子雙層任務分區調度設計[J].北京航空航天大學學報,2008,34(11): 1364-1368.

[19] 周天然,熊華鋼.航空電子系統混合實時任務的雙層調度[J].航空學報,2011,32(6):1067-1074.

[20] 湯小明,張新國.基于分區的安全關鍵軟件體系及其時間分析研究[J].系統仿真學報,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

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

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

2013-08-27

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

中文引用格式:袁 翔,胡 軍,馬金晶,等.基于AADL的綜合航電分區系統可調度性判定[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.