一種嵌入式操作系統(tǒng)運(yùn)行時(shí)驗(yàn)證方法*

張可迪,舒紹嫻,董 威

(國(guó)防科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院，湖南 長(zhǎng)沙 410073)

一種嵌入式操作系統(tǒng)運(yùn)行時(shí)驗(yàn)證方法*

張可迪,舒紹嫻,董 威

(國(guó)防科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院，湖南 長(zhǎng)沙 410073)

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

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

1 引言

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

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

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

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

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

2 整體架構(gòu)

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

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

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

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

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

針對(duì)上面四個(gè)子問題，解決方案分別如下：

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

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

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

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

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

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

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

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

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

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

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

3 規(guī)約語言

3.1 事件與條件定義語言

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

(1)語法。

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

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

(2)語義。

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

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

3.2 事件定義語言

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

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

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

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

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

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

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

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

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

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

(2)反饋控制接口。

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

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

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

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

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

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

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

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

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

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

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

6 結(jié)束語

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

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

附中文參考文獻(xiàn):

[4] 劉濱,王琦,劉麗麗.嵌入式操作系統(tǒng)FreeRTOS的原理與實(shí)現(xiàn)[J].單片機(jī)與嵌入式系統(tǒng)應(yīng)用,2005(7):1-2.

[12] 隋平.基于三值語義的軟件運(yùn)行時(shí)驗(yàn)證方法.[D].長(zhǎng)沙：國(guó)防科學(xué)技術(shù)大學(xué),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

國(guó)家自然科學(xué)基金資助項(xiàng)目(60970035)；國(guó)家863計(jì)劃資助項(xiàng)目(2011AA010106)

TP311.5

：A

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

張可迪(1988-),男,黑龍江哈爾濱人，碩士生，研究方向?yàn)檐浖こ?。E-mail:Zkd008@21cn.com

通信地址：410073 湖南省長(zhǎng)沙市國(guó)防科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院

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