李愛(ài)萍，馬俊偉，段利國(guó)

(太原理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,太原 030024)

?

智能家居平臺(tái)構(gòu)件適應(yīng)與協(xié)同模型及形式化分析

李愛(ài)萍，馬俊偉，段利國(guó)

(太原理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,太原 030024)

摘要:以解決智能家居平臺(tái)運(yùn)行過(guò)程中的構(gòu)件適應(yīng)與協(xié)同問(wèn)題為目的，保證設(shè)備獨(dú)立性與數(shù)據(jù)一致性為特點(diǎn)，提出一種基于構(gòu)件適應(yīng)與協(xié)同的智能家居平臺(tái)邏輯模型,對(duì)平臺(tái)及各構(gòu)件進(jìn)行形式化描述與建模,并結(jié)合平臺(tái)功能需求對(duì)模型性質(zhì)進(jìn)行分析與驗(yàn)證。實(shí)驗(yàn)表明,在本模型下平臺(tái)構(gòu)件的適應(yīng)與協(xié)同滿足不死鎖、不中止、不發(fā)散的必要性質(zhì),且在并行處理多用戶請(qǐng)求的條件下能夠?qū)崿F(xiàn)數(shù)據(jù)一致性與操作有效性。本研究對(duì)智能家居平臺(tái)的研發(fā)與驗(yàn)證有一定意義。

關(guān)鍵詞:智能家居平臺(tái);構(gòu)件適應(yīng);構(gòu)件協(xié)同;形式化

智能家居平臺(tái)是針對(duì)智能家居設(shè)備管理的軟件開(kāi)發(fā)框架[1-2]。一般定義智能設(shè)備及控制程序的訪問(wèn)接口、協(xié)議及控制方法,將家庭看作一個(gè)智能家居設(shè)備的集合,通過(guò)家庭、房間、區(qū)域的概念把這些設(shè)備有機(jī)地組合起來(lái)。在對(duì)設(shè)備的控制上,硬件設(shè)備被定義成提供一個(gè)或者多個(gè)服務(wù)的單元,而這些服務(wù)可以被第三方控制程序發(fā)現(xiàn)和調(diào)用[2-3]。

構(gòu)件適應(yīng)是軟件工程中的一個(gè)關(guān)鍵問(wèn)題[4-5],是指將部分滿足要求的構(gòu)件按照合適的適應(yīng)結(jié)構(gòu)組裝在一起,形成滿足用戶需求的復(fù)合構(gòu)件。智能家居平臺(tái)需要將智能設(shè)備、控制程序、操作系統(tǒng)等構(gòu)件復(fù)合成為用戶提供服務(wù)的綜合系統(tǒng),各構(gòu)件的適應(yīng)與協(xié)同就顯得至關(guān)重要。而目前國(guó)內(nèi)外在該領(lǐng)域的研究工作較少,且缺乏基于嚴(yán)謹(jǐn)數(shù)學(xué)基礎(chǔ)的形式化研究支持,導(dǎo)致平臺(tái)構(gòu)件適應(yīng)協(xié)同等問(wèn)題無(wú)法進(jìn)行有效驗(yàn)證,大大阻礙了智能家居行業(yè)的創(chuàng)新與發(fā)展。

以解決平臺(tái)運(yùn)行過(guò)程中的構(gòu)件適應(yīng)與協(xié)同問(wèn)題為目的,保證設(shè)備獨(dú)立性與數(shù)據(jù)一致性為特點(diǎn),提出一種基于構(gòu)件適應(yīng)與協(xié)同的智能家居平臺(tái)邏輯模型,對(duì)構(gòu)件及平臺(tái)進(jìn)行形式化描述與建模,并結(jié)合平臺(tái)功能需求對(duì)模型性質(zhì)進(jìn)行分析與驗(yàn)證,證明了模型的正確性與實(shí)用性。

1相關(guān)工作

文獻(xiàn)[10]設(shè)計(jì)了一種智能家居系統(tǒng)規(guī)則沖突避免和沖突檢測(cè)的方法,它將場(chǎng)景中的用戶、觸發(fā)器、環(huán)境實(shí)體和執(zhí)行器這四個(gè)部分抽取出來(lái),建立UTEA (User-Trigger-Environment-Actuator)形式化的模型;進(jìn)而定義了多種規(guī)則關(guān)系和沖突模型,最后設(shè)計(jì)了沖突檢測(cè)算法。但并未對(duì)系統(tǒng)本身的性質(zhì)進(jìn)行研究,且尚未實(shí)現(xiàn)對(duì)系統(tǒng)其它關(guān)鍵性質(zhì)如數(shù)據(jù)一致性等問(wèn)題的分析驗(yàn)證。

