一種嵌入式操作系統運行時驗證方法*

張可迪,舒紹嫻,董 威

(國防科學技術大學計算機學院，湖南 長沙 410073)

一種嵌入式操作系統運行時驗證方法*

張可迪,舒紹嫻,董 威

(國防科學技術大學計算機學院，湖南 長沙 410073)

作為測試、模型檢驗等開發階段所用技術的有效補充，運行時驗證技術越來越受到廣泛的關注。然而，當前的運行時驗證技術主要用于應用軟件，很少專門針對操作系統進行研究。對面向嵌入式操作系統的運行時驗證框架和關鍵技術進行了研究，并結合一個開源嵌入式操作系統FreeRTOS進行了設計與實現。首先提出了一種面向嵌入式操作系統的運行時驗證和反饋調整框架，然后針對框架中的關鍵技術部分，完成了規約語言的設計、三值語義監控器的生成、FreeRTOS嵌入式操作系統相關接口的實現等主要工作。

嵌入式操作系統;FreeRTOS;運行時驗證;規約語言;三值語義監控器

1 引言

目前計算機技術的應用領域日益廣泛，從傳統到高新，從軍事到民生，都與計算機技術密不可分。然而隨著計算機應用中軟件所占部分規模的日益擴大，如何提高軟件的可靠性和安全性受到了學術界和工業界的廣泛關注和深入研究。人們為確保軟件的正確性、可靠性、安全性、可用性和可維護性，在設計、編碼、測試等不同階段不遺余力地采取各種各樣的方法和手段。但是，由于軟件自身特性，軟件失效仍然難以避免，尤其是關鍵軟件的可靠性、安全性問題仍然面臨嚴峻挑戰。

運行時驗證[1]是一種新興的輕量級程序驗證技術。在運行時驗證中，通常從系統需求中產生監控器，監控器通過觀測程序的執行來檢查程序運行過程是否滿足系統需求，是傳統的軟件驗證和確認技術如測試[2]和模型驗證[3]的有效補充。它不但可以有效地檢測系統運行中的異常行為，也使得在檢測到正確性背離問題時有效地修復系統成為可能。

傳統的運行時驗證技術主要針對實際的應用程序，關注應用程序本身的運行過程是否滿足系統需求，忽視了對可能在操作系統一級出現的如任務沖突或任務調度、資源使用等過程不滿足事先設計等軟件失效的監控。這是由于操作系統本身的控制調度十分復雜，監控軟件要對其內核運行過程進行訪問和操作來獲取監控信息或執行反饋動作十分不易。而嵌入式操作系統結構相對簡單，其在航空航天、國防等領域又非常關鍵，例如許多航天系統對操作系統中的任務執行過程都有嚴格限制，不僅關注具體狀態，還對執行的時序、資源分配等有具體要求，因此嵌入式操作系統的運行過程采用運行時驗證技術進行監控非常有必要。同時，只要在嵌入式操作系統內核中加入提供可供監控器使用的數據獲取接口，可使其運行時驗證成為可能。

本文主要針對嵌入式操作系統的運行時驗證技術展開研究，并結合FreeRTOS嵌入式操作系統提出了一種面向嵌入式操作系統的運行時驗證框架，實現了對嵌入式操作系統調度過程信息的獲取，并通過從事先編寫好的規約自動生成監控器以對系統的運行軌跡進行監控，當系統的運行軌跡發生異常時，能夠執行相應的反饋操作盡量避免違反規約的情況發生。

本文的組織如下：第2節介紹該方法的整體框架，第3節介紹相關的規約語言，第4節進行FreeRTOS監控接口和反饋接口的設計，第5節闡述了監控器的構造與實現，最后對文章進行了總結并對下一步工作進行概述。

2 整體架構

本文研究的問題根據運行時驗證的主要工作流程，可以分解為以下幾個子問題：

(1)如何定義嵌入式操作系統應該滿足的性質規約和相關的關鍵屬性，如何建立關鍵屬性與性質規約之間的聯系；

(2)如何在系統運行過程中提取系統關鍵屬性的相關信息；

(3)如何在目標系統和監控器之間傳遞信息；

(4)如何從性質規約生成監控器模型，并實現能在違反規約時執行反饋動作的監控程序。

針對上面四個子問題，解決方案分別如下：

