基于AADL的嵌入式系統可調度性驗證

孫 健，徐 敏

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

基于AADL的嵌入式系統可調度性驗證

孫 健，徐 敏

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

AADL近年來在嵌入式實時系統領域得到了廣泛的應用，相對于其他語言能夠更好地描述系統的非功能屬性，同時支持系統軟硬件建模，在基于模型驅動的開發方法下對系統進行建模和分析，用形式化的方法對系統的相關屬性進行驗證，從而可以在設計階段發現錯誤，對保證系統的安全運行和開發效率的提高有著重要意義。對于驗證AADL模型可調度性的問題，文中利用時間自動機理論，根據AADL調度模型和時間自動機模型的語義相似性，將AADL模型轉換成時間自動機模型，并設計轉換插件，通過Eclipse插件開發技術將其集成到AADL建模與分析工具OSATE中。最后在UPPAAL工具中對轉換后的時間自動機模型進行模擬和驗證，利用相關性質驗證語句等價地對原模型的可調度性進行驗證。

嵌入式系統；體系結構分析設計語言；時間自動機；模型轉換；UPPAAL；實時性

0 引 言

對于安全關鍵的嵌入式系統來說，系統的非功能屬性跟功能屬性一樣重要，都需要得到滿足[1-2]。基于模型驅動的方法可對系統設計和安全性分析采用一致的模型，該模型貫穿整個開發過程[3]。在系統設計階段，通過對模型分析和驗證，發現錯誤來提高系統的安全性，保證系統能夠正常運行，從而提高開發效率。

體系結構分析設計語言(Architecture Analysis and Design Language，AADL)近年來在航空電子領域以及安全性分析等方面得到了廣泛應用，是一種符合模型驅動思想的建模和分析語言，在2004年由SAE基于MetaH和UML提出，并發布為SAEAS5506標準，能對系統的軟硬件進行建模。隨著AADL的廣泛應用以及對內容的擴展，與AADL相關的研究工作及其工具的開發日益成為研究熱點。

時間自動機建模與分析工具UPPAAL近年來在實時系統中得到廣泛應用，具有建模功能靈活、驗證效率高等特點，也在AADL建模與分析中得到了嘗試[4-5]。其中，Johnsen在文獻[6]中提出用UPPAAL進行建模，并在模擬器和驗證器中對模型進行模擬和驗證，且模型的調度策略是固定優先級的；劉倩等使用UPPAAL對AADL非可搶占調度模型設計了時間自動機[7]。上述研究存在的問題是調度策略單一，沒有考慮到線程切換中的時間消耗，從而對于實際的AADL模型不能很好地進行模擬，且其考慮的問題還停在了對自動機的建模和驗證上，而對于AADL模型轉換為時間自動機模型，以及轉換插件的設計都還沒較多的涉及。

針對上述問題，利用時間自動機理論，根據AADL調度模型和時間自動機模型的語義相似性，將AADL模型轉換成時間自動機模型，并設計轉換插件，在UPPAAL工具中對轉換后的時間自動機模型進行模擬和驗證，利用相關性質驗證語句等價地對原模型的可調度性進行驗證。

1 AADL與UPPAAL

1.1 AADL概述

在AADL中，組件通過類型和實現聲明來定義[8]。一個組件類型說明定義了一個組件的接口元素以及外部可觀察屬性(即與其他組件、流程規范和內部屬性值之間交互點的特性)。一個組件實現的聲明定義了一個組件內部結構的子組件、子組件連接、子程序調用、模式、流實現以及屬性。組件被分為應用程序軟件，執行平臺和復合組件，屬性集和附件庫使得設計者能夠擴展語言和自定義一個AADL規范來符合項目或特定區域的需求。

組件在特定的組件類別中聲明為類型和實現，有三組不同的組件類別：應用軟件、執行平臺和復合。一個AADL組件類型聲明建立了一個組件的外部可見特性[7]。例如，一個聲明指定了一個線程組件的接口，一個組件類型聲明由一個定義句子和描述性的子句組成，特征(features)是組件的接口，流(flows)指定信息流的不同抽象通道，屬性(properties)定義組件的固有特性，每個組件類別都有預定義的屬性(如一個線程的執行時間)。組件的實現就是用來描述一個組件的內部結構，一個組件實現包括的子句主要有：流，屬性，模式和子組件。流(flows)代表組件類型里流規范的實現或者端到端的流分析(流從一個子組件開始，經過零個或更多子組件并在另一個子組件結束)；模式(modes)是對組件、連接及屬性值的配置，表示一個系統或組件可達到的操作狀態；屬性(properties)定義組件的固有特性，每個組件的實現都有預定義的屬性。

