楊　榮

(湖北科技學(xué)院　計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖北　咸寧　437100)

基于形式化模型的嵌入式服務(wù)模塊規(guī)約

楊榮

(湖北科技學(xué)院計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖北咸寧437100)

摘要：如今，嵌入式系統(tǒng)發(fā)展迅速，伴隨的嵌入式服務(wù)軟件地位越來(lái)越重要，其服務(wù)軟件的可靠性尤其被重點(diǎn)關(guān)注。本文研究嵌入式外層服務(wù)軟件模塊之間的可靠通信方式，如何以較低代價(jià)換取嵌入式系統(tǒng)的高可靠性和穩(wěn)定性。對(duì)嵌入式服務(wù)軟件可靠行為進(jìn)行建模，重點(diǎn)對(duì)信息的發(fā)送模式和信息接收模式進(jìn)行建模。

關(guān)鍵詞：嵌入式系統(tǒng)；服務(wù)軟件；可靠性；建模

目前,嵌入式系統(tǒng)面臨著新的發(fā)展階段，設(shè)計(jì)者面臨著新的挑戰(zhàn)，傳統(tǒng)的嵌入式系統(tǒng)設(shè)計(jì)方法已無(wú)法適應(yīng)新的設(shè)計(jì)需求和約束。現(xiàn)在，嵌入式系統(tǒng)設(shè)計(jì)者采用一種基于ADL(Architecture Description Language)的新的系統(tǒng)級(jí)設(shè)計(jì)規(guī)約方法。設(shè)計(jì)者在最上面用抽象的體系結(jié)構(gòu)描述語(yǔ)言對(duì)系統(tǒng)進(jìn)行規(guī)約，并通過(guò)實(shí)驗(yàn)進(jìn)行性能評(píng)估，并且經(jīng)過(guò)一個(gè)“規(guī)約——驗(yàn)證——再規(guī)約”的反復(fù)過(guò)程，直到設(shè)計(jì)達(dá)到功能要求。這樣，設(shè)計(jì)者就可以在早期發(fā)現(xiàn)問(wèn)題，并及時(shí)修改，改變了過(guò)去在后期才發(fā)現(xiàn)問(wèn)題的缺陷，大大減少了整個(gè)設(shè)計(jì)的工作量。

另外，自從嵌入式系統(tǒng)誕生以來(lái)，隨著應(yīng)用需求的變化，軟件在嵌入式系統(tǒng)中的地位越來(lái)越重要。比如交換機(jī)和路由器，即使硬件一模一樣，如果軟件不一樣，則產(chǎn)品也是不同的。然而，嵌入式系統(tǒng)應(yīng)用領(lǐng)域豐富多變，不同應(yīng)用對(duì)軟件系統(tǒng)的要求和側(cè)重點(diǎn)都不同。但一般都要求嵌入式系統(tǒng)功能強(qiáng)大、性能穩(wěn)定、工作可靠，這三點(diǎn)需求有時(shí)候會(huì)相互沖突。一個(gè)嵌入式系統(tǒng)要具備功能豐富、性能穩(wěn)定可靠，不僅需要設(shè)計(jì)精良的硬件來(lái)支撐，而且必須有高質(zhì)量的軟件實(shí)現(xiàn)。本文主要研究嵌入式系統(tǒng)軟件的可靠性設(shè)計(jì)問(wèn)題，即已知前提條件是嵌入式系統(tǒng)所需的硬件穩(wěn)定可靠。

從理論上分析，已知一定的穩(wěn)定性和可靠性，一個(gè)嵌入式系統(tǒng)都有一個(gè)最小復(fù)雜度，但具體實(shí)現(xiàn)時(shí)往往不可能達(dá)到這個(gè)最小復(fù)雜度。在實(shí)際應(yīng)用中，類似于在錘子上刻花，即使增加了復(fù)雜度，也不會(huì)提高系統(tǒng)的穩(wěn)定性，而且，如果設(shè)計(jì)不當(dāng)，反而會(huì)降低系統(tǒng)的穩(wěn)定性。因此，犧牲比較小的代價(jià)來(lái)提高系統(tǒng)的穩(wěn)定性和可靠性，最理想的辦法就是減少系統(tǒng)不必要的復(fù)雜度。然而，對(duì)系統(tǒng)復(fù)雜度影響最大的就是軟件框架、嵌入式軟件模塊之間的可靠通信。嵌入式模塊之間的可靠通信，能夠抑制系統(tǒng)復(fù)雜度的不必要的增加。這樣，設(shè)計(jì)嵌入式模塊之間的可靠通信方式，就能實(shí)現(xiàn)以較低代價(jià)換取嵌入式系統(tǒng)的高可靠性和穩(wěn)定性。在下面幾節(jié)中我們將用Event-B[1～3]的不變量和事件來(lái)建模嵌入式模塊的內(nèi)部行為和可靠交互通信方式。