(1)將使用線性時序邏輯LTL(Line Temporal Logic)公式描述軟件系統應該滿足的性質規約，構造為基于LTL三值語義的運行時監控器；通過借鑒經典的運行時驗證框架，引入一套事件和條件機制，給出擴展的事件定義語言EDL(Event Definition Language)。按照事件定義語言的規定，由目標系統的關鍵屬性抽象出一組事件和條件，同時將這些事件和條件作為待驗證的性質即LTL公式的謂詞。這樣，就在目標系統的關鍵屬性和待驗證的性質規約之間建立起了聯系。

(2)本文選用的嵌入式操作系統是FreeRTOS[4]，該操作系統為開源代碼，主要由C語言以及少量的匯編語言編寫而成，這符合很多現實應用的需要(許多關鍵領域如我國航天領域的代碼都是由C語言編寫而成)。對于C語言，不能像Java語言那樣方便地進行相關監控代碼的自動插裝，這主要是由于它不存在用于給插裝工具定位用的字節碼和“類”結構。與應用程序的運行時驗證相比，操作系統的運行時驗證還存在以下特點：

①操作系統的功能和結構相對確定，而不同的應用程序其功能和設計結構區別很大。

②操作系統的內核在運行時訪問受限，而應用程序則沒有這種限制。

③操作系統要監控的內容和性質相對比較確定，而應用程序則因不同的需求而異。

結合嵌入式操作系統的特性，可以確定在運行時通過自動插裝的方法到操作系統內核中去獲取信息難以實現，因為運行時在內核中進行插裝操作是不安全和不穩定的。而由于操作系統相對固定的結構和相對確定的監控屬性類型，本文將不采用程序自動插裝的方式，而是在FreeRTOS嵌入式操作系統中提前定義并實現相關監控接口，以提取系統關鍵屬性的信息。

(3)根據航天等領域的實際應用現狀，操作系統監控接口本身將獲取的數據以日志的形式進行存儲和傳輸，監控程序通過對日志的訪問分析獲取監控信息。

(4)使用開源軟件LTL3 Tools可以在輸入LTL公式后自動生成監控器模型，根據監控器模型通過JavaMOP形成監控程序，同時要在FreeRTOS嵌入式操作系統中加入能夠接受反饋控制指令的接口。

根據問題和解決方案，本文提出一種面向嵌入式操作系統的的運行時驗證框架，如圖1所示。

根據圖1中嵌入式操作系統運行時驗證的框架，本文將從規約語言的設計、操作系統的擴展、監控器的構造與實現三個方面進行具體工作的闡述。

Figure 1 Runtime verification framework based on embedded operating system圖1 基于嵌入式操作系統的運行時驗證框架

3 規約語言

3.1 事件與條件定義語言

線性時序邏輯LTL[5]是在命題邏輯的基礎上加上時序操作而得來的，基于線性時序邏輯的規約與驗證是描述和驗證軟件系統的一類重要形式化方法，最終監控器要監控的性質就是由LTL公式描述。為了將系統的“高層規約”與程序相關的“底層信息”聯系起來，作者借鑒了經典的運行時驗證框架MaC[6]中的事件和條件機制。將事件定義為某個時刻發生的一個動作，條件則定義為某一段時間成立的一個命題。比如進入或者退出某個方法是一個事件，而像x=1之類表示程序在某一段時間內成立的一個命題則表示一個條件。下面介紹針對操作系統和時序邏輯的需要進行擴展后的事件與條件機制。

(1)語法。

條件由原子條件C通過邏輯符號相連遞歸而成。其中的原子條件是指程序中某些屬性抽象而成的一個條件，比如由監控的變量通過簡單的符號連接形成真假表達式，原子條件的定義在面向嵌入式操作系統的運行時驗證框架中和在MaC中的定義類似，并不需要擴充。同樣，事件由原子事件E通過邏輯符號連接遞歸而成，MaC定義的一些原子事件的關注對象是方法和變量，因為它監控的對象是應用程序。而當主要的關注對象是操作系統運行過程與任務、中斷、資源等相關的內容時，則要定義一部分適用于操作系統的原子事件，這些原子事件與條件能用于方便地描述操作系統的具體信息。另外，MaC中定義的事件與條件機制只滿足了部分邏輯表達的能力，但要完全表達LTL公式中的時序邏輯關系還有很大不足，因此要對事件與條件機制進行相應的擴展。

條件〈C〉和事件〈E〉擴展后的語法定義如圖2所示，其中〈TC〉是對條件關于線性時序邏輯部分的擴展，〈atomE〉是針對于操作系統中的原子事件的定義。

(2)語義。

Figure 3 Semantics for event &condition and atom E formal difinition圖3 事件與條件和針對于操作系統的 原子事件atom E的形式化定義語義