文獻(xiàn)[11]提出一個(gè)智能家居上下文模型,根據(jù)智能家居系統(tǒng)自身的需求和上下文感知工作流框架的特點(diǎn),采用FollowMe框架進(jìn)行智能家居平臺(tái)設(shè)計(jì)?？稍谙到y(tǒng)投入運(yùn)行之前對(duì)系統(tǒng)的正確性進(jìn)行驗(yàn)證,發(fā)現(xiàn)系統(tǒng)潛在的漏洞,避免系統(tǒng)投入運(yùn)行后發(fā)生嚴(yán)重的錯(cuò)誤。然而驗(yàn)證過(guò)程結(jié)構(gòu)復(fù)雜,容易出現(xiàn)錯(cuò)誤信號(hào)甚至沖突,導(dǎo)致驗(yàn)證可靠性大打折扣。

文獻(xiàn)[12-13]分別提出了基于ZigBee和Android平臺(tái)的智能家居系統(tǒng)。研究重點(diǎn)皆為功能的豐富和性能的優(yōu)化,并未對(duì)系統(tǒng)可靠性、并行處理性質(zhì)等作出分析,其實(shí)驗(yàn)結(jié)果難以令人信服。

2智能家居平臺(tái)邏輯模型

智能家居平臺(tái)的實(shí)際系統(tǒng)結(jié)構(gòu)包括感知層、傳輸層及應(yīng)用層等[14],本文僅研究應(yīng)用層上各構(gòu)件的適應(yīng)與協(xié)同,并以此為目的建立邏輯模型進(jìn)行形式化分析與驗(yàn)證。

智能家居平臺(tái)的邏輯模型如圖1所示,分為四類構(gòu)件。

1) 控制程序(Control App)。即用戶使用的第三方應(yīng)用,它從操作系統(tǒng)的數(shù)據(jù)容器中獲知當(dāng)前智能設(shè)備的狀態(tài),并通過(guò)智能家居開(kāi)發(fā)框架所提供的接口來(lái)對(duì)智能設(shè)備進(jìn)行控制。

2) 設(shè)備控制框架(Accessories Controlling Frameworks)。設(shè)備控制框架是智能家居平臺(tái)的核心部分,它定義實(shí)現(xiàn)智能家居管理的類、關(guān)系和方法,實(shí)現(xiàn)控制程序?qū)χ悄茉O(shè)備的控制。操作系統(tǒng)(Operating System)是控制框架的載體,框架方法的實(shí)現(xiàn)可能需要調(diào)用操作系統(tǒng)的相關(guān)接口。另外,實(shí)現(xiàn)對(duì)設(shè)備的控制應(yīng)至少需要以下兩個(gè)大類，

a.Home表示一個(gè)獨(dú)立的房屋,不同的房屋需要分別進(jìn)行控制。一個(gè)房屋可能由多個(gè)用戶進(jìn)行管理,并存在多個(gè)房間(Room),設(shè)備可以被附屬在Room中,用戶通過(guò)Room找到智能設(shè)備,進(jìn)行單個(gè)或統(tǒng)一通信和配置。

b.AccessoryOb表示房屋中一個(gè)獨(dú)立的智能設(shè)備。一個(gè)智能設(shè)備有且僅有一個(gè)AccessoryOb對(duì)象與其對(duì)應(yīng)。一個(gè)AccessoryOb對(duì)象提供一個(gè)或多個(gè)服務(wù)(service),每個(gè)Service有多個(gè)屬性(characteristics)來(lái)表示其狀態(tài)。

3) 數(shù)據(jù)容器(Common Database)。數(shù)據(jù)容器是操作系統(tǒng)中用于保持?jǐn)?shù)據(jù)一致性的數(shù)據(jù)存儲(chǔ)器。智能設(shè)備的狀態(tài)信息被存儲(chǔ)在Common Database中,所有控制程序都須從此獲得設(shè)備信息。

4) 智能設(shè)備(Accessory)。即所要控制的智能設(shè)備硬件。

圖1　智能家居平臺(tái)邏輯模型Fig.1　Logical Model of Frameworks for Smart Home

3智能家居平臺(tái)及構(gòu)件的形式化描述

