智能家居平臺構件適應與協同模型及形式化分析

李愛萍，馬俊偉，段利國

(太原理工大學 計算機科學與技術學院,太原 030024)

?

智能家居平臺構件適應與協同模型及形式化分析

李愛萍，馬俊偉，段利國

(太原理工大學 計算機科學與技術學院,太原 030024)

摘要:以解決智能家居平臺運行過程中的構件適應與協同問題為目的，保證設備獨立性與數據一致性為特點，提出一種基于構件適應與協同的智能家居平臺邏輯模型,對平臺及各構件進行形式化描述與建模,并結合平臺功能需求對模型性質進行分析與驗證。實驗表明,在本模型下平臺構件的適應與協同滿足不死鎖、不中止、不發散的必要性質,且在并行處理多用戶請求的條件下能夠實現數據一致性與操作有效性。本研究對智能家居平臺的研發與驗證有一定意義。

關鍵詞:智能家居平臺;構件適應;構件協同;形式化

智能家居平臺是針對智能家居設備管理的軟件開發框架[1-2]。一般定義智能設備及控制程序的訪問接口、協議及控制方法,將家庭看作一個智能家居設備的集合,通過家庭、房間、區域的概念把這些設備有機地組合起來。在對設備的控制上,硬件設備被定義成提供一個或者多個服務的單元,而這些服務可以被第三方控制程序發現和調用[2-3]。

構件適應是軟件工程中的一個關鍵問題[4-5],是指將部分滿足要求的構件按照合適的適應結構組裝在一起,形成滿足用戶需求的復合構件。智能家居平臺需要將智能設備、控制程序、操作系統等構件復合成為用戶提供服務的綜合系統,各構件的適應與協同就顯得至關重要。而目前國內外在該領域的研究工作較少,且缺乏基于嚴謹數學基礎的形式化研究支持,導致平臺構件適應協同等問題無法進行有效驗證,大大阻礙了智能家居行業的創新與發展。

以解決平臺運行過程中的構件適應與協同問題為目的,保證設備獨立性與數據一致性為特點,提出一種基于構件適應與協同的智能家居平臺邏輯模型,對構件及平臺進行形式化描述與建模,并結合平臺功能需求對模型性質進行分析與驗證,證明了模型的正確性與實用性。

1相關工作

文獻[10]設計了一種智能家居系統規則沖突避免和沖突檢測的方法,它將場景中的用戶、觸發器、環境實體和執行器這四個部分抽取出來,建立UTEA (User-Trigger-Environment-Actuator)形式化的模型;進而定義了多種規則關系和沖突模型,最后設計了沖突檢測算法。但并未對系統本身的性質進行研究,且尚未實現對系統其它關鍵性質如數據一致性等問題的分析驗證。

文獻[11]提出一個智能家居上下文模型,根據智能家居系統自身的需求和上下文感知工作流框架的特點,采用FollowMe框架進行智能家居平臺設計。可在系統投入運行之前對系統的正確性進行驗證,發現系統潛在的漏洞,避免系統投入運行后發生嚴重的錯誤。然而驗證過程結構復雜,容易出現錯誤信號甚至沖突,導致驗證可靠性大打折扣。

文獻[12-13]分別提出了基于ZigBee和Android平臺的智能家居系統。研究重點皆為功能的豐富和性能的優化,并未對系統可靠性、并行處理性質等作出分析,其實驗結果難以令人信服。

2智能家居平臺邏輯模型

智能家居平臺的實際系統結構包括感知層、傳輸層及應用層等[14],本文僅研究應用層上各構件的適應與協同,并以此為目的建立邏輯模型進行形式化分析與驗證。

智能家居平臺的邏輯模型如圖1所示,分為四類構件。

1) 控制程序(Control App)。即用戶使用的第三方應用,它從操作系統的數據容器中獲知當前智能設備的狀態,并通過智能家居開發框架所提供的接口來對智能設備進行控制。

2) 設備控制框架(Accessories Controlling Frameworks)。設備控制框架是智能家居平臺的核心部分,它定義實現智能家居管理的類、關系和方法,實現控制程序對智能設備的控制。操作系統(Operating System)是控制框架的載體,框架方法的實現可能需要調用操作系統的相關接口。另外,實現對設備的控制應至少需要以下兩個大類，

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

