楊　榮

(湖北科技學院　計算機科學與技術(shù)學院，湖北　咸寧　437100)

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

楊榮

(湖北科技學院計算機科學與技術(shù)學院，湖北咸寧437100)

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

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

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

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

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

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

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

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

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

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

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

1.發(fā)送模式

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

(1)Send Without Guaranteed Delivery

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

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ā)送機制，但是沒有阻塞效應(yīng)，要求AckRequested總是為真，而BlockingSend總是為假。同理，OkSend(m)和Arriving(m)都設(shè)置為真。另外，設(shè)置WaitingForAck為真，表示需要等待接收確認信號。sendTime為當前系統(tǒng)時間，并把截止時間設(shè)置為3個基本時間單位。

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ā)送模式，即帶確認機制的阻塞式信息發(fā)送模式。在這種發(fā)送模式下，要求AckRequested和BlockingSend總設(shè)置為真，s為信息m的發(fā)送者。通過WaitingForAck信號，保證了信息被發(fā)送后，能夠從接收方收到反饋信息。同時，通過把信號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ù)到達的信息是否被緩存以便于進一步被處理，本節(jié)建模的四種信息接收模式分別為：接收者準備接收的基本接收模式；第二種接收模式下，收到的信息將被舍棄；第三種情況下，接收者準備好接收信息，而且信息不被舍棄、不被緩存，并要求反饋信息，但需要阻塞發(fā)送者；最后一種接收模式跟第三種相似，只是需要阻塞信息發(fā)送者。

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

在這種類型接收模式下，信息m不會被拋棄，也不會被緩存，并且服務(wù)行為不是阻塞的，服務(wù)也不要求返回確認信號。因此，ReadyToReceive(m)設(shè)置為真，AckRequested(m)和BlockingSend(m)都設(shè)置為假。在下面的語法描述中，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必須被扔掉，行為不被阻塞，而且不需要進行信息接收確認。但是，信息m將被緩存起來，如下所示，ToBeBuffered設(shè)置為真，并通過將其入隊來實現(xiàn)緩存。另外，信號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

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

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

這種接收模式下，接收者準備好接收信息，而且信息不被舍棄，但是當接收者在接收信息的時候，必須阻塞發(fā)送者，當接收者完全接收后，再把發(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

二、驗證

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

在一個嵌入式系統(tǒng)中，其外層服務(wù)軟件的每個模塊服務(wù)和其依賴模塊之間都有一個有線或無線關(guān)系，它們之間必須遵循協(xié)議一致性和匹配性。這條限制規(guī)則通過不變量inv_ wire_ protocols_ compatibility 來進行定義。我們規(guī)定，對于一個模塊s和其依賴模塊r之間具有一個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

有時一個模塊發(fā)送一個消息，但是另外一個模塊可能不希望收到此消息，因為它在等待其他的消息來臨。比如：協(xié)議p1正在給協(xié)議p2發(fā)送消息m1，但是p2不需要m1，因為它需要消息m2。在此上下文環(huán)境下，我們定義另外一個服務(wù)，表示為intermediateService，它的作用是負責接收消息m1并臨時存儲它，當p2下次需要m1的時候再傳送給它。我們用inv _Unspecified _reception Event_B不變量來進行定義：

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é)語

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

參考文獻：

[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.

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

基金項目：湖北科技學院校級青年課題資助(KY10037)

* 收稿日期：2015-12-22

中圖分類號：TP311.5

文獻標識碼：A