借鑒文獻(xiàn)[5]的描述方法,智能家居平臺(tái)中每個(gè)構(gòu)件的形式化描述規(guī)則如下。

式中：D是所有輸入值的集合;R是所有輸出值的集合;I(x)表示所有前置條件,每一個(gè)前置條件定義了構(gòu)件的合法輸入,只有前置條件被滿足時(shí)相應(yīng)服務(wù)才能被執(zhí)行(前置條件是在提供服務(wù)之前對(duì)象狀態(tài)的約束);O(x,y) 表示所有后置條件,即提供服務(wù)后所得到的所有狀態(tài)的集合(后置條件是在提供服務(wù)之后對(duì)象狀態(tài)的約束),每一個(gè)后置條件定義了一個(gè)合法輸入所對(duì)應(yīng)的所有合法輸出。例如:

Component(inxseq, outyN, outzN)

prex≠Null

post1y∈elements(x) ∧(?e∈elements(x)|y≥e)

post2z∈elements(x) ∧(?e∈elements(x)|y≤e)式中：符號(hào)‘in’ 代表輸入?yún)?shù);符號(hào) ‘out’ 代表輸出參數(shù); ‘seq’ 和 ‘N’ 表示參數(shù)類型;‘pre’ 代表前置條件,描述了構(gòu)件的所有合法輸入;‘post1’ 和‘post2’ 代表后置條件,描述了構(gòu)件所有的合法輸出。

3.1構(gòu)件形式化模型

3.1.1控制程序構(gòu)件

ControlApps(in Room seq,in Acc seq,in Ser seq,in Cha seq,in Cmd seq,out Room seq, out Acc seq, out Req seq)

pre1Room ∈ elements (rooms)

pre2Acc∈(elements (accessories,rooms)∧(rooms==Room))

pre3Ser∈(elements (services, accessories)∧ (accessories==Acc))

pre4Cha∈(elements (characteristics, services) ∧ (services=Ser))

pre5Cmd∈(elements (commands, rooms,accessories) ∧ (rooms==Room)∧ (accessories==Acc))

post1Req∈(elements (requests, rooms, accessories, commands)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (commands==Cmd))

控制程序構(gòu)件的輸入?yún)?shù)為房間(Room)、設(shè)備(Acc)、服務(wù)(Ser)、屬性(Cha)和命令(Cmd),輸出為同一房間、設(shè)備及用于控制程序和設(shè)備控制框架進(jìn)行協(xié)同的命令(Req)。前置條件為Room屬于房間集合elements(rooms)中的元素,Acc屬于當(dāng)rooms值等于Room時(shí)二元組elements(accessories, rooms)中的元素,其他前置條件的表示方法與含義與其類似。后置條件為Req屬于在Room、Acc、Cmd為確定值時(shí)四元組elements (requests, rooms, accessories, commands)中的元素。

其他構(gòu)件的形式化描述方法與含義與該構(gòu)件相類似。

3.1.2設(shè)備控制框架構(gòu)件

該構(gòu)件的輸入構(gòu)件有控制程序及智能設(shè)備兩個(gè),且其中一個(gè)為輸入時(shí),另一個(gè)為輸出。因此需要表示為兩個(gè)部分。

輸入為控制程序時(shí):

OS1(in Room seq, in Acc seq, in Req seq, out Ctrl seq)

pre1Room∈elements (rooms)

pre2Acc∈(elements (accessories, rooms) ∧ (rooms==Room))

pre3Req∈(elements (requests, rooms, accessories)∧ (rooms==Room) ∧ (accessories==Acc))

postCtrl∈(elements (controls, rooms, accessories, requests)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (requests==Req))

其中Ctrl是用于設(shè)備控制框架與智能設(shè)備進(jìn)行協(xié)同的命令。

輸入為智能設(shè)備時(shí):

OS2(in Ser2 seq,in Cha2 seq, out Room2 seq, out Acc2 seq,out Ser2 seq, out Cha2 seq)

pre1Ser2∈(elements (services, accessories)∧ (accessories=Acc)) ?Ser2==null

pre2Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ?Cha2==null

post1Room2∈elements (rooms)?Room2==null

post2Acc2∈(elements (accessories, rooms)∧ (room=Room2)) ?Acc2==null

post3Ser2∈(elements (services, accessories)∧ (accessories=Acc2)) ?Ser2==null

post4Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ?Cha2==null

3.1.3智能設(shè)備構(gòu)件

Accessory(in Ctrl seq, out Ser2 seq, out Cha2 seq)