一、嵌入式服務(wù)軟件可靠交互行為建模

在本節(jié)，基于Event-B的不變量和事件(關(guān)于Event-B的詳細(xì)資料和語(yǔ)法，請(qǐng)參閱[1～3])，本文建模嵌入式系統(tǒng)服務(wù)軟件的可靠性交互行為，如圖1所示，利用外層服務(wù)訪問(wèn)接口，嵌入式系統(tǒng)可以訪問(wèn)外圍服務(wù)軟件。外圍服務(wù)軟件的性能直接影響著整個(gè)嵌入式系統(tǒng)的性能，因此，保障外圍服務(wù)軟件的可靠性，也會(huì)增強(qiáng)整個(gè)嵌入式系統(tǒng)的穩(wěn)定性和健壯性。

圖1　嵌入式系統(tǒng)結(jié)構(gòu)圖

利用Event-B的不變量和事件，本節(jié)建模外圍服務(wù)軟件的內(nèi)部行為和可靠交互方式。在外圍服務(wù)軟件中，可能存在多個(gè)軟件模塊，每個(gè)模塊之間通過(guò)接口或無(wú)線進(jìn)行通信。然而，在通信時(shí)，由于結(jié)構(gòu)或行為的不匹配，可能引起很多問(wèn)題。例如，兩個(gè)模塊如果接口實(shí)現(xiàn)協(xié)議不同，則他們不能進(jìn)行通信。兩個(gè)模塊是兼容的，當(dāng)且僅當(dāng)他們的接口是兼容的。在一個(gè)嵌入式系統(tǒng)中，其服務(wù)軟件的每個(gè)模塊之間通過(guò)通信活動(dòng)進(jìn)行交互。最基本的通信活動(dòng)包括信息發(fā)送(Send)和信息接收(Receive)，這樣構(gòu)成四種最基本的模塊雙邊互動(dòng)模型，如圖2所示。

圖2　軟件服務(wù)模塊雙邊互動(dòng)模式

本文考慮不同類型的信息發(fā)送，這依賴于傳遞是否可靠，在可靠的信息傳遞環(huán)境下，分析通信活動(dòng)是阻塞或非阻塞的。所有的發(fā)送模式用基于預(yù)期解釋的Event-B事件進(jìn)行建模，即對(duì)信息m進(jìn)行發(fā)送或傳遞。

1.發(fā)送模式

本小節(jié)分析三種最基本的信息發(fā)送模式，首先分析無(wú)可靠傳遞性的信息發(fā)送模式，接著介紹可靠下的無(wú)阻塞信息發(fā)送模式，最后總結(jié)了可靠下和阻塞下的信息發(fā)送模式。

(1)Send Without Guaranteed Delivery

在這種信息發(fā)送模式下，要求AckRequested和BlockingSend總設(shè)置為假，并把布爾值OkSend(m)和Arriving(m)設(shè)置為真。變量OkSend設(shè)置為真則表示信息正確發(fā)送，而Arriving信號(hào)則可以通知接收者信息m正在到達(dá)，并要準(zhǔn)備接收它。

Event BasicSend︽

where

grd1 : sendMode(m) = TRUE

grd2 : AckRequested(m) = FALSE

grd3 : BlockingSend(m) = FALSE

then

act1 : sendMode(m) := FALSE

act2 : OkSend(m) := TRUE

act3 : Arriving(m) := TRUE

end

(2)Guaranteed Non-Blocking Send

在這種信息發(fā)送模式下，具有確保發(fā)送機(jī)制，但是沒(méi)有阻塞效應(yīng)，要求AckRequested總是為真，而B(niǎo)lockingSend總是為假。同理，OkSend(m)和Arriving(m)都設(shè)置為真。另外，設(shè)置WaitingForAck為真，表示需要等待接收確認(rèn)信號(hào)。sendTime為當(dāng)前系統(tǒng)時(shí)間，并把截止時(shí)間設(shè)置為3個(gè)基本時(shí)間單位。

Event SendAckNonBlocking︽

where

grd1 : AckRequested(m) = TRUE

grd2 : BlockingSend(m) = FALSE

grd3 : m→s∈sender

then

act4 : WaitingForAck(s) := TRUE

act5 : sendTime(m) := CurrentTime

act6 : deadline(m) := 3

end

(3)Guaranteed Blocking Send

