基于模型檢查的嵌入式軟件構(gòu)件化分析與驗(yàn)證

聶捷楠

摘 要： 對嵌入式軟件構(gòu)件化進(jìn)行準(zhǔn)確分析與驗(yàn)證，能夠?yàn)榍度胧较到y(tǒng)安全、穩(wěn)定的運(yùn)行提供保障。提出一種基于模型檢查的嵌入式軟件構(gòu)件化分析與驗(yàn)證方法。設(shè)計(jì)一種用于檢查軟件構(gòu)件的模型，為嵌入式軟件構(gòu)件化分析與驗(yàn)證提供理論基礎(chǔ)；將嵌入式軟件系統(tǒng)模型用SMV語言的形式表達(dá)，利用SMV模型檢查工具實(shí)現(xiàn)對嵌入式軟件運(yùn)行狀態(tài)的分析與檢驗(yàn)。實(shí)驗(yàn)結(jié)果表明，該模型能夠?qū)η度胧杰浖?gòu)件化的非功能性方面的設(shè)計(jì)要求進(jìn)行準(zhǔn)確分析與驗(yàn)證，為嵌入式系統(tǒng)安全穩(wěn)定的運(yùn)行提供了保障。

關(guān)鍵詞： 模型檢查； 嵌入式軟件； 構(gòu)件化； SMV

中圖分類號： TN911?34； TP391 文獻(xiàn)標(biāo)識碼： A 文章編號： 1004?373X（2016）24?0063?03

Embedded software component analysis and verification based on model checking

NIE Jienan

（Institute of Humanity Information Management， Chengdu Medical College， Chengdu 610500， China）

Abstract： The embedded software component is analyzed and validated accurately， which may provide the safe and stable operation for the embedded system. A analysis and validation method of the embedded software component based on model checking is put forward. A kind of model used to examine the software component is designed， which provides a theoretical foundation for analysis and verification of the embedded software component. The embedded software system model is expressed in the form of SMV language. The SMV model checking tool is used to implement analysis and test of the embedded software running status. The experimental results show that the model can accurately analyze and validate the non?functional design requirements of the embedded software component， and provided the safeguard for the embedded system safe and stable operation.

Keywords： model checking； embedded software； component； SMV

嵌入式系統(tǒng)各種功能的實(shí)現(xiàn)都離不開軟件[1]，軟件具有極其重要的意義[2]，它是影響嵌入式系統(tǒng)穩(wěn)定運(yùn)行的關(guān)鍵因素，一旦關(guān)鍵部位中嵌入式系統(tǒng)的軟件失效[3]，輕則造成財(cái)產(chǎn)損失，重則使生命受到威脅[4]。與PC機(jī)中的軟件相比，嵌入式系統(tǒng)中的軟件既要滿足其功能性設(shè)計(jì)要求[5]，又要滿足其非功能性的設(shè)計(jì)要求，如軟件的驅(qū)動(dòng)程度、運(yùn)算資源的占用程度、對能量的消耗程度等[6]。因此如何對嵌入式系統(tǒng)中的非功能性設(shè)計(jì)要求進(jìn)行分析與驗(yàn)證，已經(jīng)成為當(dāng)前IT領(lǐng)域中的一個(gè)熱點(diǎn)研究課題，受到專家學(xué)者的廣泛關(guān)注[7]。

目前，主要的嵌入式系統(tǒng)軟件驗(yàn)證方法包括基于馬爾科夫的驗(yàn)證方法[8]、基于定理證明的驗(yàn)證方法和基于調(diào)試代理軟件的驗(yàn)證方法[9]。最常用的是基于馬爾科夫的嵌入式軟件驗(yàn)證方法。但利用傳統(tǒng)方法進(jìn)行嵌入式系統(tǒng)軟件的驗(yàn)證，驗(yàn)證的項(xiàng)目主要為軟件的功能性設(shè)計(jì)要求，并且只能在軟件設(shè)計(jì)的后期才能進(jìn)行驗(yàn)證，難以對非功能性的設(shè)計(jì)要求進(jìn)行準(zhǔn)確分析與驗(yàn)證，導(dǎo)致嵌入式軟件的穩(wěn)定性與安全性難以得到保障[10]。