preCtrl∈(elements (controls, rooms, accessories)∧ (rooms==Room) ∧ (accessories==Acc))

post1Ser2∈(elements (services, accessories)∧ (accessories=Acc)) ?Ser2==null

post2Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ?Cha2==null

3.1.4數(shù)據(jù)容器構(gòu)件

Database(in Room2, in Acc2 seq, in Ser2 seq, in Cha2 seq, out Room3 seq, out Acc3 seq, out Ser3 seq, out Cha3 seq)

pre1Room2∈elements (rooms)

pre2Acc2∈(elements (accessories, rooms) ∧ (rooms==Room2))

pre3Ser2∈(elements (services, accessories)∧ (accessories==Acc2))

pre4Cha2∈(elements (characteristics, services) ∧ (services=Ser2))

post1Room3∈elements (rooms)

post2Acc3∈(elements (accessories, rooms) ∧ (rooms==Room3))

post3Ser3∈(elements (services, accessories)∧ (accessories==Acc3))

post4Cha3∈(elements (characteristics, services) ∧ (services=Ser3))

數(shù)據(jù)容器存儲(chǔ)從設(shè)備控制框架輸入的房間和設(shè)備信息并進(jìn)行更新,同時(shí)提供控制程序需要的房間設(shè)備信息。

3.2智能家居平臺(tái)形式化模型

在平臺(tái)系統(tǒng)各構(gòu)件模型已確立的基礎(chǔ)上,按照復(fù)合構(gòu)件構(gòu)造規(guī)則[4]對(duì)各構(gòu)件進(jìn)行復(fù)合,得出智能家居平臺(tái)構(gòu)件適應(yīng)與協(xié)同的整體系統(tǒng)模型。

模型為循環(huán)結(jié)構(gòu),執(zhí)行過(guò)程為:

System=ControlApps+OS1+Accessory+OS2+Database+System*

式中：符號(hào)‘+’表示構(gòu)件的順序執(zhí)行關(guān)系,執(zhí)行語(yǔ)義是依次執(zhí)行ControlApps、OS1、Accessory、OS2 、Database五個(gè)構(gòu)件,最后再次執(zhí)行System；*表示0或多次的重復(fù),用于表示平臺(tái)對(duì)智能設(shè)備的多次控制。

智能家居平臺(tái)整體模型形式化描述如下:

System (in room seq, in acc seq, in ser seq, in cha seq, in cmd seq, out room’ seq, out acc’ seq, out ser’ seq, out cha’ seq)

pre1Room∈elements (rooms)

pre2Acc∈(elements (accessories, rooms) ∧ (rooms==Room))

pre3Ser∈(elements (services, accessories)∧ (accessories==Acc))

pre4Cha∈(elements (characteristics, services) ∧ (services=Ser’))

pre5Cmd∈(elements (commands, rooms, accessories) ∧ (rooms==Room)∧ (accessories==Acc))

post1?Req∈(elements (requests, rooms, accessories, commands)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (commands==Cmd))

post2?Ctrl∈(elements (controls, rooms, accessories, requests)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (requests==Req))

post3Room’∈elements (rooms)?Room’==null

post4Acc’∈(elements (accessories, rooms)∧ (room=Room’)) ?Acc’==null

post5Ser’∈(elements (services, accessories)∧ (accessories=Acc’)) ?Ser’==null

post6Cha’∈(elements (characteristics, services)∧ (services=Ser’)) ?Cha’==null

4模型應(yīng)用實(shí)驗(yàn)

智能家居平臺(tái)應(yīng)使用戶能夠在搭載平臺(tái)的操作系統(tǒng)上通過(guò)應(yīng)用程序控制和配置智能設(shè)備,主要實(shí)現(xiàn)以下四大功能[3]:

1) 房間設(shè)置。用戶能夠創(chuàng)建、命名、調(diào)整以及刪除虛擬的房間及房間組合。

2) 用戶管理。具有相關(guān)權(quán)限的用戶能夠?qū)Ξ?dāng)前連接在同一家庭中的其他用戶進(jìn)行管理。

3) 設(shè)備的增加與刪減。用戶可以便捷地發(fā)現(xiàn)設(shè)備并將其添加到相應(yīng)房間中,也可以快捷地刪除設(shè)備。

4) 情景設(shè)置。用戶可以對(duì)多個(gè)設(shè)備進(jìn)行配置,并將其定義為一個(gè)“情景”,從而通過(guò)對(duì)“情景”的控制來(lái)方便地調(diào)配多個(gè)智能設(shè)備。