1.2 時間自動機與UPPAAL概述

1.2.1 時間自動機理論

時間自動機[9]理論最早是在1992年由Alur R提出，在有限狀態自動機上擴充了時鐘、時鐘約束及不變條件而得到。時間自動機被提出是實時系統建模自動機理論的擴展，從此時間自動機理論及其驗證工具一直是計算機科學研究的一個密集領域。一個時間自動機是一個配備了一組有限時鐘的有限自動機，時鐘是時間的連續的實值函數，精確地記錄時間的流逝。所有時鐘以相同的速度前進，即它們是同步的，實時系統行為使用時間自動機來捕獲，通過設置時鐘以及用常數比較時鐘讀數[10]。所有時鐘都有和時間相關的相同的衍生物，且都被假定為一個相同的定義。

下面根據時間自動機的定義，做如下說明[11]：

定義1：狀態轉移系統。

將狀態轉移系統形式化為四元組。其中：T為轉移系統中的狀態集合；t0(t0∈T)為初始狀態；P為觸發狀態發生轉移的事件集合；E?T×P×T為所有狀態轉移的集合。

在一個系統中，一個狀態在觸發事件的作用下發生狀態轉移，若一個狀態到另一個狀態的轉移發生則稱該狀態到另一狀態是可到達的，而從初始狀態開始，所有可到達其他狀態的轉移構成了狀態空間。

定義2：時鐘約束。

把φ(C)作為時鐘約束集合，其中C為時鐘變量集，定義時鐘約束集合為：

φ:=x??n|φ1∧φ2

其中：x是一個時鐘變量；n是一個自然數集N中的常量。

定義3：時鐘解釋。

時鐘解釋v:C→N表示集合C到自然數的映射。

對于一個δ∈R，R表示的時鐘解釋是對于集合C中的每一個時鐘變量x的賦值為v(x)+δ；對于一個δ∈R，δ·v表示的時鐘解釋是對C中的每個時鐘變量x賦值為δ·v(x)；對于X?C，v[X:=0]表示對于滿足x∈X的時鐘x復位為0，其余時鐘保持增長。

定義4：時間自動機。

在有限狀態自動機的基礎上，通過增加時鐘變量的概念形成了時間自動機，其中時鐘為整型變量，并且所有的時鐘變量是同步遞增的[12-14]。一個時間自動機可以表示為一個六元組，TA=。其中：T為有向圖中有窮的位置(location)集合；t0為自動機的初始狀態；C為時鐘集合，默認從0開始，不斷自增加1，可以隨時被重新賦值；V為所有變量的集合；E為有向圖中所有邊(edge)的集合；I為狀態轉移約束函數的集合，即不變條件(invariant)。

1.2.2 驗證工具UPPAAL

UPPAAL[7]是一個基于約束求解和動態技術的，用來進行實時系統建模、仿真和驗證的工具，它可以將系統建模成一系列具有有限控制結構和實值時鐘的非確定性的進程，并通過共享變量進行通信。典型的應用領域包括實時控制器和特別的通信協議，時間方面是十分關鍵的，所以在設計方面，主要是通過探索系統的狀態空間來檢查不變和可達性。

UPPAAL工具的兩個設計標準是效率和易于使用，可達性分析的限制對于工具的模型檢查器的效率至關重要。對效率的另一個關鍵是結合符號技術的動態搜索技術的應用，減少為處理和解決簡單約束的驗證問題。為了方便建模和調試，UPPAAL模型檢查器會自動生成一個診斷跟蹤，來解釋為什么一個屬性滿足(或不滿足)一個系統描述，由模型檢查器生成的診斷跟蹤可以使用模擬器來圖形化顯示。

2 AADL可調度模型轉換與驗證

為了驗證實時系統AADL模型中的可調度性，利用時間自動機形式化方法。首先分析AADL模型，將與系統調度相關的屬性信息提取出來，抽象出調度模型。在非可搶占及可搶占調度策略下，分別設計了線程和調度器時間自動機模板(以下簡稱模板)，并利用TCTL驗證語句對UPPAAL中的時間自動機模型進行可調度性驗證。最后設計了從AADL調度模型到時間自動機模型的轉換插件，并自動調用UPPAAL打開模型對相關性質進行驗證。

2.1 非可搶占調度策略下的時間自動機設計

(1)線程模板。