針對傳統(tǒng)方法存在的缺陷，提出一種基于模型檢查的嵌入式軟件構(gòu)件化分析與驗(yàn)證方法。利用SMV檢查工具對嵌入式軟件運(yùn)行狀態(tài)進(jìn)行分析與檢驗(yàn)，實(shí)現(xiàn)對嵌入式軟件的分析與驗(yàn)證。仿真實(shí)驗(yàn)證明了改進(jìn)算法在嵌入式軟件構(gòu)件化分析與驗(yàn)證方面的優(yōu)勢。

1 嵌入式軟件構(gòu)件化驗(yàn)證模型設(shè)計(jì)

對嵌入式系統(tǒng)中的軟件進(jìn)行構(gòu)件化驗(yàn)證，主要通過重復(fù)使用模塊化軟件來建立嵌入式軟件構(gòu)件化驗(yàn)證的模型，實(shí)現(xiàn)對嵌入式系統(tǒng)軟件的驗(yàn)證。

通常情況下，一個(gè)完整的嵌入式系統(tǒng)軟件包括多個(gè)子系統(tǒng)軟件，其軟件系統(tǒng)具有較高的構(gòu)件化特征。對嵌入式系統(tǒng)中構(gòu)件化軟件進(jìn)行分析與驗(yàn)證，能夠?yàn)榍度胧较到y(tǒng)安全穩(wěn)定的運(yùn)行提供保障。由于分析與驗(yàn)證過程需要消耗大量能量，能量成為嵌入式系統(tǒng)中一種特殊的資源消耗，嵌入式系統(tǒng)的運(yùn)行時(shí)間與能量消耗呈正相關(guān)，運(yùn)行時(shí)間越長，能量消耗越多。因此，可以利用能量消耗的時(shí)間特性對嵌入式軟件構(gòu)件化的驗(yàn)證過程建模。

設(shè)計(jì)一種驗(yàn)證模型，在驗(yàn)證模型中加入嵌入式系統(tǒng)主要可以利用資源（包括存儲空間、緩沖區(qū)、消息隊(duì)列、傳感器）特征向量，使該模型能夠反映嵌入式軟件構(gòu)件運(yùn)行時(shí)主要可以利用資源的變化情況。設(shè)計(jì)驗(yàn)證模型時(shí)需要包含如下參數(shù)：假設(shè)[VP]是資源利用狀態(tài)的集合，對于每一嵌入式資源利用狀態(tài)都有[vi∈VP]，且[P]的初始狀態(tài)為[vi∈VInitP]；[FP]為資源狀態(tài)的映射集合，[FP=（f1P，f2P，…，fKP）]，其中[K]為嵌入式系統(tǒng)中可利用資源種類的數(shù)目；[WP]表示可利用資源的有窮集合，[WP=（VP，F(xiàn)P（VP））]；[ΓP]為資源利用狀態(tài)的轉(zhuǎn)換集。通過以上參數(shù)的描述，將嵌入式軟件構(gòu)件化驗(yàn)證的模型轉(zhuǎn)化為多元組的形式進(jìn)行構(gòu)建：

[P=VP?FP?WP?ΓP]

2 嵌入式軟件構(gòu)件化驗(yàn)證方法設(shè)計(jì)與實(shí)現(xiàn)

本文構(gòu)建立了嵌入式軟件構(gòu)件化驗(yàn)證的模型，將嵌入式軟件構(gòu)件化驗(yàn)證模型中軟件運(yùn)行路徑逐一遍歷，直到獲取正確的軟件運(yùn)行路徑，實(shí)現(xiàn)模型檢查算法設(shè)計(jì)，最終實(shí)現(xiàn)基于模型檢查的嵌入式軟件構(gòu)件化分析與驗(yàn)證。

2.1 基于時(shí)序邏輯CTL算子的模型檢查算法