4.1構(gòu)件協(xié)同模型建模

應(yīng)用實(shí)驗(yàn)以本文提出的形式化模型為基礎(chǔ),模擬在智能家居平臺(tái)模型上并發(fā)進(jìn)行各類功能操作的過(guò)程,來(lái)檢驗(yàn)構(gòu)件協(xié)同性質(zhì)以及并行處理性質(zhì)。模擬工具為形式化進(jìn)程分析工具PAT平臺(tái),使用語(yǔ)言為CSP#。

為保持?jǐn)?shù)據(jù)一致性,對(duì)數(shù)據(jù)容器和智能設(shè)備的任何操作都需要互斥進(jìn)行[15]。因此,以經(jīng)典算法面包店算法[16]作為各進(jìn)程訪問(wèn)以上資源的互斥算法,并表示為進(jìn)程Cs()。在組成智能家居系統(tǒng)的過(guò)程中,構(gòu)件之間需要進(jìn)行適應(yīng)連接及工作協(xié)同,而在實(shí)際運(yùn)行過(guò)程中則表現(xiàn)為通過(guò)協(xié)議進(jìn)行通信交互。整個(gè)過(guò)程的形式化表示中會(huì)涉及構(gòu)件間的多個(gè)通信協(xié)議,為增強(qiáng)模型易讀性,直接以協(xié)議名稱表示通信事件。

4.1.1房間設(shè)置功能過(guò)程建模

對(duì)該功能所要完成的任務(wù)進(jìn)行分析,用戶首先通過(guò)Cs()進(jìn)程從數(shù)據(jù)容器中獲知房間當(dāng)前情況,隨后發(fā)出配置請(qǐng)求事件requestA。實(shí)現(xiàn)對(duì)Room的控制。HomeDelegate協(xié)議實(shí)現(xiàn)從應(yīng)用程序到平臺(tái)的通信。homeoperateR事件表示對(duì)請(qǐng)求進(jìn)行的處理,最后調(diào)用Cs()在Common Database中寫(xiě)入最新配置信息,同時(shí)通過(guò)協(xié)議將結(jié)果返回用戶程序。該功能行為流程用CSP#建模表示為:

SetupHome()=Cs();requestA-> HomeDelegate-> homeoperateR-> Cs(); HomeDelegate-> Skip

4.1.2用戶管理功能行為流程表示

用戶通過(guò)Cs()獲取當(dāng)前用戶信息,隨后發(fā)出用戶管理請(qǐng)求requestB。用戶信息由Home模塊進(jìn)行處理,因此通過(guò)HomeDelegate協(xié)議進(jìn)行傳達(dá)。HomeoprateU表示Home模塊收到指令后對(duì)用戶進(jìn)行操作,最后調(diào)用Cs()更新信息,同時(shí)使用協(xié)議將處理結(jié)果返回用戶。該功能行為流程用CSP#建模表示為:

ManageUsers()=Cs();requestB->HomeDelegate-> homeoprateU-> Cs();HomeDelegate-> Skip

4.1.3設(shè)備增刪功能行為流程表示

用戶調(diào)用Cs()后發(fā)出設(shè)備增刪請(qǐng)求requestC,通過(guò)HomeDelegate協(xié)議與Home模塊協(xié)同,通過(guò)homeoprateB操作增刪設(shè)備。最后通過(guò)Cs()更新信息并通過(guò)AccessoryDelegate協(xié)議告知用戶結(jié)果。該功能行為流程用CSP#建模表示為:

AddandRemovingAccessories()=Cs(); requestC-> (HomeDelegate-> homeoprateB-> Cs();AccessoryDelegate-> Skip

4.1.4情景設(shè)置功能行為流程表示

用戶在設(shè)置情景時(shí)是對(duì)多個(gè)家居設(shè)備進(jìn)行配置,但彼此之間是互相獨(dú)立的。為簡(jiǎn)化模型,減少系統(tǒng)狀態(tài)數(shù),將此功能的行為流程模擬為對(duì)單個(gè)設(shè)備的配置,最后通過(guò)聲明多個(gè)該過(guò)程模型來(lái)達(dá)到模擬情景設(shè)置的情況。首先用戶仍然是通過(guò)Cs()獲得設(shè)備當(dāng)前的設(shè)置,然后發(fā)出操作指令requestD,通過(guò)HomeDelegate協(xié)議傳遞至AccessoryOb模塊。accoperate事件表示模塊在進(jìn)行相關(guān)處理,處理后通過(guò)預(yù)定義的協(xié)議CommunicateDelegate與設(shè)備進(jìn)行通信。隨后設(shè)備根據(jù)命令進(jìn)行操作,表示為事件accessoyconf,最后通過(guò)callback事件返回結(jié)果。由于設(shè)備是臨界資源,故從accoperate事件到callback事件為原子操作,在CSP#中用atomic{}進(jìn)行表示。最后調(diào)用Cs()將更改后的設(shè)備信息寫(xiě)入數(shù)據(jù)容器并通過(guò)AccessoryDelegate協(xié)議告知用戶結(jié)果。該功能行為流程用CSP#建模表示為:

DefScenes()=Cs(); requestD-> HomeDelegate-> atomic {accoperate->CommunicateDelegate-> accessoryconf-> callback-> Skip};Cs();AccessoryDelegate-> Skip

綜上,智能家居平臺(tái)所實(shí)現(xiàn)的四大功能流程CSP#建模已完成。對(duì)于一個(gè)用戶,其通過(guò)平臺(tái)對(duì)智能家居在家庭中進(jìn)行配置的所有操作就包含于以上四個(gè)功能之中。因此,以一個(gè)user()進(jìn)程表示一個(gè)用戶的行為,該用戶在某一時(shí)間所做的操作為以上功能之一。用CSP#表示為:

User(i)=SetupHome() [] ManageUsers() [] AddandRemovingAccessories() [] DefScenes()

其中參數(shù)i為用戶編號(hào)。

最后,模擬N個(gè)用戶同時(shí)通過(guò)智能家居平臺(tái)來(lái)配置智能家居作為整個(gè)系統(tǒng)的進(jìn)程System()。

System()=|||m:{0..N-1} @ User(m)

4.2模型性質(zhì)的分析與驗(yàn)證

實(shí)驗(yàn)從構(gòu)件協(xié)同性質(zhì)和并行處理性質(zhì)兩方面進(jìn)行分析與驗(yàn)證。

4.2.1構(gòu)件有效適應(yīng)與協(xié)同的性質(zhì)驗(yàn)證

在協(xié)同性質(zhì)方面,該行為流程模型所涉及的構(gòu)件適應(yīng)與協(xié)同應(yīng)具備不死鎖、不中止、不發(fā)散的性質(zhì)[17]。用CSP#斷言可表示為:

#assert System() deadlockfree;

#assert System() divergencefree;

#assert System() nonterminating.

通過(guò)PAT平臺(tái)對(duì)流程模型進(jìn)行自動(dòng)驗(yàn)證,可以得出構(gòu)件的適應(yīng)與協(xié)同具備相關(guān)性質(zhì)。

4.2.2模型并行處理性質(zhì)驗(yàn)證

本驗(yàn)證通過(guò)LTL線性時(shí)序邏輯[18]驗(yàn)證對(duì)模型并行處理多用戶請(qǐng)求時(shí)的數(shù)據(jù)一致性與操作有效性進(jìn)行驗(yàn)證。具體來(lái)說(shuō):第一,數(shù)據(jù)容器作為臨界資源,不能同時(shí)有大于一個(gè)的用戶對(duì)其進(jìn)行訪問(wèn);第二,在情景設(shè)置功能中成功對(duì)設(shè)備狀態(tài)進(jìn)行更改才能達(dá)到目的,因此需要驗(yàn)證requestD指令發(fā)生后是否總能發(fā)生accessoyconf事件;第三,為保證數(shù)據(jù)一致性,每個(gè)用戶進(jìn)行使用任一功能時(shí)都需要訪問(wèn)兩次Common Database,在讀取一次數(shù)據(jù)后必須還有一次寫(xiě)入操作。第四,為確保Common Database中的數(shù)據(jù)正確表示對(duì)應(yīng)家居設(shè)備的情況,需要驗(yàn)證數(shù)據(jù)返回后、寫(xiě)入Common Database之前,是否有其他事件更改設(shè)備數(shù)據(jù)。在PAT中相關(guān)語(yǔ)句和表示為:

#define collision (count> 1);

#assert System() |=collision;

#assert System() |=requestD-> []<>accessoryconf;

#assert User() |=ncs->[]<>ncs;

#assert User() |=callback-> Skip->[]ncs

在以上五條語(yǔ)句中,首先將用于記錄臨界區(qū)用戶數(shù)的count參數(shù)大于1的情況定義為collision事件,然后聲明斷言驗(yàn)證System()是否有collision事件出現(xiàn)。若沒(méi)有,即驗(yàn)證不通過(guò),則說(shuō)明臨界資源不存在用戶數(shù)大于1的情況;第三條表示在System()中若發(fā)生requestD事件,則接下來(lái)必發(fā)生accessoryconf事件;第四條中ncs事件為互斥算法中的第一個(gè)事件,一個(gè)User()中發(fā)生兩次該事件則說(shuō)明其訪問(wèn)量?jī)纱蜟ommon Database,完成了讀和寫(xiě)的操作;第五條表示發(fā)生callback事件且原子操作結(jié)束后(Skip),下一個(gè)事件是否始終為ncs;若不是,則說(shuō)明存在其它事件修改數(shù)據(jù)的潛在風(fēng)險(xiǎn)。