這種發(fā)送模式，即帶確認(rèn)機(jī)制的阻塞式信息發(fā)送模式。在這種發(fā)送模式下，要求AckRequested和BlockingSend總設(shè)置為真，s為信息m的發(fā)送者。通過(guò)WaitingForAck信號(hào)，保證了信息被發(fā)送后，能夠從接收方收到反饋信息。同時(shí)，通過(guò)把信號(hào)stateOfService設(shè)置為blocked，即將服務(wù)s的狀態(tài)設(shè)置為阻塞。

Event SendAckBlocking︽

where

grd3 : AckRequested(m) = TRUE

grd4 : BlockingSend(m) = TRUE

grd5 : m→s∈sender

then

act4 : WaitingForAck(s) := TRUE

act5 : sendTime(m) := CurrentTime

act6 : deadline(m) := 3

act9 : stateOfService(s) := blocked

end

2.接收模式

本小節(jié)討論四種信息接收模式。根據(jù)行為是阻塞的或非阻塞的，或者根據(jù)到達(dá)的信息是否被緩存以便于進(jìn)一步被處理，本節(jié)建模的四種信息接收模式分別為：接收者準(zhǔn)備接收的基本接收模式；第二種接收模式下，收到的信息將被舍棄；第三種情況下，接收者準(zhǔn)備好接收信息，而且信息不被舍棄、不被緩存，并要求反饋信息，但需要阻塞發(fā)送者；最后一種接收模式跟第三種相似，只是需要阻塞信息發(fā)送者。

(1)Basic receive where the recipient is ready to receive

在這種類型接收模式下，信息m不會(huì)被拋棄，也不會(huì)被緩存，并且服務(wù)行為不是阻塞的，服務(wù)也不要求返回確認(rèn)信號(hào)。因此，ReadyToReceive(m)設(shè)置為真，AckRequested(m)和BlockingSend(m)都設(shè)置為假。在下面的語(yǔ)法描述中，r為接收者，s為信息發(fā)送者，并把信息m添加到r的已接收信息集合中，把信息m包含的數(shù)據(jù)添加到接收到的數(shù)據(jù)集合中。

Event BasicReceiveReady︽

where

grd1 : Arriving(m) = TRUE

grd2 : ReadyToReceive(m) = TRUE

grd4 : AckRequested(m) = FALSE

grd5 : BlockingSend(m) = FALSE

then

act1 : Consume(m) := TRUE

end

Event Consume︽

where

grd3 : m→s∈sender

grd1 : Consume(m) = TRUE

grd2 : m→r∈recipient

then

act1 : receivedMessages(r) := (receivedMessages(r) ∪ {m})

act2 : receivedDatas := (receivedDatas) ∪ {d · d ∈{DatasOfmessage(m)}| r→ d}

end

(2)Basic receive where the message has to be discarded

這種接收模式環(huán)境下，信息m必須被扔掉，行為不被阻塞，而且不需要進(jìn)行信息接收確認(rèn)。但是，信息m將被緩存起來(lái)，如下所示，ToBeBuffered設(shè)置為真，并通過(guò)將其入隊(duì)來(lái)實(shí)現(xiàn)緩存。另外，信號(hào)ToBeDiscarded(m)設(shè)置為真，AckRequested(m)和BlockingSend(m)都設(shè)置為假。

Event BasicReceiveBuffer︽

any

m

r

where

grd1 : ToBeBuffered(m) = TRUE

grd2 : m→r∈recipient

grd3 : AckRequested(m) = FALSE

grd4 : BlockingSend(m) = FALSE

then

act1 : Enqueue(m) := TRUE

act2 : enqueueTime(m) := CurrentTime

act3 : Queue(r) := (Queue(r)) ∪ {m}

act4 : Arriving(m) := FALSE

act5 : ToBeBuffered(m) := FALSE

act6 : dequeueTime(m) := 3

end

(3)Receive where the recipient is ready to end the action request an acknowledgment

對(duì)于信息m，將ReadyToReceive(m)和AckRequested(m)都設(shè)置為真，并把BlockingSend(m)設(shè)置為假，這樣，信息m不會(huì)被扔掉，但也不會(huì)被緩存，但是動(dòng)作行為要求確認(rèn)。

Event ReceiveAckNonBlockingReady︽

where

grd1 : m → r ∈ recipient

grd2 : Arriving(m) = TRUE

grd3 : ReadyToReceive(m) = TRUE

grd4 : AckRequested(m) = TRUE

grd5 : BlockingSend(m) = FALSE

then

act1 : SendAck(r) := TRUE

end

(4)Receive where the recipient is ready to and the action is blocking

這種接收模式下，接收者準(zhǔn)備好接收信息，而且信息不被舍棄，但是當(dāng)接收者在接收信息的時(shí)候，必須阻塞發(fā)送者，當(dāng)接收者完全接收后，再把發(fā)送者解除阻塞。

Event ReceiveAckBlockingReady︽

where

