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

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

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

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

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

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

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

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

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

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

1 概述

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

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

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

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

2 背景知識

2.1 ARINC653

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

圖1 ARINC653軟件體系結構

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

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

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

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

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

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

2.2 AADL

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

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

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

2.3 Cheddar

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

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

3 相關工作

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

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

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

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

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

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

4.1 AADL與ARINC653的對應規(guī)則

4.1.1 模塊對應規(guī)則

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

4.1.2 分區(qū)對應規(guī)則

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

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

4.1.3 進程對應規(guī)則

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

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

圖3 AADL與ARINC653對應規(guī)則

4.2 Cheddar自定義調度策略

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

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

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

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

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

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

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

4.3 建模實例分析

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

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

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

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

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

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

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

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

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

圖5 調度時間自動機

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

5 基于Cheddar的可調度性判定

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

圖6 可調度性判定流程

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

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

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

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

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

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

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

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

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

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

5.2 理論依據(jù)

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

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

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

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

5.3 仿真實例分析

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

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

圖7 調度仿真結果

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

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

6 結束語

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

[1] 易建平,韓 慶.飛機綜合模塊化航電系統(tǒng)總體設計研究[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] 何 峰,宋麗茹,熊華鋼.航空電子雙層任務分區(qū)調度設計[J].北京航空航天大學學報,2008,34(11): 1364-1368.

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

[20] 湯小明,張新國.基于分區(qū)的安全關鍵軟件體系及其時間分析研究[J].系統(tǒng)仿真學報,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);江蘇省普通高校研究生科研創(chuàng)新計劃基金資助項目(CXZZ11_0218)。

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

2013-08-27

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

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