同樣地,使用PAT平臺(tái)對(duì)流程模型的并行處理性質(zhì)進(jìn)行LTL檢測(cè),從結(jié)果可以得出模型具有所要驗(yàn)證的性質(zhì)。

將本文所提模型的驗(yàn)證結(jié)果與第二節(jié)中的相關(guān)工作進(jìn)行比較,可得以下優(yōu)點(diǎn):

1) 實(shí)現(xiàn)了控制器與智能設(shè)備的相對(duì)獨(dú)立。在本模型中,控制程序與智能設(shè)備通過(guò)操作系統(tǒng)進(jìn)行協(xié)同,兩者相互獨(dú)立。兩個(gè)部分的開(kāi)發(fā)者只需遵從系統(tǒng)提供的接口即可進(jìn)行開(kāi)發(fā),實(shí)現(xiàn)了軟件和硬件端的相對(duì)獨(dú)立設(shè)計(jì)與操作。

2) 解決了構(gòu)件協(xié)同中的數(shù)據(jù)一致性難題。本模型中的數(shù)據(jù)都儲(chǔ)存在數(shù)據(jù)容器中,所有操作都需要在其中讀取或?qū)懭霐?shù)據(jù),保證了對(duì)設(shè)備進(jìn)行操作的有效性和安全性等。

3) 實(shí)現(xiàn)了設(shè)備的聯(lián)動(dòng)操作。由于設(shè)備被安排在房間中,因此可以以房間為單位進(jìn)行從屬設(shè)備的統(tǒng)一設(shè)置與聯(lián)動(dòng)操作,亦可以以情境為前提進(jìn)行多個(gè)設(shè)備的設(shè)定。真正實(shí)現(xiàn)智能地為用戶服務(wù),而不是單一、復(fù)雜地操作設(shè)備。

5結(jié)論

提出一種基于構(gòu)件適應(yīng)與協(xié)同的智能家居平臺(tái)邏輯模型,對(duì)平臺(tái)及各構(gòu)件進(jìn)行了形式化描述與建模,并結(jié)合平臺(tái)功能需求對(duì)模型性質(zhì)進(jìn)行了分析與驗(yàn)證。實(shí)驗(yàn)表明,在本模型下平臺(tái)構(gòu)件的適應(yīng)與協(xié)同過(guò)程滿足不死鎖、不中止、不發(fā)散的必要性質(zhì),且在并行處理多用戶請(qǐng)求的條件下能夠?qū)崿F(xiàn)數(shù)據(jù)一致性與操作有效性,對(duì)智能家居平臺(tái)的研發(fā)與驗(yàn)證有一定意義。下一步的工作中將在模型中加入時(shí)鐘控制,建立實(shí)時(shí)模型,更加準(zhǔn)確地模擬系統(tǒng)工作狀態(tài),進(jìn)一步提出平臺(tái)研發(fā)與驗(yàn)證的意見(jiàn)和建議。

參考文獻(xiàn)：

[2]APPLE,Inc.Introducing homekit[EB/OL].[2014-11-18].https:∥developer.apple.com/homekit/.

[3]APPLE,Inc.HomeKit user interface guidelines[EB/OL].[2014-11-18].https:∥developer.apple.com/homekit/ui-guidelines/.

[4]謝兄,張維石.構(gòu)件適應(yīng)和組裝的形式化語(yǔ)義描述[J].計(jì)算機(jī)工程與應(yīng)用,2007,43(21):36-39.

[5]MOREL B,ALEXANDER P.Aslicingapproach for parallel component adaptation technical report ITTC-FY2003-TR-29120-01[R].Information and Telecommunications Technology Center,University of Kansas,2002.