grd3 : Arriving(m) = TRUE

grd4 : ReadyToReceive(m) = TRUE

grd5 : AckRequested(m) = TRUE

grd6 : BlockingSend(m) = TRUE

then

act1 : SendAck(r) := TRUE

end

二、驗(yàn)證

首先進(jìn)行一致性檢查，即檢查系統(tǒng)中模塊之間的行為一致性，也就是模塊之間通信協(xié)議的一致性。在通信時(shí)，如果兩個(gè)模塊的通信協(xié)議陷入混亂，則這兩個(gè)模塊行為不匹配。其實(shí)，模塊之間通過(guò)具有非常嚴(yán)格順序的消息進(jìn)行通信。通過(guò)分析信息數(shù)據(jù)交換的順序約束，以及死鎖的存在，能夠分析出模塊之間的行為是否存在不一致性。

在一個(gè)嵌入式系統(tǒng)中，其外層服務(wù)軟件的每個(gè)模塊服務(wù)和其依賴模塊之間都有一個(gè)有線或無(wú)線關(guān)系，它們之間必須遵循協(xié)議一致性和匹配性。這條限制規(guī)則通過(guò)不變量inv_ wire_ protocols_ compatibility 來(lái)進(jìn)行定義。我們規(guī)定，對(duì)于一個(gè)模塊s和其依賴模塊r之間具有一個(gè)r → s∈Wire關(guān)系，他們之間的服務(wù)協(xié)議也是一致的和兼容的，即有：protocolOf Service(s) → protocolOf Service(r) ∈compatibleProtocols。inv_ wire_ protocols_ compatibility : ?s, r·s ∈

componentServices ∧ r ∈ componentReferences ∧ s →

r ∈ Wire ? protocolOfService(s) →

protocolOfService(r) ∈ compatibleProtocols

有時(shí)一個(gè)模塊發(fā)送一個(gè)消息，但是另外一個(gè)模塊可能不希望收到此消息，因?yàn)樗诘却渌南?lái)臨。比如：協(xié)議p1正在給協(xié)議p2發(fā)送消息m1，但是p2不需要m1，因?yàn)樗枰2。在此上下文環(huán)境下，我們定義另外一個(gè)服務(wù)，表示為intermediateService，它的作用是負(fù)責(zé)接收消息m1并臨時(shí)存儲(chǔ)它，當(dāng)p2下次需要m1的時(shí)候再傳送給它。我們用inv _Unspecified _reception Event_B不變量來(lái)進(jìn)行定義：

inv Unspecified reception : ?p1 , p2 · p1 → p2 ∈

NoUnspecifiedReception ? (?i ·p1 → i ∈

interactionsOfP ∧ i = send ? ((stateOfP(p1 ) =

sendState) ∧ (stateOfP(p2) = receiveState)) ∧

sendMessage(p1 ) = TRUE ∧ receiveMessage(p2) =

TRUE ∧ sendAck(p2) = TRUE ∧ receiveAck(p1 ) =

TRUE)

三、結(jié)語(yǔ)

為了提高嵌入式系統(tǒng)的可靠性，提高其外層服務(wù)軟件的可靠性和健壯性變得非常重要，而且能夠?qū)崿F(xiàn)以較低代價(jià)換取高穩(wěn)定性。本文用Event-B的不變量和事件來(lái)建模嵌入式軟件服務(wù)模塊的內(nèi)部行為和可靠交互通信方式。首先對(duì)嵌入式服務(wù)軟件可靠行為進(jìn)行建模，重點(diǎn)對(duì)信息的發(fā)送模式和信息接收模式進(jìn)行了建模。接著分析了驗(yàn)證方法，即進(jìn)行一致性檢查，檢查系統(tǒng)中模塊之間的行為一致性，也就是模塊之間通信協(xié)議的一致性。

參考文獻(xiàn)：

[1]A. Lahouij, L. Hamel, and M. Graiet.Formal verification of SCA assembly model with event-b[J]. In Ninth International Conference on Semantics, Knowledge and Grids, SKG 2013, Beijing, China, October 3-4, 2013, 2013. 44～51.

[2] S. Basu and T. Bultan.Automatic verification of interactions in asynchronous systems with unbounded buffers[J]. In ACM/IEEE International Conference on Automated Software Engineering, ASE，2014, (14)： 743～754.

[3] D. Cansell and D. Mery.The event-b modelling method[J].Concepts and case studies, 2008. 47～152.

文章編號(hào)：2095-4654(2016)03-0001-04

基金項(xiàng)目：湖北科技學(xué)院校級(jí)青年課題資助(KY10037)

* 收稿日期：2015-12-22

中圖分類號(hào)：TP311.5

文獻(xiàn)標(biāo)識(shí)碼：A