首先定義模型M為二元組{S,τ}，其中S={s1,s2,…,}，τ是S到時間域的一個映射,即τ(Si)表示事件S發生的時間。若模型M中條件c在時間t下值為true，則表示為(M,tc)；同理，若事件在時間t發生，則表示為(M,te)。事件與條件的形式化語義如圖3a所示，針對操作系統的原子事件atom E的形式化定義語義如圖3b所示。

3.2 事件定義語言

在面向嵌入式操作系統的運行時驗證方法框架中，事件和條件分為由目標系統中的變量和方法抽象而成的原子事件和條件，以及由原子事件和條件構成的復合事件和條件兩種。

為了準確描述原子事件和條件以及復合事件和條件，本文在事件定義語言的基礎之上引進了MaC-Java[7]中的原子事件定義語言(PEDL)和復合事件定義語言(MEDL)[8]，它們分別用PEDL規約和MEDL規約描述。其中PEDL規約中描述了原子事件和條件是如何由目標系統中的變量和方法抽象而成；而MEDL規約中描述了原子事件和條件如何組成復合事件和條件，即構成監控器要使用的時序性質謂詞，同時聲明要使用的反饋動作。而與MaC-Java中PEDL、MEDL語言不同，因為當前不能實現自動插裝來獲取相應的信息，針對的目標也是C語言，所以具體的語法要重新設計。其功能上主要是為了能規范地描述事件與條件，方便生成相關的代碼，并為構造監控器提供用于連接底層信息與高層規約的謂詞。

PEDL規約腳本包含三個主要部分：導出事件和條件部分、監控對象聲明部分、事件和條件定義部分并以Mobscr開頭和END結尾。MEDL規約腳本包含三個主要部分：導入事件和條件、復合事件和條件定義和反饋動作的定義，并以Eventspec開頭和END結尾。兩種規約的具體格式將在第5節最后的案例中體現。

4 嵌入式操作系統接口設計

為了獲取相應事件的信息，例如進程的創建與調度、中斷的產生等，需要對操作系統的實現進行一些擴充，以便把規約相關的事件的發生以及相關的信息通過監控接口輸送出來；為了對操作系統的運行進行反饋調整，還需要定義相應的反饋接口。

當前相關的工作主要包括兩個方面，即FreeRTOS的運行信息獲取和反饋控制接口。

(1)FreeRTOS的運行信息獲取。

目前本文使用的是FreeRTOS的Win32模擬器,在Windows7環境下運行，即由Windows7操作系統在PC環境下模擬FreeRTOS嵌入式操作系統的獨立運行。在此種運行模式下，內存的管理部分FreeRTOS交由Windows進行管理，因此本文目前考慮監控的時序性質規約暫不包括內存管理方面的性質。同時，監控軟件是運行在Windows平臺上的，因為在實際使用情況中，由于內置嵌入式操作系統的終端往往運算能力有限，進行驗證計算的監控程序也往往獨立運行在另外的終端上。如在航天領域中，常見的方式就是監控軟件運行在地面，而航天器上的系統把運行信息保存在存儲區中，再根據需要發送給地面系統。

在FreeRTOS中獲取的相關信息先輸出到一個日志文件中，再由監控程序讀取使用。該日志是一種事件日志，用于記錄相關原子事件的發生。為了在這些事件發生時把相應信息記錄到日志文件中，需要對FreeRTOS內核進行修改，當前完成的信息獲取的內容如下：獲取系統任務的狀態、獲取時間信息、任務狀態轉換、優先級的變化、創建與刪除任務。

獲取方法是在已有的內核函數執行關鍵動作時增加用于記錄信息到日志的代碼。以創建和刪除任務為例，創建任務由API函數xTaskCreate()負責，任務的刪除由API函數xTaskDelet()負責，當創建和刪除任務時會觸發Createtask(m)和Destroytask(m)事件。我們在API函數中進行修改，當創建和刪除任務的時候輸出任務名、優先級和事件發生的時間到事件日志。具體FreeRTOS的相關內核代碼請參考文獻[9]。

(2)反饋控制接口。

反饋接口用于在發現問題時，監控程序可以對操作系統的運行進行干涉，例如停止某些任務、改變任務優先級、禁止某些中斷等。在FreeRTOS中有一些API函數是用于改變相關對象狀態，由于在運行時不能直接訪問操作系統內核，所以需要設計一個可由監控程序調用的反饋接口，間接對操作系統的運行進行調整。當前反饋控制接口使用到FreeRTOS中API函數提供的調控能力能完成以下反饋控制：將調度器掛起、改變任務優先級、掛起任務、中斷任務、刪除任務。