[6]SUN Jun,LIU Yang,SONG Jin,et al.Modeling and verifying hierarchical real-time systems using stateful timed CSP[J].The ACM Transactions on Software Engineering and Methodology,2013,22(1):1-29.

[7]LIU Yang.User Manual[EB/OL].[2013-05-17].http:∥pat.sce.ntu.edu.sg/wp-source/resources/OnlineHelp/htm/index.htm.

[8]SUN Jun,LIU Yang，DONG Jinsong.Model checking CSP revisited:introducing a process analysis toolkit[C]∥MARGARIA T,STEFFEN B.The Third International Symposium on Leveraging Applications of Formal Methods,Verification and Validation,Porto Sani,Greece.Berlin Heidelberg:Springer,2008:307-322.

[9]SUN Jun,LIU Yang,DONG Jinsong,et al.PAT:towards flexible verification under fairness[C]∥BOUAJJANI A,MALER O.The 21th International Conference on Computer Aided Verification (CAV 2009).Grenoble,France,2009,5643:709-714.

[10]王栩凱.智能家居系統(tǒng)規(guī)則沖突檢測(cè)機(jī)制的研究與實(shí)現(xiàn)[D].北京郵電大學(xué),2015.

[11]張星.基于Petri網(wǎng)的智能家居原型系統(tǒng)的設(shè)計(jì)與分析[D].華東理工大學(xué),2013.

[12]龐泳,李光明.基于ZigBee的智能家居系統(tǒng)改進(jìn)研究[J]. 計(jì)算機(jī)工程與設(shè)計(jì),2014,35(5):1547-1550.

[13]陳瑋,秦會(huì)斌,曹曙光,等.基于Android平臺(tái)的智能家居系統(tǒng)設(shè)計(jì)[J].電子技術(shù)應(yīng)用,2015,41(10):158-160.

[14]韓江洪.智能家居系統(tǒng)與技術(shù)[M].合肥:合肥工業(yè)大學(xué)出版社,2005.

[15]張協(xié)衍,章兢.基于連續(xù)時(shí)間模型的多智能體系統(tǒng)采樣數(shù)據(jù)一致性[J].自動(dòng)化學(xué)報(bào),2014,40(11):2549-2555.

[16]LAMPORT,LESLIE.The mutual exclusion problem has been solved[J].Communications of the Association for Computing Machinery,1991,34(1):110-119.

[17]謝開(kāi)斌,陳海明,崔莉,等.物聯(lián)網(wǎng)軟件體系結(jié)構(gòu)中的感執(zhí)模型的求精[J].軟件學(xué)報(bào),2014(8):1659-1670.

[18]Gerth R,Peled D,Vardi M Y,et al.Simple on-the-fly automatic verification of linear temporal logic[J].Simple On-the-fly Automatic Verification of Linear Temporal Logic-ResearchGate,1995:3-18.

(編輯：朱倩)

The Formal Analysis of Component Adaptation and Interaction of Frameworks for Smart Home

LI Aiping，MA Junwei，DUAN Liguo

(CollegeofComputerScienceandTechnology,TaiyuanUniversityofTechnology,Taiyuan030024，China)

Abstract:This paper proposed a smart home frameworks model concentrated on components’ adaptation and interaction.Formal description and modeling of frameworks and components were performed.According to the functional requirements,the properties of the model were analyzed and verified.Experimental results show that adaptation and interaction of components have the essential qualities of being deadlock-free, divergence-free and nonterminating.And the model can keep data consistency and operational effectiveness under the condition of processing user requests in parallel.The modeling and verification methods have certain significance in the formal verification and research of smart home frameworks.

Key words:sart home frameworks;component adaptation;component interaction;formal methods

文章編號(hào):1007-9432(2016)02-0212-06

*收稿日期：2015-05-30

基金項(xiàng)目：山西省科技攻關(guān)資助項(xiàng)目(工業(yè)):遺留軟件再工程的研究與實(shí)現(xiàn)(20120321030)；太原理工大學(xué)?？萍及l(fā)展基金資助項(xiàng)目(2012L067)

作者簡(jiǎn)介：李愛(ài)萍(1974-)，女，山西文水人，博士，副教授，主要從事計(jì)算機(jī)應(yīng)用，軟件形式化描述與驗(yàn)證，軟件體系結(jié)構(gòu)等的研究，(E-mail)tyutli@163.com

中圖分類號(hào):TP399

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

DOI：10.16355/j.cnki.issn1007-9432tyut.2016.02.017