b.AccessoryOb表示房屋中一個獨立的智能設備。一個智能設備有且僅有一個AccessoryOb對象與其對應。一個AccessoryOb對象提供一個或多個服務(service),每個Service有多個屬性(characteristics)來表示其狀態。

3) 數據容器(Common Database)。數據容器是操作系統中用于保持數據一致性的數據存儲器。智能設備的狀態信息被存儲在Common Database中,所有控制程序都須從此獲得設備信息。

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

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

3智能家居平臺及構件的形式化描述

借鑒文獻[5]的描述方法,智能家居平臺中每個構件的形式化描述規則如下。

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

Component(inxseq, outyN, outzN)

prex≠Null

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

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

3.1構件形式化模型

3.1.1控制程序構件

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

控制程序構件的輸入參數為房間(Room)、設備(Acc)、服務(Ser)、屬性(Cha)和命令(Cmd),輸出為同一房間、設備及用于控制程序和設備控制框架進行協同的命令(Req)。前置條件為Room屬于房間集合elements(rooms)中的元素,Acc屬于當rooms值等于Room時二元組elements(accessories, rooms)中的元素,其他前置條件的表示方法與含義與其類似。后置條件為Req屬于在Room、Acc、Cmd為確定值時四元組elements (requests, rooms, accessories, commands)中的元素。

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

3.1.2設備控制框架構件

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

輸入為控制程序時:

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是用于設備控制框架與智能設備進行協同的命令。

輸入為智能設備時:

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智能設備構件

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數據容器構件

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

數據容器存儲從設備控制框架輸入的房間和設備信息并進行更新,同時提供控制程序需要的房間設備信息。

3.2智能家居平臺形式化模型

在平臺系統各構件模型已確立的基礎上,按照復合構件構造規則[4]對各構件進行復合,得出智能家居平臺構件適應與協同的整體系統模型。

模型為循環結構,執行過程為:

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

式中：符號‘+’表示構件的順序執行關系,執行語義是依次執行ControlApps、OS1、Accessory、OS2 、Database五個構件,最后再次執行System；*表示0或多次的重復,用于表示平臺對智能設備的多次控制。

智能家居平臺整體模型形式化描述如下:

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模型應用實驗

智能家居平臺應使用戶能夠在搭載平臺的操作系統上通過應用程序控制和配置智能設備,主要實現以下四大功能[3]:

1) 房間設置。用戶能夠創建、命名、調整以及刪除虛擬的房間及房間組合。

2) 用戶管理。具有相關權限的用戶能夠對當前連接在同一家庭中的其他用戶進行管理。

3) 設備的增加與刪減。用戶可以便捷地發現設備并將其添加到相應房間中,也可以快捷地刪除設備。

4) 情景設置。用戶可以對多個設備進行配置,并將其定義為一個“情景”,從而通過對“情景”的控制來方便地調配多個智能設備。

4.1構件協同模型建模

應用實驗以本文提出的形式化模型為基礎,模擬在智能家居平臺模型上并發進行各類功能操作的過程,來檢驗構件協同性質以及并行處理性質。模擬工具為形式化進程分析工具PAT平臺,使用語言為CSP#。

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

4.1.1房間設置功能過程建模

對該功能所要完成的任務進行分析,用戶首先通過Cs()進程從數據容器中獲知房間當前情況,隨后發出配置請求事件requestA。實現對Room的控制。HomeDelegate協議實現從應用程序到平臺的通信。homeoperateR事件表示對請求進行的處理,最后調用Cs()在Common Database中寫入最新配置信息,同時通過協議將結果返回用戶程序。該功能行為流程用CSP#建模表示為:

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

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

用戶通過Cs()獲取當前用戶信息,隨后發出用戶管理請求requestB。用戶信息由Home模塊進行處理,因此通過HomeDelegate協議進行傳達。HomeoprateU表示Home模塊收到指令后對用戶進行操作,最后調用Cs()更新信息,同時使用協議將處理結果返回用戶。該功能行為流程用CSP#建模表示為:

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

4.1.3設備增刪功能行為流程表示

用戶調用Cs()后發出設備增刪請求requestC,通過HomeDelegate協議與Home模塊協同,通過homeoprateB操作增刪設備。最后通過Cs()更新信息并通過AccessoryDelegate協議告知用戶結果。該功能行為流程用CSP#建模表示為:

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