首先獲得嵌入式軟件運(yùn)行過程中的時(shí)序邏輯CTL算子，通過CTL算子獲取嵌入式軟件構(gòu)件化驗(yàn)證模型中軟件運(yùn)行路徑的有關(guān)性質(zhì)，并逐一遍歷，直到搜索出正確的軟件運(yùn)行路徑，設(shè)計(jì)了模型檢查算法。具體過程如下所述：將時(shí)序邏輯CTL劃分為分支時(shí)間算子和線性時(shí)間算子。其中，分支時(shí)間算子包括軟件的全部運(yùn)行路徑A和特定的運(yùn)行路徑E，線性時(shí)間算子包括G（always，經(jīng)常）、F（sometimes，偶爾）、X（next time，下一時(shí)刻）和U（until，直到）。引入上述構(gòu)建的嵌入式軟件構(gòu)件化驗(yàn)證模型，利用時(shí)序邏輯CTL中的分支時(shí)間算子和線性時(shí)間算子描述嵌入式軟件構(gòu)件化驗(yàn)證模型中軟件運(yùn)行路徑的相關(guān)性質(zhì)，如圖1所示。圖1（a）為[EFg]，表示“資源利用狀態(tài)的集合[VP]中存在一條運(yùn)行路徑使布爾量公式[g]在某種運(yùn)行狀態(tài)下為真”；圖1（b）為[AFg]，表示“資源狀態(tài)的映射集合[FP]中所有運(yùn)行路徑中布爾量公式[g]在某種運(yùn)行狀態(tài)下為真”；圖1（c）為[EGg]，表示“可利用資源的有窮集合[WP]中存在一條運(yùn)算路徑使得布爾量公式[g]在該路徑中的全部狀態(tài)下都為真”；圖1（d）為[AGg]，表示“資源利用狀態(tài)的轉(zhuǎn)換集[ΓP]中布爾量公式[g]在全部運(yùn)行路徑中的全部狀態(tài)下都為真”，通過對這些條件進(jìn)行逐一判定，最終選擇正確的軟件運(yùn)行路徑，完成模型檢查算法設(shè)計(jì)。

2.2 基于模型檢查的嵌入式軟件驗(yàn)證的實(shí)現(xiàn)

針對嵌入式軟件進(jìn)行分析與驗(yàn)證的模型檢查工具主要包括：貝爾實(shí)驗(yàn)室開發(fā)的SPIN工具、赫爾辛基工業(yè)大學(xué)開發(fā)的PROD工具、CMU大學(xué)開發(fā)的SMV工具等。每種模型檢查工具都有不同的特點(diǎn)，其中，SMV工具結(jié)構(gòu)簡單、運(yùn)算量小、準(zhǔn)確率高。因此本文將SMV工具作為嵌入式軟件分析與驗(yàn)證的模型檢查工具。

SMV工具是根據(jù)“符號模型檢查”的原理開發(fā)，目的是通過對符號模型對軟件的性能進(jìn)行檢查，隨著SMV工具功能的不斷完善，SMV工具已經(jīng)被廣泛應(yīng)用于軟件有限狀態(tài)的檢查。本節(jié)將上述模型檢查算法利用SMV語言的形式表達(dá)，構(gòu)建SMV模型檢查工具，完成嵌入式軟件構(gòu)件化分析與驗(yàn)證，具體步驟如下所述：

一個(gè)完整的SMV模型檢查工具由兩個(gè)部分構(gòu)成，分別為：一個(gè)狀態(tài)轉(zhuǎn)換系統(tǒng)；一個(gè)CTL公式組，能夠準(zhǔn)確描述嵌入式軟件的屬性。通過這兩個(gè)部分可以將嵌入式軟件的構(gòu)件化驗(yàn)證過程描述為一個(gè)二叉樹BDD的形式。SMV模型檢查工具只需要對嵌入式軟件二叉樹BDD的運(yùn)行狀態(tài)進(jìn)行搜索，將搜索結(jié)果進(jìn)行逐一判定，判定后輸出的結(jié)果分為：正確和錯(cuò)誤，即為模型檢查算法對嵌入式軟件構(gòu)件化的驗(yàn)證結(jié)果，實(shí)現(xiàn)了嵌入式軟件的構(gòu)件化驗(yàn)證。

2.3 部分代碼設(shè)計(jì)

利用SMV模型檢查工具對嵌入式系統(tǒng)的構(gòu)件化進(jìn)行驗(yàn)證與分析，部分程序如下所述：

MODULE main

VAR

Pen_irq；booleam；

D_jitery_delay；boolean；

U_jittery_delay；boolean；

Detect：touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）；

SPEC

AG（detect，state=Touch_up&pen_irq=0?>AF detect，state=Touch_Down）

SPEC

AG（detect，state=Touch_Down&pen_irq?>AF detect，state=Touch_up）

MODULE Touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）

state：{ Touch_Idle，Touch_up，Touch_down，Touch_ChkUp；Touch_chkDown；}

3 實(shí)驗(yàn)結(jié)果及分析