具體使用到的API函數的相應信息需求請參考文獻[9]。為了對操作系統的反饋控制使用一個統一的接口，本文在FreeRTOS中定義一個接口Steer()。當運行的系統出現了違反規約的情況，監控程序根據預先設計好的反饋動作向Steer()接口傳輸指令，每種操作指令都對應好要調用的API函數，當接到指令時Steer()就能對相應任務調用相應的API函數。這樣的設計使得監控程序只用完成與Steer()接口的通信工作而不用自己直接調用API函數，而Steer()又可以執行不同的監控程序的反饋請求，加強了通用性。

5 監控器的構造與實現

運行時驗證的LTL公式的預測語義，也稱三值語義[10](簡稱LTL3)。與已經被用于運行時驗證工具的基于有窮軌跡上的兩值語義(true/false)監控器相比，基于三值語義的監控器非常適合于嵌入式系統運行時驗證。一方面，三值語義的公平性使得監控器的裁決始終是正確的，另一方面，三值語義的預測性使得監控器有發現一條無窮運行軌跡的最小好(壞)前綴[11]的能力，即監控器能盡可能早地作出裁決，因此在一定意義上具有預測性。所以，本文的監控器構造也將使用三值語義。三值語義監控器的理論構造過程請參照文獻[12]。

基于三值語義的監控程序的構造過程如圖4所示。

Figure 4 Generation process for monitoring program圖4 監控程序生成流程圖

在基于LTL三值語義的監控器構造的實現中，使用了一個開源工具LTL3Tools用于生成監控器的有限狀態機FSM(Finite-StateMachine)。LTL3Tools輸出相應的FSM的.txt格式文本文件，如圖5所示，可以看作是一個監控器模型，輸入有窮字u，它會判斷出是否公式成立。通過將.txt文件中的FSM進行簡化，去除冗余的邊，并生成下一步JavaMOP所需的.mop文件，運行JavaMOP得到相應的.aj文件，當前正在編寫相關的簡化轉換工具FSM2Mop，用于自動將FSM生成下一步JavaMOP所需的.mop文件，避免人工帶來的誤操作。得到的代碼已經是一個較為完整的監控器實現框架，但目前還不能完全自動執行，仍需要一些人工改造以加入相應的信息獲取代碼和調整代碼，才能得到相應的監控程序，人工參與和調整代碼可能會帶來誤操作，而造成監控程序的不準確，本文下一步將考慮如何把該過程完全自動化。同時，本文還實現了對日志進行讀取的相應接口函數，用于讀取日志內的數據。

Figure 5 Instance for monitor automata圖5 生成的監控器自動機模型的圖形和文字表示示例

這里例舉一個具體的案例：系統中一個任務a開始運行時，當前系統中還有另外的任務b處于等待運行的狀態，任務a開始運行到完成期間，任務b都不能運行。那么，在任務a的執行期間,任務a不能被中斷，且任務b的優先級不能高于任務a，發現違反規約的情況后就反饋控制掛起任務b，直到任務a完成運行。

該案例首先可以用LTL公式G(SM→KO)表示，其中復合條件SM(Start Misssion)表示任務開始運行，復合條件KO(Keep Operating)表示保持運行狀態，公式中G表示always。針對LTL公式G(SM→KO)，首先定義復合條件SM=Start_a，其中Start_a=Start task(a)是原子事件，表示輸出字符的任務a開始運行,再定義復合條件KO=(!(Block_a)&&Priority)∪End_a，其中Block_a=Start block(a)為原子事件，表示任務a中斷，Priority是一個原子條件,表示任務b的優先級不能高于任務a，End_a為一個原子事件,表示任務a結束運行。案例生成的PEDL與MEDL規約如圖6所示。根據LTL公式，由上文所述過程即可得到相應的監控程序，結合添加了相應接口的FreeRTOS嵌入式操作系統以及接口程序，在該案例中監控程序能夠及時、準確地發現系統運行時性質規約違背的情況，并給出警報，進行反饋控制。

Figure 6 PEDL and MEDL statute of usecase圖6 案例的PEDL和MEDL規約

6 結束語

本文在傳統的運行時驗證技術的基礎上，結合FreeRTOS嵌入式操作系統提出了一種針對嵌入式操作系統而不是應用程序的運行時驗證框架，并對相關的具體工作進行了初步實現。