4.1.4情景設置功能行為流程表示

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

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

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

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

其中參數i為用戶編號。

最后,模擬N個用戶同時通過智能家居平臺來配置智能家居作為整個系統的進程System()。

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

4.2模型性質的分析與驗證

實驗從構件協同性質和并行處理性質兩方面進行分析與驗證。

4.2.1構件有效適應與協同的性質驗證

在協同性質方面,該行為流程模型所涉及的構件適應與協同應具備不死鎖、不中止、不發散的性質[17]。用CSP#斷言可表示為:

#assert System() deadlockfree;

#assert System() divergencefree;

#assert System() nonterminating.

通過PAT平臺對流程模型進行自動驗證,可以得出構件的適應與協同具備相關性質。

4.2.2模型并行處理性質驗證

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

#define collision (count> 1);

#assert System() |=collision;

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

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

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

在以上五條語句中,首先將用于記錄臨界區用戶數的count參數大于1的情況定義為collision事件,然后聲明斷言驗證System()是否有collision事件出現。若沒有,即驗證不通過,則說明臨界資源不存在用戶數大于1的情況;第三條表示在System()中若發生requestD事件,則接下來必發生accessoryconf事件;第四條中ncs事件為互斥算法中的第一個事件,一個User()中發生兩次該事件則說明其訪問量兩次Common Database,完成了讀和寫的操作;第五條表示發生callback事件且原子操作結束后(Skip),下一個事件是否始終為ncs;若不是,則說明存在其它事件修改數據的潛在風險。

同樣地,使用PAT平臺對流程模型的并行處理性質進行LTL檢測,從結果可以得出模型具有所要驗證的性質。

將本文所提模型的驗證結果與第二節中的相關工作進行比較,可得以下優點:

1) 實現了控制器與智能設備的相對獨立。在本模型中,控制程序與智能設備通過操作系統進行協同,兩者相互獨立。兩個部分的開發者只需遵從系統提供的接口即可進行開發,實現了軟件和硬件端的相對獨立設計與操作。

2) 解決了構件協同中的數據一致性難題。本模型中的數據都儲存在數據容器中,所有操作都需要在其中讀取或寫入數據,保證了對設備進行操作的有效性和安全性等。

3) 實現了設備的聯動操作。由于設備被安排在房間中,因此可以以房間為單位進行從屬設備的統一設置與聯動操作,亦可以以情境為前提進行多個設備的設定。真正實現智能地為用戶服務,而不是單一、復雜地操作設備。

5結論

提出一種基于構件適應與協同的智能家居平臺邏輯模型,對平臺及各構件進行了形式化描述與建模,并結合平臺功能需求對模型性質進行了分析與驗證。實驗表明,在本模型下平臺構件的適應與協同過程滿足不死鎖、不中止、不發散的必要性質,且在并行處理多用戶請求的條件下能夠實現數據一致性與操作有效性,對智能家居平臺的研發與驗證有一定意義。下一步的工作中將在模型中加入時鐘控制,建立實時模型,更加準確地模擬系統工作狀態,進一步提出平臺研發與驗證的意見和建議。

參考文獻：

[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]謝兄,張維石.構件適應和組裝的形式化語義描述[J].計算機工程與應用,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]王栩凱.智能家居系統規則沖突檢測機制的研究與實現[D].北京郵電大學,2015.

[11]張星.基于Petri網的智能家居原型系統的設計與分析[D].華東理工大學,2013.

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

[13]陳瑋,秦會斌,曹曙光,等.基于Android平臺的智能家居系統設計[J].電子技術應用,2015,41(10):158-160.

[14]韓江洪.智能家居系統與技術[M].合肥:合肥工業大學出版社,2005.

[15]張協衍,章兢.基于連續時間模型的多智能體系統采樣數據一致性[J].自動化學報,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]謝開斌,陳海明,崔莉,等.物聯網軟件體系結構中的感執模型的求精[J].軟件學報,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

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

*收稿日期：2015-05-30

基金項目：山西省科技攻關資助項目(工業):遺留軟件再工程的研究與實現(20120321030)；太原理工大學校科技發展基金資助項目(2012L067)

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

中圖分類號:TP399

文獻標識碼:A

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