線程是執行的主體，線程組件也是通過線程模板來進行轉換，在線程模擬的過程中，用標號id來區分，在非可搶占策略下設計了如圖1所示的周期線程時間自動機模板。

圖1 非可搶占調度策略下周期線程時間自動機模板

如圖1所示，模板中有四個狀態，分別為初始化狀態(Initialized)、準備狀態(Ready)、錯誤狀態(Error)及運行狀態(Running)。Initialized狀態表示線程創建成功且處于等待被派發的狀態，其中不變條件cl<=Period代表線程處于Initialized狀態的條件為局部時鐘小于等于周期；Ready表示線程按照優先級的高低進入到等待隊列，等待被處理器執行；Running狀態對應于線程狀態轉換機制中的Compute(計算)狀態，表示線程正在被運行；Error狀態對應于線程狀態轉換機制中的Recover(恢復)狀態，表示線程由于超時而進入到一種死鎖狀態，且所有的狀態轉移在該狀態下都會中止。

(2)調度器模板。

根據并發系統的特點，即線程會根據調度策略通過調度器來決定其運行狀況，于是在調度器時間自動機模板的設計過程中，利用同步通道以及全局變量與線程進行通信，對組件調度屬性進行模擬，設計的調度器模板如圖2所示。

圖2 非可搶占調度策略下調度器時間自動機模板

從圖中可以看出，調度器模板有如下五個狀態：等待狀態(Awaiting)、調度狀態(Schedule)、運行狀態(Running)、完成狀態(Completed)、超時狀態(MissedDeadline)。其中調度狀態、完成狀態為限制狀態，即不考慮時間的流逝，為中間狀態。Awaiting狀態表示在處理器中沒有要調度執行的線程；Schedule是一種中間狀態，調度器會在有線程被派發時進入到該狀態；Running狀態表示線程的運行狀態，模擬線程在處理器上的運行；Completed狀態表示線程運行完畢，進入該狀態的條件為線程實際運行時間與需要的最大運行時間相等；MissedDeadline狀態表示線程運行超時，沒有在截止時間之前完成運行，當系統進入到此狀態便會發生死鎖，即該系統不可調度。

(3)帶有線程切換時間下的非可搶占調度器模板。

線程在切換時產生了時間的消耗，并在模型中用Thread_Swap_Execution_Time表示線程切換過程所產生的時間消耗。因此本節擴展了模板，用switch_clock表示切換時鐘，用switch_clock<=switchTime模擬某狀態的時間切換。

擴充后的模板中，switchTime若為0，則表示該調度器模板不考慮切換時間，但在實際情況中，新增加的判斷條件可能會帶來很大的影響和負擔，因此將其轉換到對應的模板顯得尤為重要。

2.2 可搶占調度策略下時間自動機設計

(1)線程模板。

相對于非可搶占調度策略，在可搶占調度策略下，周期線程時間自動機模板增加了一個Preempted狀態。該狀態表示線程在運行時被更高優先級的線程搶占后停止運行，等到更高優先線程運行完之后，該線程恢復運行，返回到Running狀態，其中該狀態上的截止時鐘是持續增長的。

(2)調度器模板。

由于引入了線程的搶占、恢復等操作，在可搶占調度策略下，調度器模板的復雜程度相對來說要大些。在非可搶占的調度器模板基礎上，該模板增加了兩個狀態Schedule1和Preemption。其中：Schedule1是一種中間狀態，調度器在有線程被派發時會進入到此狀態，同時線程會在調度器中按優先級高低排成一個隊列ready_q；Preemeption狀態表示有新線程派發時Schedule1決定執行可搶占調度，并按優先級由高到低依次進入運行狀態，且被搶占的線程會進入到被搶占狀態。

(3)帶有線程切換時間下的可搶占調度器模板。

線程在可搶占調度策略下，因搶占而產生時間的消耗，所以線程在恢復到執行狀態時被搶占時間的計算會有所不同。

2.3 模型轉換器的工具實現

對于模型的自動轉換，通過Eclipse插件開發技術設計了轉換插件，并將其集成到了AADL建模與分析工具OSATE中，實現了AADL模型到時間自動機模型的自動轉換。插件以實例化的AADL模型作為輸入，通過文件解析，轉換生成時間自動機模型文件和性質驗證查詢文件，自動調用UPPAAL工具打開模型進行可調度性驗證。

2.4 可調度性驗證