當前對嵌入式操作系統的運行時驗證框架的實現還處于初步階段，今后工作的重點主要在：構造監控的對象更加全面，反饋的動作更多，并能夠像Java-MaC工具一樣自動生成相應的監控程序的工具集；結合其他工作讓FreeRTOS構成一個功能更全面、能夠滿足實際應用的帶運行時驗證技術的嵌入式系統，使其有更廣泛的用途。另外，當前運行時驗證技術最大的瓶頸就是驗證計算本身對系統的損耗，對于嵌入式操作系統這種實時性要求很高的系統更是一個關鍵問題。下一步，作者還將研究使用運行時驗證對系統的影響有多大，影響的因素是什么，通過什么樣的技術手段使得這種影響降低到最小的程度。

[1]ColinS,MarianiL.Run-timeverification,chapter18 [J].ProcofLNCS,2005, 3472:525-555.

[2]PeleskaJ.Testautomationforsafety-criticalsystems:Industrialapplicationandfuturedevelopments[C]∥Procofthe3rdInternationalSymposiumofFormalMethods,1996,1051:39-59.

[3]ClarkeEM,GrumbergO,PeledDA.Modelchecking[M].London:TheMITPress,1999.

[4]LiuBin,WangQi,LiuLi-li.PrincipleandimplementationofembeddedoperatingsystemFreeRTOS[J].MocrocontrollerandEmbeddedSystem,2005(7):1-2.(inChinese)

[5]KrogerF.Thetemporallogicofprograms[M].NewYork:Springer-Verlag,1987.

[6]SammapunU,LeeI,SokolskyO.RT-MaC:Runtimemonitoringandcheckingofquantitativeandprobabilisticproperties[C]∥Procofthe11thIEEEInternationalConferenceofEmbeddedandReal-TimeComputingSystemsandApplications,2005:147-153.

[7]KimM,KannanS,LeeI,etal.Java-MaC:AruntimeassuranceapproachforJavaprograms[J].FormalMethodsinSystemsDesign, 2004,24(2):129-155.

[8]MaCResearchteamofUniveristyofPennsylvania.LanguagesintheMaCprototypeimplementation[EB/OL].[2008-01-01].http://rtg.cis.upenn.edu/mac/index.php3.

[9]BarryR.FreeRTOSusermanual[EB/OL].[2004-12-09].http://www.FreeRTOS.net.

[10]GeilenMCW.Ontheconstructionofmonitorsfortemporallogicproperties[J].ElectronicNotesinTheoreticalComputerScience,2001,55(2):181-199.

[11]BauerA,LeucherM,SchallhartC.RuntimeverificationforLTLandPTLTL[J].JournalofACMTransactionsonSotwareEngineerandMethodology, 2011,20(4):ArticleNo.14.

[12]SuiPing.Softwareruntimeverificationmethodbasedonthree-valuedsemantics[D].Changsha:NationalUniversityofDefenseTechnology,2010.(inChinese)

附中文參考文獻:

[4] 劉濱,王琦,劉麗麗.嵌入式操作系統FreeRTOS的原理與實現[J].單片機與嵌入式系統應用,2005(7):1-2.

[12] 隋平.基于三值語義的軟件運行時驗證方法.[D].長沙：國防科學技術大學,2010.

ZHANGKe-di,born in 1988,MS candidate,his research interest includes software engineering.

Aruntimeverificationmethodforembeddedoperatingsystem

ZHANG Ke-di,SHU Shao-xian,DONG Wei

(College of Computer,National University of Defense Technology,Changsha 410073,China)

As an effective supplement of testing and model checking, runtime verification technique attracts more and more attentions. However, the current runtime verification technology is mainly used for application software. Very few are specialized for monitoring the running state of an operating system. The paper studies the runtime verification framework and key techniques for embedded operating system and realizes a demo combined with an open source system FreeRTOS. Firstly, an embedded operating system oriented framework for runtime verification and feedback adjustment is proposed. Secondly, based on the critical part of our frame, the specification language, three-valued semantic monitor generation and FreeRTOS related interfaces are designed and implemented.

embedded operating system;FreeRTOS;runtime verification;specification language;three-valued semantic monitor

1007-130X(2014)05-0900-06

2012-11-09;

：2013-04-17

國家自然科學基金資助項目(60970035)；國家863計劃資助項目(2011AA010106)

TP311.5

：A

10.3969/j.issn.1007-130X.2014.05.020

張可迪(1988-),男,黑龍江哈爾濱人，碩士生，研究方向為軟件工程。E-mail:Zkd008@21cn.com

通信地址：410073 湖南省長沙市國防科學技術大學計算機學院

Address:College of Computer,National University of Defense Technology,Changsha 410073,Hunan,P.R.China