張可迪,舒紹嫻,董 威

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

一種嵌入式操作系統(tǒng)運行時驗證方法*

張可迪,舒紹嫻,董 威

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

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

嵌入式操作系統(tǒng);FreeRTOS;運行時驗證;規(guī)約語言;三值語義監(jiān)控器

1 引言

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

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

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

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

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

2 整體架構(gòu)

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

(1)如何定義嵌入式操作系統(tǒng)應該滿足的性質(zhì)規(guī)約和相關(guān)的關(guān)鍵屬性，如何建立關(guān)鍵屬性與性質(zhì)規(guī)約之間的聯(lián)系；

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

(3)如何在目標系統(tǒng)和監(jiān)控器之間傳遞信息；

(4)如何從性質(zhì)規(guī)約生成監(jiān)控器模型，并實現(xiàn)能在違反規(guī)約時執(zhí)行反饋動作的監(jiān)控程序。

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

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

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

①操作系統(tǒng)的功能和結(jié)構(gòu)相對確定，而不同的應用程序其功能和設(shè)計結(jié)構(gòu)區(qū)別很大。

②操作系統(tǒng)的內(nèi)核在運行時訪問受限，而應用程序則沒有這種限制。

③操作系統(tǒng)要監(jiān)控的內(nèi)容和性質(zhì)相對比較確定，而應用程序則因不同的需求而異。

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

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

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

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

根據(jù)圖1中嵌入式操作系統(tǒng)運行時驗證的框架，本文將從規(guī)約語言的設(shè)計、操作系統(tǒng)的擴展、監(jiān)控器的構(gòu)造與實現(xiàn)三個方面進行具體工作的闡述。

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

3 規(guī)約語言

3.1 事件與條件定義語言

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

(1)語法。

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

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

(2)語義。

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

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

3.2 事件定義語言

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

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

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

4 嵌入式操作系統(tǒng)接口設(shè)計

為了獲取相應事件的信息，例如進程的創(chuàng)建與調(diào)度、中斷的產(chǎn)生等，需要對操作系統(tǒng)的實現(xiàn)進行一些擴充，以便把規(guī)約相關(guān)的事件的發(fā)生以及相關(guān)的信息通過監(jiān)控接口輸送出來；為了對操作系統(tǒng)的運行進行反饋調(diào)整，還需要定義相應的反饋接口。

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

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

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

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

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

(2)反饋控制接口。

反饋接口用于在發(fā)現(xiàn)問題時，監(jiān)控程序可以對操作系統(tǒng)的運行進行干涉，例如停止某些任務、改變?nèi)蝿諆?yōu)先級、禁止某些中斷等。在FreeRTOS中有一些API函數(shù)是用于改變相關(guān)對象狀態(tài)，由于在運行時不能直接訪問操作系統(tǒng)內(nèi)核，所以需要設(shè)計一個可由監(jiān)控程序調(diào)用的反饋接口，間接對操作系統(tǒng)的運行進行調(diào)整。當前反饋控制接口使用到FreeRTOS中API函數(shù)提供的調(diào)控能力能完成以下反饋控制：將調(diào)度器掛起、改變?nèi)蝿諆?yōu)先級、掛起任務、中斷任務、刪除任務。

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

5 監(jiān)控器的構(gòu)造與實現(xiàn)

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

基于三值語義的監(jiān)控程序的構(gòu)造過程如圖4所示。

Figure 4 Generation process for monitoring program圖4 監(jiān)控程序生成流程圖

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

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

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

該案例首先可以用LTL公式G(SM→KO)表示，其中復合條件SM(Start Misssion)表示任務開始運行，復合條件KO(Keep Operating)表示保持運行狀態(tài)，公式中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的優(yōu)先級不能高于任務a，End_a為一個原子事件,表示任務a結(jié)束運行。案例生成的PEDL與MEDL規(guī)約如圖6所示。根據(jù)LTL公式，由上文所述過程即可得到相應的監(jiān)控程序，結(jié)合添加了相應接口的FreeRTOS嵌入式操作系統(tǒng)以及接口程序，在該案例中監(jiān)控程序能夠及時、準確地發(fā)現(xiàn)系統(tǒng)運行時性質(zhì)規(guī)約違背的情況，并給出警報，進行反饋控制。

Figure 6 PEDL and MEDL statute of usecase圖6 案例的PEDL和MEDL規(guī)約

6 結(jié)束語

本文在傳統(tǒng)的運行時驗證技術(shù)的基礎(chǔ)上，結(jié)合FreeRTOS嵌入式操作系統(tǒng)提出了一種針對嵌入式操作系統(tǒng)而不是應用程序的運行時驗證框架，并對相關(guān)的具體工作進行了初步實現(xiàn)。

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

[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] 劉濱,王琦,劉麗麗.嵌入式操作系統(tǒng)FreeRTOS的原理與實現(xiàn)[J].單片機與嵌入式系統(tǒng)應用,2005(7):1-2.

[12] 隋平.基于三值語義的軟件運行時驗證方法.[D].長沙：國防科學技術(shù)大學,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 湖南省長沙市國防科學技術(shù)大學計算機學院

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