文中使用UPPAAL(時間自動機建模與驗證工具)來驗證設計的時間自動機模型，從而對AADL調度模型進行等價的可調度性驗證。UPPAAL內含有模擬器和驗證器，在模擬器里可以觀察時間自動機的狀態轉移，且可用單步或連續的方式，同時可觀察狀態序列的變化，從而模擬系統的運行。從前面的介紹中可知，在UPPAAL中，模型驗證時所使用的理論是自動機可達性驗證理論。同時在驗證器中使用了時序邏輯TCTL來進行相關屬性的驗證，其性質查詢語言包括狀態公式和路徑公式。而文中在驗證調度模型的可調度性中，用到的主要語句見表1。

3 結束語

文中利用時間自動機的形式化檢驗方法，設計了AADL調度模型到時間自動機模型的轉換方法，在UPPAAL工具中對時間自動機模型進行模擬和驗證，利用相關驗證語句，等價地驗證原模型可調度性。同時設計了不同調度策略下的線程和調度器模板以及自動轉換插件，并將其集成到工具OSATE中，使得嵌入式實時系統的建模、轉換以及驗證實現一體化。

表1 模型可調度性性質驗證語句

對基于時間自動機的AADL模型驗證工作雖然取得了一定進展，但考慮調度策略影響因素時，所關心的還不是很全面，如目前還不支持多處理器和EDF調度算法。在未來的研究工作中，需進一步考慮影響系統調度的因素，從而使得分析和驗證的效果更加全面。

[1] Krishna C M.Real-time systems[M].[s.l.]:John Wiley & Sons,Inc.,1999.

[2] Peled D.Software reliability methods[M].Berlin:Springer,2001.

[3] Selic B.The pragmatics of model-driven development[J].IEEE Software,2003,20(5):19-25.

[4] Bj?rnander S, Seceleanu C.A formal analysis framework for AADL[J].Journal of Science and Technology,2011,49(5):1-13.

[5] Bae K,?lveczky P C,Meseguer J,et al.The SynchAADL2 Maude tool[M].Berlin:Springer,2012.

[6] Johnsen A.Architecture-based verification of dependable embedded systems[D].Sweden:M?lardalen University,2013.

[7] 劉 倩，桂盛霖，李 允,等.基于UPPAAL的AADL模型可調度性驗證[J].計算機應用，2009,29(7)：1820-1824.

[8] 楊志斌，皮 磊,胡 凱,等.復雜嵌入式實時系統體系結構設計與分析語言:AADL[J].軟件學報，2010，21(5)：899-915.

[9] Alur R.Timed automata[M]//Computer aided verification.Berlin:Springer,1999.

[10] 譙婷婷，王 樂，耶國棟.基于AADL的軟件可靠性驗證[J].計算機應用，2012，32：92-95.

[11] 童 超.基于時間自動機的RBC控車流程研究[D].成都:西南交通大學，2009.

[12] 朱雪陽，唐稚松.基于時序邏輯的軟件體系結構描述語言XYZ/ADL[J].軟件學報，2003，14(4)：713-720.

[13] 李振松,顧 斌.基于UPPAAL的AADL行為模型驗證方法研究[J].計算機科學，2012，39(2)：159-161.

[14] 周清雷,姬莉霞,王艷梅.基于UPPAAL的實時系統模型驗證[J].計算機應用，2004，24(9)：129-131.

Schedulability Verification of Embedded System Based on AADL

SUN Jian，XU Min

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

AADL has been widely used in embedded real-time system in recent years.Compared with other languages,it can better describe the system non functional attributes,and also support the software and hardware modeling of the system.AADL can model and analyze the system based on the model driven development method,and verify relevant properties using formal method.Error can be found in the design phase,and it has great significance to ensure the safe operation of the system and improve the efficiency of development.For verifying AADL model schedulability problem,according to the semantics similarity of AADL scheduling model and timed automata model,the theory of timed automata is used to convert AADL model to timed automata model,and integrate conversion plug-in into the AADL modeling and analysis tool OSATE through the development of Eclipse plug-in technology.Finally,the converted timed automaton model in the UPPAAL tool is simulated and verified,using the related verification statement to verify the schedulability of the original model.

embedded system;AADL;timed automata;model transformation;UPPAAL;real-time

2015-06-09

2015-09-15

時間：2016-02-18

國家“973”重點基礎研究發展計劃項目(2014CB744900)

孫 健(1990-)，男，碩士研究生，研究方向為人工智能；徐 敏，副教授，研究方向為人工智能、軟件工程。

http://www.cnki.net/kcms/detail/61.1450.TP.20160218.1630.032.html

TP302

A

1673-629X(2016)03-0023-04

10.3969/j.issn.1673-629X.2016.03.006