3.1 實(shí)驗(yàn)環(huán)境設(shè)置

為了驗(yàn)證改進(jìn)算法在嵌入式軟件構(gòu)件化驗(yàn)證方面的有效性，需要進(jìn)行仿真實(shí)驗(yàn)。嵌入式軟件構(gòu)件化分析與驗(yàn)證的運(yùn)行環(huán)境為：Windows 7操作系統(tǒng)，利用Rational Rose 2003生成 MDL文件；以嵌入式軟件的非功能性設(shè)計(jì)要求為依據(jù)，對改進(jìn)算法和傳統(tǒng)算法的性能進(jìn)行比較。研究表明，資源的占用程度、投影路徑中非法信息檢驗(yàn)、能耗行為的路徑是嵌入式軟件構(gòu)件化的具體屬性，本文以手持PDA為例，以這三個(gè)屬性為目標(biāo)，對手持PDA軟件進(jìn)行構(gòu)件化驗(yàn)證。

3.2 不同算法下仿真實(shí)驗(yàn)結(jié)果及分析

首先利用上述獲得的SMV模型檢查工具對PDA的通信的驅(qū)動(dòng)程序和信息交互序列的驅(qū)動(dòng)程序運(yùn)行資源的占用情況進(jìn)行檢驗(yàn)。這兩種驅(qū)動(dòng)程序包含三類資源，分別為r1，r2和r3，軟件在進(jìn)行狀態(tài)轉(zhuǎn)換過程中需要占用的資源數(shù)量和資源種類利用向量進(jìn)行描述，例如，

3.2.1 不同算法下嵌入式軟件運(yùn)行資源的占用情況驗(yàn)證

首先利用不同算法對手持PDA軟件進(jìn)行資源的占用情況方面驗(yàn)證，以驗(yàn)證軟件在狀態(tài)轉(zhuǎn)換的過程中需要占用的資源是否滿足設(shè)計(jì)要求。利用傳統(tǒng)算法進(jìn)行驗(yàn)證結(jié)果表明：傳統(tǒng)算法只能檢測出軟件在狀態(tài)轉(zhuǎn)換的過程中需要占用的資源種類為3種，但不能檢測出具體的資源名稱和占用資源的數(shù)量；而利用改進(jìn)算法進(jìn)行驗(yàn)證結(jié)果表明：手持PDA通信的驅(qū)動(dòng)程序在進(jìn)行轉(zhuǎn)換的過程中有一個(gè)資源處于非法狀態(tài)，即（s4|s1），該程序在進(jìn)行狀態(tài)轉(zhuǎn)換的過程中需要的資源為[r1，2]，[r2，5]，[r3，3]。（s4|s1）狀態(tài)在轉(zhuǎn)換的過程中對資源r2的需求量為5，而在實(shí)際程序中r2的資源總的數(shù)量為4，因此可推出該狀態(tài)在轉(zhuǎn)換的過程中有1個(gè)資源不符合設(shè)計(jì)要求，體現(xiàn)了改進(jìn)算法的巨大優(yōu)勢。

3.2.2 不同算法下嵌入式軟件運(yùn)行中投影路徑中非法

信息檢驗(yàn)驗(yàn)證

為了進(jìn)一步驗(yàn)證改進(jìn)算法的有效性，本文以PDA中信息交互序列的驅(qū)動(dòng)程序?yàn)槔?，對信息交互過程中投影路徑中的非法信息進(jìn)行檢驗(yàn)。結(jié)果表明，利用傳統(tǒng)算法進(jìn)行投影路徑中非法信息檢驗(yàn)，沒有搜索出對應(yīng)的投影路徑中存在的非法信息；而改進(jìn)算法結(jié)果表明：PDA在進(jìn)行信息交互的過程中，在組合狀態(tài)空間內(nèi)存在一個(gè)與信息交互行為相對應(yīng)的投影路徑，但是該路徑存在一個(gè)非法狀態(tài)（s2|s1），占用資源[r2，r3]，表明在此信息交互行為的狀態(tài)下，嵌入式軟件系統(tǒng)不滿足設(shè)定的資源限制條件，需要PDA軟件的編寫者對軟件進(jìn)行及時(shí)修改，以保證嵌入式軟件的安全性。嵌入式軟件的非法信息驗(yàn)證界面如圖2所示。

3.2.3 不同算法下嵌入式軟件運(yùn)行中能耗行為的路徑

比對驗(yàn)證

在PDA中，為了對比不同算法在嵌入式軟件能耗行為的路徑方面的驗(yàn)證性能。利用不同算法對PDA非功能性的能耗行為的路徑進(jìn)行檢驗(yàn)。首先搜索出滿足非功能性行為的路徑共19條。然后利用不同算法對這19條路徑消耗的能耗進(jìn)行對比。

實(shí)驗(yàn)結(jié)果為：實(shí)際情況下所有有路徑中最大能量為44.6，對應(yīng)的投影路徑為s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8，改進(jìn)算法下所有路徑中最大能量為46.3，對應(yīng)的投影路徑為s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8；傳統(tǒng)算法下最大能量為29.7，對應(yīng)的投影路徑為s0|s0（0，0）2.8→s1|s1（0，0）5.5→s2|s1（0，1）4.0→s3|s1（0，3）5.3→s4|s1（0，5）5.3→s5|s1（0，9）4.7。通過仿真實(shí)驗(yàn)表明，傳統(tǒng)算法與實(shí)際的能耗值相差較大，并且對應(yīng)的投影路徑不一致；而改進(jìn)算法與實(shí)際的能耗最為接近，并且對應(yīng)的投影路徑一致，充分體現(xiàn)了改進(jìn)算法在嵌入式軟件能耗行為的路徑設(shè)計(jì)驗(yàn)證方面的優(yōu)越性。

4 結(jié) 語

針對傳統(tǒng)算法存在的缺陷，提出一種基于模型檢查的嵌入式軟件構(gòu)件化分析與驗(yàn)證方法。利用SMV檢查工具對嵌入式軟件運(yùn)行狀態(tài)進(jìn)行分析與檢驗(yàn)，實(shí)現(xiàn)對嵌入式軟件的分析與驗(yàn)證。仿真表明，改進(jìn)算法能夠?qū)η度胧杰浖?gòu)件化的非功能性方面的設(shè)計(jì)要求進(jìn)行準(zhǔn)確分析與驗(yàn)證，為嵌入式系統(tǒng)安全穩(wěn)定的運(yùn)行提供了保障。

參考文獻(xiàn)

[1] 王鋒，張弛.構(gòu)件化嵌入式軟件設(shè)計(jì)模型驗(yàn)證工具的研究[J].通訊世界，2014（21）：36.

[2] 王博，白曉穎，賀飛.可組合嵌入式軟件建模與驗(yàn)證技術(shù)研究綜述[J].軟件學(xué)報(bào)，2014，25（2）：234?253.

[3] 符寧，杜承烈，李建良，等.AADL分級調(diào)度模型的分析與驗(yàn)證[J].計(jì)算機(jī)研究與發(fā)展，2015，52（1）：167?176.

[4] 胡寧，葉宏.嵌入式操作系統(tǒng)的形式化驗(yàn)證方法[J].航空計(jì)算技術(shù)，2015（2）：96?100.

[5] 白海洋，李靜，趙娜.基于時(shí)間自動(dòng)機(jī)的嵌入式軟件模型可調(diào)度性驗(yàn)證[J].計(jì)算機(jī)工程與科學(xué)，2013，35（3）：121?127.

[6] 趙競雄.嵌入式系統(tǒng)威脅與風(fēng)險(xiǎn)評估過程仿真分析[J].計(jì)算機(jī)仿真，2014，31（4）：295?298.

[7] 黃傳林，黃志球，胡軍，等.基于擴(kuò)展SysML活動(dòng)圖的嵌入式系統(tǒng)設(shè)計(jì)安全性驗(yàn)證方法研究[J].小型微型計(jì)算機(jī)系統(tǒng)，2015（3）：408?417.

[8] 謝開斌，陳海明，崔莉.物聯(lián)網(wǎng)軟件體系結(jié)構(gòu)中的感執(zhí)模型的求精[J].軟件學(xué)報(bào)，2014，25（8）：1659?1670.

[9] 王誠.硬件構(gòu)件化的嵌入式底層構(gòu)件開發(fā)技術(shù)分析[J].中國科技博覽，2013（9）：134.

[10] 黃菲.嵌入式實(shí)時(shí)軟件的構(gòu)件化開發(fā)技術(shù)探究[J].信息技術(shù)與信息化，2015（10）：197?198.