SSRules:讓智能家居自動化規則更易于編寫和檢查*

王 博,張 昱,耿佳寧,李向陽

1(中國科學技術大學 計算機科學與技術學院 下一代移動計算與數據創新實驗室,安徽 合肥 230027)

2(中國科學院 無線光電通信重點實驗室,安徽 合肥 230027)

隨著物聯網、人工智能與5G 等創新技術驅動的萬物互聯時代的到來,智能家居作為物聯網的重要應用場景之一,正快速進入千家萬戶.智能家居令家庭中的各種設備互聯互通,使用戶實現設備的自動控制、遠程控制和可編程控制,甚至可以根據歷史經驗主動進行自動化服務.根據MarketWatch 發布的報告[1],2016 年,全球智能家居市值556.5 億美元,預計2025 年將達到1 742.4 億美元;同時,中國的智能家居市場也在快速發展,據艾瑞咨詢發布的報告[2],2017 年,中國智能家居市場規模為3 254.7 億元,預計2020 年將達到5 819.3 億元.

為管理種類和規模不斷增加的智能設備,國內外主要領導廠商紛紛推出智能家居平臺,如三星的SmartThings、Amazon 的Alexa、Google 的Home、小米的米家、華為HiLink、云端規則定制平臺IFTTT(“IF This Then That”)[3]等,但它們幾乎不開源并且僅支持相關品牌的設備,限制了用戶所能管控的設備類型及范圍;在開源的智能家居平臺中,基于Python3 的HomeAssistant[4]相對成熟,支持多種操作系統/平臺,集成了IFTTT、GoogleAssistant、MQTT 等產品/功能.這些智能家居平臺將要管控的設備抽象化,通過建立通信標準以及API互聯等方式連接設備和app,采用“觸發-動作編程”(trigger-action programming,簡稱TAP)[5]支持用戶定制規則以指定系統行為.但我們通過多次調研發現:現有TAP 雖足以滿足終端用戶表達簡單的自動化任務,但靈活性不足,難以支持更復雜的用例[5-8].

TAP 規則(如IFTTT)典型地將單個觸發器(trigger)與單個動作(action)關聯起來,例如“如果開始下雨,則關窗”.然而,許多常見行為需要TAP 提供更強的表達能力,如對空調等復雜設備的設定、對門鎖窗戶等安全攸關設備的可靠設定、對夜燈/咖啡機等設備的工作持續時間設定等.為支持用戶的日常需求,不同的智能家居平臺提供不同的支持,例如引入and 連接多個觸發器[5]或者連接多個觸發器和多個動作(如Stringify[9])、用更一般的and/or 組合多個觸發器或多個動作(如HomeAssistant)、增加對觸發器的條件過濾(如Microsoft Flow[10],Zapier[11]和 HomeAssistant)、增加“狀態保持時長”的表達能力(如 SmartRules[12])、支持自定義的事件/服務(如HomeAssistant).各種TAP 擴展豐富了可定制性,但是也存在語義不清晰、編寫復雜等缺陷,不便于用戶使用.

隨著設備數量的增加,其交互也隨之增多,TAP 編程出錯的可能性也會增加.針對這類問題,一些研究如BuildingRules[13],IRuler[14]等提供對某些TAP 編程缺陷的檢測;AutoTap[15]能由線性時序邏輯表達的設備性質合成某些TAP 規則,從而避免用戶直接編寫TAP 規則;AutoTap 和Menshen[16]還提供有限的錯誤修復功能.Brackenbury 等人[17]首次提出和規范可用于TAP 規則觸發器的3 種時序范式Event-Event,State-State 和Event- State,并總結了TAP 可能存在的10 種編程缺陷.

針對智能家居系統面臨的挑戰,本文研究易寫易改、支持多觸發器-多動作、支持狀態保持描述等能力的TAP 規則的表示,然后構建支持這種規則表示的智能家居自動化框架.在TAP 規則的表示方面,觸發器和動作均可以分為(純)狀態型和事件型.本文首先系統分析和總結了各種TAP 編程范式以及它們引起的缺陷種類、原因和檢測/修復現狀,指出了改進TAP 的可能渠道;然后,針對用戶不易分清事件和狀態、不易寫全規則所要考慮的情況組合以及“Event-trigger Event-action”(EE)風格的規則冗長、更改瑣碎等特征,本文提出以“State-trigger State-action”(SS)為基礎構建面向終端用戶易寫易改的、具有豐富表達能力的具體SS 規則范式.在自動化框架構建方面,鑒于HomeAssistant(簡稱HA)相對成熟和開源,支持多種平臺和多種設備及服務集成方式,提供以Event 為核心的寬泛TAP 配置,本文以它為基礎構建支持SS 規則范式的智能家居自動化框架SSRules.針對Brackenbury 等人[17]指出的10 種TAP 缺陷,采用SS 規則范式能天然排除時間窗錯誤和翻轉觸發器這2 種缺陷,完全避免優先級沖突;結合SSRules 的實現策略,能部分解決或消除安全默認偏差、非瞬時動作、重復觸發這3種缺陷,并附帶改善缺少反向動作的缺陷;對于無限循環和不確定時序這兩種缺陷,可以通過模型檢查等方法在規則轉譯成HA 之前避免;SSRules 尚不能解決矛盾的動作這種缺陷.本文的主要貢獻如下:

(1) 系統分析和總結了TAP 編程范式及其編程缺陷,指出了改進TAP 的幾種可能渠道,為我國智能家居領域從業者和軟件研發人員全面了解TAP 編程、缺陷及改進提供了參考資料;

(2) 提出以“State-trigger State-action”為基礎構建易寫易改、有豐富表達力的TAP 編程范式.SS 規則范式以實體-能力抽象為基礎,按動作實體將規則分組、組內按序優先,有效避免了優先級沖突;它區分只讀和可控能力,提供4 種表示歷史狀態的算符,并方便表達在指定狀態/狀態保持下對多種能力的期望;

(3) 引入能表達事件型智能家居執行引擎的獨立“Event-trigger Event-action”(EE)中間表示,基于HA 構建智能家居自動化框架SSRules,它能將SS 規則集合經EE 規則表示轉譯成HA 規則,利用Z3 定理證明器[18]進行觸發事件的篩選和規則化簡,并提供運行時子系統動態感知設備變化和檢查規則執行的有效性;

(4) 實現了智能家居模擬器和SSRules 原型系統.對10 組測試場景,用SS 范式編寫所需的規則條數比轉譯和合并后得到的EE 范式規則數平均減少了60%左右;在模擬實驗環境下,最終生成的HA 規則的運行時檢查都未發現連續異常,并且所記錄到的瞬時異常(小于總檢查次數的0.3%)經查閱日志均為網絡延遲引起.

本文第1 節對現有TAP 編程范式及其引起的缺陷、易用性以及缺陷檢查和修復現狀進行總結.第2 節提出智能家居自動化框架的設計目標,對以HA 為底層基礎、以SS 規則范式為用戶輸入的智能家居自動化框架SSRules 的總體設計進行總結.第3 節詳細討論SS 規則范式的定義及其到HA 規則的轉譯方法.第4 節介紹基于HA 構建的智能家居模擬環境,并在該模擬環境上評估了SSRules 的有效性.第5 節和第6 節分別對相關工作和本文的工作進行總結.

1 TAP 編程范式及缺陷分析

為了滿足終端用戶靈活多樣的需求,大多數智能家居平臺都提供特定的TAP 編程接口用于對智能設備和/或服務進行編程,以定制智能家居系統的行為.本節首先對TAP 編程范式進行了詳細分析,然后系統總結分析了可能導致TAP 缺陷的原因,最后簡要總結改進TAP 的可能渠道.

1.1 TAP編程范式概述

TAP 的表達能力及易寫易改性,對智能家居的推廣和普及至關重要.目前最流行的TAP 接口是IFTTT 在線服務[3],它允許用戶創建程序、自動執行由單個事件觸發的動作,盡管IFTTT 應用廣泛,但其表達能力非常受限.

? 多觸發器、多動作

根據Ur 等人的用戶調查[5],22%的編程行為需要不止一個觸發器或動作,并且觸發器和動作在用戶期望的行為中的組合也更為多樣化.因此,Ur 等人引入“and”連接觸發同一動作的多個事件,例如“IF 窗戶是開的and 在下雨”就觸發“關窗”.Zapier[11]允許將多個動作綁定到一個觸發器;Stringify[9]支持形如“If This and This,Then That and That”的規則.HA[4]還允許定制只要多個觸發器中任意一個被觸發就執行的規則.

? 條件過濾與工作流控制

Zapier 和HA 提供過濾器,支持對觸發器的進一步(and/or)條件過濾.例如:可以在觸發器“接收郵件”后追加過濾器“主題包含X and 來自Y”;MicrosoftFlow[10]不僅提供多步驟的工作流,還提供If-then-else 條件過濾、For-Each 和Do-While 循環等;HA 允許定制包含“call service”動作、自定義事件和自定義觸發器的規則,允許開發者編程實現各種服務.Flow 和HA 提供的這些功能非常強大,但是對終端用戶編程的能力要求高,且缺少對用戶配置的有效性檢查.

? 區分事件(event)與狀態(state)

IFTTT 的“if this then that”易被理解為通用編程中的if-then 語句,而其實際語義卻等價于事件驅動編程.Huang 等人[6]認為:把IFTTT 隱喻成if-then 會有歧義,這種歧義會給用戶帶來困難.由此提出用事件和狀態區分觸發器:事件是瞬時信號(如“溫度降到10°C 以下”),而狀態是可隨時評價的布爾條件(如“在下雨”).Brackenbury等人[17]進一步將動作分成事件(在特定時刻發生,如“關燈”)和狀態(一段時間內設備的期望狀態,如“燈應亮著”)兩類.這種區分事件和狀態的TAP 看似消除了一些歧義,潛在簡化了系統實現中對TAP 規則的理解,但是研究表明:終端用戶往往很難清晰區分事件和狀態[6],且它們的組合又引出新問題.

? 事件和狀態的組合

事件和狀態在組合時有以下語義:多個狀態si的合取是另一個狀態s,僅當每個si為真時s 為真;狀態s 與事件e 的合取是在s為真時e 同時發生的另一個事件e′;兩個事件e1和e2的合取是與e1和e2同時發生的另一個事件.然而在智能家居系統中,“事件同時發生”無論是理論還是實際都不太可能發生.Brackenbury 等人[17]提出了3 種多觸發器組合的時序范式:Event-Event,Event-State 和State-State,并將它們與動作組合成表1 所示的4 類TAP 規則.其中:Event-Event 時序范式引入 WITHIN 時間窗口子句來描述不能同時發生的事件,并提供AFTERWARDS 指定事件次序;Event-State 時序范式將觸發器限制為一個帶若干狀態的事件.這兩類觸發器均觸發事件型動作,也是真實智能家居系統主要采取的方式.State-State 觸發器范式組合多個狀態并且狀態會在一段時間內滿足,故自然地觸發狀態動作;考慮到影響同一設備的多條規則的多個狀態可能同時為真(如控制空調的模式),故State-State→State 范式需要包含優先級來解決沖突.此外,對于少數不能直接表示為狀態型的離散事件動作(如“記錄日志”),State-State 時序范式會觸發事件動作.

? 狀態保持性描述

Huang 等人[6]將動作分成瞬時動作(如“發郵件”)、在固定時間完成的動作(如“沖泡咖啡”)、包含改變狀態的持續性動作(如“開燈”),這給智能家居系統提出了描述和實現狀態保持特性的需求.SmartRules 提供“狀態保持”的表達,可以創建“如果門開著有5 分鐘就通知”之類的動作.HA 提供的trigger 可以定時,雖然其action 沒有直接提供保持時長的表示方法,但是它提供的callservice 動作潛在允許開發者編寫處理狀態保持時長等服務的能力,因此也可以實現類似狀態保持的表達.

Table 1 Four kinds of TAP rules defined by Brackenbury et al.and examples表1 Brackenbury 等人定義的4 類TAP 規則范式以及規則舉例

1.2 TAP規則的缺陷分析

用戶在編寫TAP 規則時很容易出錯,原因在于智能家居設備眾多、用戶期望的行為復雜多樣、智能家居設備之間存在大量的交互[19],單個設備會直接或間接影響到其他設備.人的行為也會影響設備狀態,而人的即使看似簡單的行為也可能會引起背后復雜的設備行為;且人的行為與需求并非一成不變,在不同的場景需求下,很可能會造成對已有規則的破壞[20].由于智能家居的用戶通常缺乏編程相關的訓練,為降低編程門檻,TAP 過分簡化了操作界面[6],從而使程序的表達能力變差,這進一步惡化了TAP 對復雜行為的可解釋性.

Brackenbury 等人[17]通過用戶調查,總結出可能出現在TAP 的10 種缺陷,包括:

(1) 4 種缺陷已被發現且詳細討論

① 優先級沖突(priority conflict),僅在采用State-State→State 時需要對作用于同一設備的多條規則進行優 先級排序,而用戶往往難以按自己的意圖正確設置規則優先級[21].這種缺陷已被TAP 文獻廣泛討 論[7,13,22-24],可以通過靜態分析來檢測;

② 安全默認偏差(secure-default bias)發生在用戶默認系統處在安全狀態[21](例如夜間鎖住窗口),但廣泛部 署的Event–State 設備沒有默認狀態,Yarosh 等人詳細討論了門鎖的這種缺陷[21];

③ 非瞬時動作(extended action)源于動作發生在一段時間而不是瞬時的(如沖泡咖啡);

④ 缺少反向動作(missing reversal)發生在用戶創建了一條執行某動作的規則而沒有寫撤銷該動作的規則 時,例如寫了“IF 進客廳 THEN 開燈”但忘寫離開關燈的規則,但用戶可能認為系統會自動關燈[6,21].

Huang 等人[6]詳細討論了缺陷③和缺陷④,并對系統接口提出改進建議.缺陷④可以通過靜態分析檢測,但不總能被修復.

(2) 3 種缺陷被提及

⑤ 無限循環(infinite loop)的原因是規則相互觸發,這種缺陷在機器人終端用戶編程中常被遇到[6];

⑥ 重復觸發(repeated triggering)指用戶希望規則僅觸發一次,但卻觸發多次.這種缺陷主要出現在State- State 范式下因狀態觸發器持續為真導致規則觸發多次.Cao 等人[25]在mashup 編程工作中提及了這種 缺陷;

⑦ 不確定的時序(nondeterministic timing)是由于系統處理同時發生的觸發器的順序不確定而導致.Huang 等人[6]簡要討論了TAP 中存在的這種缺陷.

這3 種缺陷均可以通過靜態分析來檢測,但是實際系統無法鑒別重復觸發是否是用戶的有意行為.缺陷⑤和缺陷⑦還可以通過動態分析檢測.

(3) TAP 新增缺陷

⑧ 矛盾的動作(contradictory action)指的是長周期內在矛盾的動作間無限循環(例如加熱和冷卻之間不斷 交替);

⑨ 時間窗錯誤(time-window fallacy)是當用戶在編寫Event-Event 范式的規則時忘指定時間窗時導致;

⑩ 翻轉觸發器(flipped triggers)是因用戶難以指定觸發器中哪部分是事件哪部分是狀態而導致的.這種缺 陷在靜態或動態分析中都很難檢測到.

表2 總結了上述10 種缺陷的原因、引起缺陷的TAP 編程范式、缺陷檢查或修復方法.

Table 2 Causes and detection of various bugs in TAP rules表2 各種TAP 缺陷的起因與可檢測性

10 種缺陷中,第①種、第②種、第④種、第⑨種、第⑩種歸結為與用戶預期不一樣,第③種、第⑦種為時序缺陷,剩余3 種為控制流缺陷.表中第3 列的“All”表示表1 中的4 類TAP 規則都可能引起這種缺陷.從中可見:第①種和第③種這兩種缺陷僅存在于純狀態觸發器的TAP 編程中,而第⑨種、第⑩種僅存在于含事件的觸發器的TAP 編程中.Brackenbury 等人[17]對這10 種缺陷的進一步用戶調查表明:相比Event-State,問卷參與者使用State-State 能寫得更正確,而使用Event-Event 則正確性要差些.

1.3 改進TAP的可能渠道

現有的TAP 平臺尚未能充分滿足用戶需求,在實際運行中容易出現缺陷導致系統出錯.綜合分析現有智能家居系統及學術研究成果,以下給出了幾種改進TAP、減少編程缺陷的渠道.

(1) TAP 編程范式

實際智能家居系統大都基于Event-State→Event 規則范式來實現.相比于使用事件型觸發器進行TAP 編程,使用純狀態觸發器更容易讓終端用戶正確表達意圖.即使使用相同的觸發器范型和動作范型,不同的TAP 規則結構仍會影響TAP 編程的表達能力、易用性和編程缺陷.現有解決方案中,除了直接讓終端用戶寫TAP 規則,研究人員還提出了不同的實現方案,如:

? AutoTap[15]允許用戶輸入設備的安全性質(可轉化為線性時序邏輯公式)而由系統合成Event-State→ Event 規則,從而減少最終規則的缺陷,但是存在合成效率較低、難以適用較多設備、安全性質不適合表達需求細節等不足;

? Zave 等人[24]提出讓用戶對設備按不同目的(如安全性、節能等)分別描述需求特征,然后手工為特征建立狀態機,并根據它設計運行時的特征組合機制來實時控制執行器.如何由非形式的特征描述建立FSM 以及解決特征沖突(或稱特征交互)是其中的難點,該方法目前只支持對幾種設備的人工建模且僅支持“值設置”動作.

(2) TAP 規則的檢查與修復

改進TAP 編程范式不可能完全消除編程缺陷,TAP 平臺仍需要一些額外的工具或方法來檢查TAP 規則的有效性,并嘗試修復規則.現有的方法大都針對Event-State→Event 規則進行靜態檢查(如IRuler[14],AutoTap[15],MenShen[16,22])、動態檢查(IoTGuard[19])或規則修復(AutoTap,MenShen,TrigGen[26]),僅有極個別方案是基于狀態觸發的[21,24],這很大程度上是因為實際的智能家居系統是按事件驅動方式來運行的.表3 從多種維度比較了已有方法,可以看出,Event-State→Event 規則的修復存在搜索修復策略低效以及在不清楚用戶意圖的情況下仍需用戶決策等局限性.而隨著設備數增多,這類規則及修復邏輯的可讀/可理解性也在下降.此外,由于網絡延遲/重放攻擊等,也會使基于EE 的智能家居系統執行不期望的動作.Wang 等人[27]提出,通過分析日志中事件間的依賴來事后追因.

Table 3 Existing work towards bugsin smart home rules表3 關于智能家居用戶規則缺陷的相關工作

(3) 智能家居系統的實現

對TAP 規則的靜態檢測和修復可以在規則實際運行前識別出部分規則缺陷,并嘗試手工/自動修復.但是如表2 第4 列所說,還有許多缺陷是靜態無法檢測,或是由于難以判斷用戶意圖從而無法確定缺陷是否存在.因此,智能家居系統在實現時需要提供:

1) 給用戶更多的提示和警告:針對那些潛在有歧義、有沖突或已做動作不會被自動撤銷等情況,系統要給出用戶易于理解的提示或警告;

2) 提供不易讓用戶混淆的選項供用戶選擇;

3) 提供運行時日志的記錄,需要權衡日志的存儲量與事后推理的便利性;

4) 支持和提供含義更明確的頂層trigger-action 結構,等等.

2 SSRules 智能家居系統總體設計

為使終端用戶易于編程,本文重點探索狀態觸發器-狀態動作的TAP 編程范式(簡稱SS 規則范式),并基于HA 構建了支持SS 規則范式輸入的SSRules 系統.SSRules 在不改變HA 規則執行引擎的基礎上,擴展提供更易被用戶理解和掌握的規則表達方式以及對應的規則轉譯器.雖然SS 規則范式尚不支持表達無狀態或難以抽象出狀態的事件動作,但由于這類動作所占比重小、用戶需求低,因此,SSRules 可以支持用戶的絕大多數需求.未來可以設計專門的機制,將這些無狀態的事件動作加入到SSRules 系統中.本節首先簡要介紹SSRules 的設計目標,然后分析HA 的關鍵特征,最后給出SSRules 總體架構以及所引入的Entity-Capability 抽象.

2.1 設計目標

智能家居正進入尋常百姓家,為了讓SSRules 滿足用戶的不同需求,現階段至少應圍繞如下目標設計.

G1.易寫易改.針對用戶調查[5,6,15,17]反映的TAP 規則編寫和修改的問題,SSRules 應提供讓無編程經驗的終端用戶快速學習并正確使用的編程范式,方便表達所期望的智能家居系統性質,且在需求變化時容易修改;

G2.可管可控.SSRules 系統應能提供按終端用戶的有效需求對來自不同廠商的設備實時監測與控制,感知系統中動態加入和退出的管控對象,而不能只支持特定廠商的設備和僅提供極其有限的監測能力;

G3.異常檢測.智能家居系統的可靠性受限于網絡、設備故障等不定因素,而用戶希望系統提供實時反饋以及對系統更多的控制感.因此,系統需要能夠幫助用戶監視運行狀況,并將異常信息反饋給用戶;

G4.協調需求.作用于同一設備的多種需求存在沖突,是智能家居中的常見現象.系統要提供簡單的處理方式,便于用戶協調好同一設備存在沖突的多種需求.例如希望燈在夜間關閉,但是有人經過則應以較低亮度打開一段時間,如果遇到緊急情況(如廚房著火)則應當完全打開;

G5.多方信息.智能家居系統的功能邊界應當不限于家庭的物理空間.系統不僅要能夠處理家庭中存在的物理設備,也要能處理虛擬傳感器和虛擬的設備,如情景模式、天氣、時鐘等.

2.2 HomeAssistant(HA)

本文的研究重點為探索TAP 編程的表示及其在現有執行引擎的實現,同時提供一定的規則有效性檢查功能.因此,為更有效地實現G2 和G5 涉及的目標,SSRules 需要選擇成熟開源的智能家居執行引擎來實現與各種(虛擬)設備的連接、實時監控、動態感知以及自動化管理等.

在開源智能家居系統中,HA 是基于Python 的成熟智能家居開源系統,能部署在任何能運行Python 3 的機器上,從樹莓派到網絡存儲,還可以使用Docker 部署到其他系統上.它主要根據automations.yaml 等配置文件實現集中化的智能家居設備管理,設備支持度高,具有自動化、群組化、UI 客制化等高度定制化設置;同時,其開發者數量、版本更新速度在所有開源項目中也都屬于佼佼者.因此,我們最終選取HA 作為SSRules 的執行引擎.

? 靈活的集成方式

在HA 中,物理設備和虛擬設備均被抽象為實體,帶有狀態的實體可以與狀態對象關聯.天氣、太陽角度等均為HA 預置的虛擬實體;通過用戶自定義或第三方集成,還可以實現如模式開關、空氣質量、用戶位置等虛擬傳感器和動作器.實體上可以執行的動作被抽象為服務調用,除了HA 自帶的值變化事件、服務調用事件等事件類型,第三方集成也能夠發布其他自定義的事件.采用HA 可以自然地支持目標G5.

? 設備的動態管理

HA 接入設備的方式之一是MQTT Discovery,它提供對基于MQTT(message queuing telemetry transport)協議通信的設備的自動發現、配置和移除.MQTT 協議是一種基于TCP 的發布訂閱協議,在物聯網通信中使用較多.設備接入HA 時,每個設備只需按照HA 指定的格式配置其MQTT 通信模塊,HA 即可間接從MQTT 代理獲得配置信息并完成配置流程.若設備需要移除,則它可以更新狀態信息將自己移除,也可以由HA 根據超時設置自動移除.因此,HA 提供實現G2 的基礎,SSRules 需要主動與HA 交互真正達到G2.

? 高自由度的輸入

HA 的規則輸入語言為Trigger-Condition-Action(即Event-State→Event)范式,單規則中可以含有多觸發器、多動作.動作不僅可以是與設備相關的服務調用,也可以是自定義的事件觸發和狀態值寫入、HTTP 接口調用等,自由度很高.但是HA 的自動化規則的編寫非常繁瑣,用戶難以使用其描述有優先級的功能需求,并且用戶自行推理編寫極易遺漏或寫錯.此外,由于HA 的實體狀態和服務調用之間的松耦合,HA 提供運行時異常檢查極其有限.HA 在G1,G3 和G4 方面較弱,因此,這也是SSRules 要重點解決的問題.

2.3 SSRules系統總體架構

SSRules 系統總體架構如圖1 所示.整個系統通過HA 提供的接口與智能家居設備連接,包括通過MQTT 代理連接智能家居真實設備或模擬器.系統由離線的轉譯器子系統和在線的SSRules 運行時子系統組成:前者提供終端用戶輸入的SS 規則到HA 規則的轉譯,后者提供HA 抽象信息的獲取和規則執行的有效性檢查.SSRules引入Entity-Capability 抽象(見第2.4 節)來描述智能家居系統所能管控的設備(實體)及可管控的內容(能力),用戶輸入的SS 規則最終被SSRules 轉化為HA 規則注入到HA 的配置文件并得以執行.

Fig.1 Overall structure of SSRules圖1 SSRules 系統總體架構

? 抽象信息獲取

SSRules 需要HA 中的實體、狀態、服務的抽象信息用于SS 規則的轉譯和異常檢測,這些信息由SSRules運行時子系統的抽象信息獲取模塊來提取和更新.該模塊定期從HA 更新實體信息并檢測變化情況,獲取設備的動態信息(加入或離開),生成SSRules 所需的最新實體-能力抽象信息和動作翻譯信息.

? 規則轉換流程

SSRules 的用戶交互模塊根據實體-能力抽象信息將用戶輸入規則所需的信息以用戶友好的方式呈現在前端界面中.用戶完成編輯后,用戶交互模塊根據用戶的輸入生成SS 規則文件.接著,SSRules 運行時系統會調用可離線運行的轉譯器將SS 規則轉譯成HA 規則,再將其更新到HA 的automations.yml 中.

? 異常檢測設計

當由SS 規則翻譯得到HA 規則并開始執行之后,規則執行有效性檢查模塊會從HA 獲取所關心的狀態變化事件,定期獲取全部實體的狀態,檢查實體狀態及其狀態變化是否符合SS 規則的描述,并將因網絡/設備故障等問題導致的設備狀態與SS 規則描述不相符等情況進行告警以及寫入日志.

2.4 Entity-Capability抽象

一個智能家居系統所管理的設備可以包括真實物理設備(如空調)、虛擬設備(如天氣、時鐘等),還可以是人.SSRules 系統使用實體-能力抽象(entity-capability abstraction)來描述智能家居系統中各種設備的可感知和/ 或可控制的能力,記為,ND為實體總數.每個設備抽象為一個實體E(entity),每個實體由其ID e、一組能力C(capability)以及描述各能力狀態之間轉移關系的狀態機M組成,即E=(e,C,M).

? 能力

每種能力表示單個可變化的只讀或者可控屬性.表4 列出了幾種常見智能家居設備及其能力.每種能力可 表示為一個四元組(c,k,ro,J),其中:c是該能力在實體內的唯一標識;k表示該能力的狀態值類型,可以是二值 (binary)/多值(set)/實數(numeric)等類型之一(實數可以細分成子界類型或實數區間等,本文為簡便起見不作區 分);布爾量ro為真表示能力是只讀的、為假表示是可控的;J表示一組關聯的命令序列,其中每個元素是要執行 的命令代號.

? 狀態機

每個實體的狀態機由該實體每種能力c 的狀態機組成:Mc=(Vc,Tc),其中,Vc是能力c 的狀態值集合,Tc是狀 態值之間的轉移函數.

Table 4 Examples of entities and their capabilities表4 實體及能力舉例

在缺省的Mc中,任意兩個狀態值之間存在條件為True 的轉移(即無條件狀態轉移);若c 可控,則存在無條件 動作,它可觸發任意兩個狀態值之間的狀態轉移.SSRules 系統會提供初始的Mc配置文件,其中提供部分常用 設備能力及其狀態轉移描述,用戶也可以根據需要添加某個設備或者某一類設備的Mc補充信息.

根據c 的Mc抽象,可以進一步檢測動作的執行前提,或者判斷事件的可能性.例如,假設電扇和咖啡機的能力狀態機如圖2 所示:① 電扇的c2(風速)只有在其c1(開關)的取值為開時才可以接受改變風速的動作;② 咖啡機的咖啡狀態僅在咖啡機的c1(開關)取值為開時才能從未準備好進入準備好狀態.

Fig.2 The state machines for each capability of the fan and coffee machine圖2 電扇和咖啡機的能力狀態機

3 SSRules 編程范式及其到HA 規則的翻譯

本節首先分析以狀態觸發器-狀態動作(SS)風格設計SSRules 編程范式的可行性;然后給出SSRules 提供給終端用戶使用的SS 規則范式的定義,分析它在應對表2 所列的10 種TAP 缺陷的能力;接著分析轉譯器面對的主要問題,并引入EE 中間范式作為SS 規則到HA 規則轉換的橋梁;最后介紹SS 到EE 轉譯的關鍵算法.

3.1 SS范式的引入

由第1 節可知:終端用戶不太能區分事件和狀態,并且用戶使用State-State 時序范式會比使用含Event 觸發器的范式更易寫對規則.為此,我們以狀態為基礎,通過規則分組、自動優先級等改進措施(詳見第3.2 節)來提供“State-trigger State-action”編程范式,簡稱SS 范式.

? SS 范式的易寫易改性

SS 范式可以較為簡潔地表達用戶日常常見需求;并且和Event-State→Event 相比,SS 范式寫出的規則容易隨需求的變更和細化進行修改.為了更清晰地表述這兩種范式的區別,表5 給出了分別用兩種范式描述夜燈開關的規則,其中,模式是HA 提供的虛擬傳感器,有回家模式和離家模式兩種取值.在SS 范式下,作用于夜燈的3條規則均作為子句按序置于“ FOR 夜燈”語句中,每個子句形如“EXPECT A [WHILE B]”,表示當B 成立(或永真)時,期望A 中各能力為指定的值;對于同一實體的多個EXPECT,SSRules 按從前往后以第一個WHILE 條件成立的EXPECT 子句所指定的期望狀態為準.然而,當用Event-State→Event 表示時,為了正確表達所列出的幾種情況的狀態保持和它們之間的轉移關系,需要寫出9 條規則來細分情況.假設用戶用SS 范式先寫了后2 條規則,運轉一段時間后他又添加第1 條保證離家模式下夜燈總是關閉的需求,在SS 范式下,這種添加是簡單的;但是若使用Event-State→Event 達到相同目的,則需要在原先第3 條~第6 條、第8 條、第9 條這6 條規則基礎之上新增3 條規則,并修改原先的規則細節(修改部分用粗體字表示),這樣的編寫和修改非?，嵥?、易錯.

Table 5 Example of comparing SS rules and Event-State→Event rules表5 SS 范式與Event-State→Event 范式的比較舉例

? SS 范式的局限

SS 范式能表達大多數智能家居的場景需求,但是無法表達無狀態或者難以抽象出狀態的事件和動作(如無狀態按鈕、記錄日志等).對于這類需求,目前仍需編寫Event-State→Event 規則.因此,SSRules 將SS 范式轉譯為Event-State→Event,并允許兩種范式共存.未來可以擴展降低這類需求編程難度的具體范式.

3.2 SS范式的定義

表6 的左部列出了SSRules 系統支持的SS 范式的抽象語法,其中:FOR 語句集結同一動作實體的所有規則,且約定組內靠前的規則優先級更高;每條規則(ssrule)包含在WHILE 子句指定的條件成立時,對該實體全部或部分能力的期望狀態;多條規則按從前到后的次序、以第1 條滿足WHILE 條件的規則中的EXPECT 子句來設置期望的實體能力狀態;一般地,無 WHILE 子句的規則放在最后作為安全默認.Condition 中的“entityID.capName op value”,“historyOp timeperiod entityID.capName value”分別表示當前狀態和歷史狀態型原子判斷,其中,歷史狀態運算符historyOp 的4 種可能取值的含義舉例如下.

? “WITHIN 5 分鐘電扇.開關關”表示電扇的開關在5 分鐘內曾經處于關閉狀態,則該原子判斷為真;

? “!WITHIN 5 分鐘電扇.開關關”表示電扇的開關在5 分鐘內不曾處于關閉狀態,則該原子判斷為真;

? “STAY 5 分鐘電扇.開關開”表示電扇的開關在5 分鐘內持續處于開啟狀態,則該原子判斷為真;

? “!STAY 5 分鐘電扇.開關關”表示電扇的開關在5 分鐘內未一直處于開啟狀態,則該原子判斷為真.

Table 6 Abstract syntax of paradigms of SS rules and EE rules used in SSRules表6 SSRules 系統使用的SS 范式和EE 范式的抽象語法

3.3 SS范式的缺陷避免能力分析

SS 范式天然地排除了表2 中所列的缺陷⑨、缺陷⑩這兩種缺陷.對于在使用State-State 時序范式時可能存在的缺陷①~缺陷⑧這8 種缺陷,SS 范式的表示機制能完全避免缺陷①優先級沖突;SS 范式的表示及轉譯機制能部分解決或消除缺陷②安全默認偏差、缺陷③非瞬時動作、缺陷⑥重復觸發,其附帶效果可以輔助改善缺陷④缺少反向動作;對于缺陷⑤無限循環、缺陷⑦不確定時序等缺陷的檢測,可以通過模型檢查等方法在規則轉譯之前避免;由于難以提供通用的鑒別何謂矛盾的機制,因而SSRules 不能解決缺陷⑧矛盾的動作.下面分別討論SS 范式應對缺陷①~缺陷③和缺陷⑥的措施.

(1) “按動作實體將規則分組、組內規則有序”可完全避免缺陷①優先級沖突

用戶只需移動規則在組內的相對位置,免除顯式設置優先級數值的困難.由于同一動作實體的各規則優先級不同,故無缺陷①(示例見3.1 節).

(2) “將配置的安全默認規則自動作為動作實體的最低優先級規則”可輔助消除缺陷②安全默認偏差

SSRules 提供可配的安全默認設置文件,其中的條目形如“實體/實體類ssrule”可描述指定實體或實體類的默認期望狀態,SSRules 會自動將其追加到相應實體的規則集尾部,作為最低優先級規則.例如針對門鎖可以配置默認安全規則“EXPECT (狀態,鎖定)”,則用戶只需描述其他需求,如:

FOR 門鎖 EXPECT (狀態,未鎖定) WHILE 人體傳感器.狀態==激活 [AND 其他安全條件]

而SSRules 會自動在尾部追加“EXPECT (狀態,鎖定)”.只要人體傳感器不再激活,SSRules 就會按最后一條無條件子句的期望狀態將門鎖鎖定.這種做法消除缺陷②的前提是要正確配置安全默認文件.

如果用戶希望在人體傳感器激活后2 分鐘內均保持門鎖解鎖,可使用SS 范式提供的歷史狀態判斷:

FOR 門鎖 EXPECT (狀態,未鎖定) WHILE WITHIN 2 分鐘人體傳感器.狀態激活 [AND 其他安全條件]

(3) “通過避免用戶直接編寫動作”可避免缺陷③非瞬時動作和缺陷⑥重復觸發

在SSRules 中,狀態轉移所需要的動作的執行前提被描述在實體-能力抽象信息中,用戶只能選擇期望的狀態,而無法寫出有缺陷的程序造成對非瞬時動作的多次觸發動作而進入不期望的狀態.例如:針對沖泡咖啡這樣的非瞬時動作,如果主人希望每天7:00 讓咖啡機工作,且咖啡機工作完成后自動關閉,7:00~7:20 之外的時間不開啟咖啡機,則用SS 范式編寫的規則為:

FOR 咖啡機

EXPECT (開關,開) WHILE 時鐘.時間>7:00 AND 時鐘.時間<7:20 AND 咖啡機.咖啡狀態==未準備好

EXPECT (開關,關)

當咖啡機開啟后,即使咖啡未準備好,SSRules 轉譯后的HA 規則也保證不會再出現開啟動作.而用戶倘若用State-State→Event 范式,容易寫出如下有缺陷的規則,造成咖啡機多次啟動:

IF 咖啡未準備好 AND 時間處于7:00~7:20 之間 THEN 啟動咖啡機

對于重復觸發缺陷,能夠用SS 范式表達的規則可以用上述類似的機制來避免;而不能夠用SS 范式表達的規則,仍需要使用Event-State→Event 或者Event-Event→Event 范式來寫(未來將對此提供更直觀的編程方式).

3.4 轉譯器面對的問題及EE中間范式的引入

? 轉譯器面對的問題

如果要在一個僅支持Event-State→Event 范式的智能家居系統上實現對SS 范式規則的支持,需要將智能家居系統狀態之間的轉移和狀態轉移帶來的新的狀態設定與智能家居系統所支持的事件和動作關聯起來,并且要盡可能避免重復觸發、非瞬時動作等缺陷.這一翻譯過程應該對用戶不可見,是由系統自動完成的.此外,為了從翻譯的主要算法中排除HA 規則描述的瑣碎細節,以及讓算法一般化以支持到其他平臺的移植,SSRules 引入了EE 中間范式(基于Event-State→Event).從而:轉譯器的第1 階段,SS→EE 的翻譯可以避開HA 的語法及實現細節,重點是基于同一套實體-能力抽象將SS 范式表示的功能需求轉化為EE 范式所表示的具體做法;而第2 階段,EE→HA 的翻譯則只需從較為抽象的EE 規則根據HA 的事件/條件描述方式、動作對應表,生成HA 所需的規則細節即可.

? EE 中間范式

表6 的右部列出了SSRules 系統轉譯中使用的EE 中間范式的抽象語法,其主要特點為:一條規則可以含有多個觸發事件(event)、條件過濾(condition)和多個按順序執行的動作(eeAction).event 包括狀態值變化事件“entityID.capName FROM range TO range”和狀態保持事件“entityID.capName STAYON value REACH timeperiod”:前者表示給定實體能力的取值從一個值集變遷到另一個值集,后者表示指定的實體能力保持給定值value 的時間長達timeperiod 時觸發該事件.目前,SSRules 僅對二值類型的能力提供狀態保持事件.EE 范式中條件過濾condition 的定義與SS 范式一樣.

? EE 規則到HA 規則的轉譯

EE 規則到HA 規則的翻譯是一一對應的,EE 規則的狀態值變化事件可以對應到HA 的state_changed 事件和在HA 規則的condition 中對事件數據中的old_state 和new_state 的限制條件.EE 規則中的狀態保持事件可以轉譯為在HA 中的延時執行和自定義事件觸發.EE 規則中的條件表達式可以對應到HA 條件表達式中的相同樹形結構.EE 規則中,實體能力的取值對應到HA 規則中的狀態對象state 或者狀態對象attribute 中的附加狀態;EE 規則中,對實體能力的歷史狀態判斷被對應到HA 規則中的自定義狀態對象取值判斷;EE 規則中的一個或多個動作被單個或組合對應到HA 中無參或帶參的服務調用.

3.5 SS規則集與EE規則集的符號表示與一些定義

為了方便后文的說明和理解,我們引入表7 中的符號以及幾個基本概念,這些符號和表6 定義的語法結構 一一對應.例如:GS對應于語法定義中的一個ssrulesGroup,RS對應于一個ssrule,RS中的C和X分別對應于 WHILE 子句中的條件表達式和EXPECT 子句中的期望狀態組.wt 和st 分別表示“WITHIN”和“STAY”.

Table 7 Symbolic representation of SS ruleset and EE ruleset表7 SS 規則集合和EE 規則集合的符號表示

對于一個由ND個實體組成的智能家居系統,每個由三元組(e,C,M)描述.在某個時刻下,W的系統狀態記為σ,它是各實體的各能力到狀態值的映射,即σ(e,c)表示實體e的能力c 在該時刻的狀態值.不論是SS 范式的程序GS,還是EE 范式的程序RE,都是對系統狀態變遷的描述;而轉譯的目標是由GS得到RE,使得GS與RE滿足一致性.在定義一致性之前,我們先定義系統抽象狀態ω,然后定義SS 規則與系統抽象狀態ω的關 系,包括規則在ω下是否激活、規則是否與ω兼容.

定義1(系統抽象狀態).對于規則引擎來說,系統當前狀態σ、當前時刻τnow以及狀態變化軌跡T可抽象為一個三元組ω=(σ,τnow,T),稱之為系統抽象狀態.其中,T=((e1,c1,v1,τ1),,…,(en,cn,vn,τn)),(ei,ci,vi,τi)表示實體ei的能力ci在τi時刻變為vi(i∈{1,…,n}),它只記錄狀態值發生變化的特定實體的特定能力及其新狀態.狀態變化可能由外 部事件引起(如用戶交互、環境變化),也可能由GS或RE執行動作序列引起.每當發生狀態變遷時,都相當于T更新為,其中,τn+1為狀態變遷發生時的τnow.

定義2(規則在系統抽象狀態ω下激活).假設GS=(e,RS)為某動作實體e的SS 規則組,表示RS中期望狀態組均為X的規則子集,當前的系統抽象狀態為ω.稱期望狀態組相同的一組規則SXR 在ω下激活,是指該組內任 意一條規則RS激活;而規則RS在ω下激活,是指在該規則所在的規則組GS內,其前面的規則的條件(對應WHILE子句,即C)在ω下都未滿足,而該規則的條件RS.C滿足.

定義3(規則與系統抽象狀態ω兼容).規則RS與系統抽象狀態ω不兼容,是指在ω下RS激活且RS.X尚不成立;而RS與ω兼容,是指在ω下RS未激活或者RS.X已成立;一組規則與ω兼容,是指組內每條規則與ω都是兼容的;一 組規則與ω不兼容,是指組內存在與ω不兼容的規則.

實際的規則引擎提供的時間戳的精度是有限的.假設系統抽象狀態ω中的時間戳都有最小時間單位(例如1秒),τnow以最小時間單位離散地更新.那么,對于規則集合執行方式的假設如下.

? SS 規則執行假設.假設無時序缺陷的規則組GS的執行方式為:每當發生狀態變化,或者τnow變為新值之后,判斷GS中是否存在與最新的ω不兼容的規則.如果存在這樣的規則RS,說明其對應實體e不滿足RS的期望狀態組X,于是計算e上的需要執行的動作序列A,使得A執行后實體e的狀態符合X;

? EE 規則執行假設.假設無時序缺陷的規則組RE的執行的方式為:設RE中的所有觸發事件可分為狀態 變化事件EI和狀態保持事件EH這兩種類型,每當出現與EI相符的狀態變遷,或者每當τnow的更新觸發了EH中的某個狀態保持事件后,檢查與觸發事件相符的各條規則.如果存在RE,RS.C在ω下成立,則執行 RE.A.

定義4(SS 與EE 的一致性).稱GS與RE一致是指:對于無時序缺陷的GS,RE,在上述規則執行假設下(且不存在超時、執行失敗、規則重疊執行的情形),從與GS兼容的任意系統抽象狀態ω開始,對于同樣的、同時刻的、一次發生一個事件的外部事件序列,GS所產生的狀態變遷序列和RE所產生的狀態變遷序列一致.

與GS一致的RE不唯一,原因在于:① RE中不會被執行的規則不影響一致性;② 一個條件較弱的EE 規則(如一條規則,條件.C為時鐘.狀態==白天)可等價于多個條件更強的EE 規則(如等價于規則和,條件.C和.C分別為“時鐘.狀態==白天 AND 模式.狀態==回家模式”和“時鐘.狀態==白天 AND 模式.狀態==離家模式”);③ 一條EE 規則RE還可以等價于m條EE 規則,滿足.E ;④ 邏輯表達式 有多種等價表述.

3.6 SS規則到EE規則的轉譯

圖3 詳細說明了SS 規則到EE 規則的轉譯算法實現,其中:圖3(a)中的算法1 是總控算法;圖3(b)是相應的 流程圖,轉譯器的輸入分別是左上角的實體-能力抽象信息W和右上角的SS 規則集合GS,輸出是與輸入SS 規則集對應的EE 規則集RE(右下角).

Fig.3 Algorithm and flowchart of translation from SS rules to EE rules圖3 SS 規則到EE 規則轉譯算法與流程圖

轉譯的具體流程為:

? SS 規則集解析器首先會解析用戶輸入的GS,并將解析結果傳給動作序列信息生成模塊;

? 然后,動作序列信息生成模塊會將同一動作實體e的SS 規則序列GS=(e,RS)按照EXPECT 子句作用的期望狀態組分類,期望狀態組X相同的SS 規則組中的多條規則會放在一起處理:一方面,調用ConditionalActionsPairs(e,X,W)(見算法2),計算實體e上所有可能的動作序列Aj和每種動作序列的執行前提Cj,得到二元組集合PairsX={(Cj,Aj) |j∈{1,n}};另一方面,求出與規則組不兼容的條件ΨX(見算法1 第5 行),這是事件發生后、動作執行前系統抽象狀態所應滿足的條件;

? 接下來,事件篩選模塊首先調用CandidateEvents(ΨX,W)(見算法3),根據ΨX生成一組候選事件E(這些事件可能對ΨX的成立與否有影響);然后,對E中的每個事件E調用ShouldRejectEvent(E,ΨX,W)(見算法4),依據缺省的事件篩選策略Pdefault判斷該事件是否要排除掉,即:若E發生后ΨX不成立,則需將E排除;

在轉譯過程中,有多個環節需要與Z3 交互:在轉譯開始之前,轉譯器會根據實體-能力抽象構建Z3 數據類型和Z3 常量,并將對應關系填入Z3-Python 數據結構轉換模塊中的Z3 常量映射表;在轉譯過程中,事件篩選模塊和EE 中間表示生成模塊通過Z3 判定事件的可滿足性;規則合并模塊通過Z3 判斷等價的條件部分,合并觸發事件;可讀性化簡模塊通過Z3 進行表達式化簡以減少條件表達式長度.

下面結合算法2~算法5 詳細介紹動作序列信息生成、事件篩選以及EE 中間表示生成這3 個關鍵模塊.

算法2.“執行前提-動作序列”對集合的生成(ConditionalActionsPairs).

輸入:實體e,期望狀態組X,系統實體-能力抽象W;

輸出:結構如{(C1,A1),…,(Cn,An)}的Pairs,表示實體e 滿足Ci時要達到X需執行Ai.

? 動作序列信息生成模塊

該模塊會針對期望狀態組X相同的SS 規則組,調用算法2 產生可能的動作序列及其執行前提集合PairsX={(Cj,Aj) |j∈{1,n}},并求出與不兼容的條件ΨX(見算法1 第5 行).算法2 的第2 行指出,X投影得到的能力集合XC 中的每個能力都必須是可控的.如第2.4 節所述,可控能力c 的狀態機Mc=(Vc,Tc)中的轉移函數,每個狀態轉移帶有條件C以及要執行的命令J,C中可能會涉及其他實體能力.考慮到實際需求以及處理上的簡便,假設XC 中各能力的狀態轉移條件C中依賴的其他能力遵循部分序關系,算法2 的第3行調用Reorder 函數將XC 中的能力按這種序關系重排得到,這樣在第8 行就可以嘗試按此順序依次檢查動作轉移的可行性.另外,對于中的能力ci,其狀態值域可能是無限的實數,而是有限的,故第5 行的SplitRangeByAction 函數會檢查中到達期望值vi的各個狀態轉移動作J和轉移條件C,將J,C相同的狀態轉移的起始狀態涉及的各狀態值劃分到同一個子集,從而形成的有限子集劃分Setsi,進而可能減少第7 行要處理的初始狀態情形的數目,也能夠減少后續規則合并的運算次數.

下面結合圖4 的例子來解釋.該例子的動作實體為“電扇”,有3 條SS 規則.這些規則按期望狀態組X是否相同分成兩組.以組為例,根據該組的X2“(開關,開)(風速,低)”和圖2 電扇的狀態機,按照算法2 求出到達X2的所有執行前提-動作序列對(圖4 左下方的4 種動作序列).另一方面,該模塊也要輸出不兼容的條件用于稍后的事件篩選,=模式.狀態==回家模式 AND 溫濕度傳感器.溫度 >28°C AND (電扇.開關!=開OR 電扇.風速!=低).

Fig.4 Generating sequences of commands information圖4 動作序列信息生成

? 事件篩選模塊

該模塊先使用算法3 生成候選事件,接著進一步使用算法4,根據系統可能的狀態變遷對事件進行篩選.算法3 主要根據一個執行前要滿足的條件C生成候選事件集,旨在以較低運算成本快速得到較小的待篩選事件集.其中:第2 行分別獲取C中出現的實體能力集合ECs以及原子條件集合Catom,原子條件有當前狀態判斷(e,c,O,v)和歷史狀態判斷(e,c,Oh,t,v)這兩種形式(如表7);第4 行的SplitRangeByCond 則是根據Catom對實體E的能力 c 的狀態值域Vc進行劃分,將對所有原子條件的判斷影響一致的狀態取值劃分到同一個子集,從而將實數類型的事件轉移轉化為了有限情形;第5 行~第7 行分別產生狀態變化事件El和狀態保持事件EH,能夠涵蓋C中出現的原子條件取值變化的情形.對于歷史狀態原子條件(e,c,Oh,t,v),由于只支持二值類型的能力c,在固定e,c,t下,Oh和v最多有8 種組合,我們為之按v的兩種取值產生2 種狀態保持事件,忽略Oh;而被忽略的Oh仍在C中,傳 遞到后續由算法5 產生的EE 規則RE=(E,C,A)中.這種狀態保持事件EH能在狀態遷移中快速知道實體能力保 持狀態的時長,再結合C中的Oh進行狀態保持的可滿足性檢查.

算法3.候選事件生成算法(CandidateEvents).

算法4.事件排除判定算法(ShouldRejectEvent).

算法5.同一動作序列的EE 規則生成(SameActionsRules).

算法4 旨在判斷事件E可否發生并在發生后使得Ψ(不兼容的條件)為真(進而導致Ψ對應的某個動作序列的執行),需要根據篩選策略P做關于系統抽象狀態的可滿足性判定.篩選策略從保守到激進有多種策略:激進 的策略需要對事件發生之前的系統狀態做出更強的假設,而保守的策略只需要相對較弱、能夠更快判定的假 設.本文提出的默認策略Pdefault為:事件發生前Ψ為假(兼容),事件發生后Ψ為真(不兼容),且事件發生前 后Vs→Vd的事件轉移條件CE成立,則該事件不會被排除.

Fig.5 Relation between current event filtering strategy and state transition圖5 當前使用的事件篩選策略與狀態轉移的關系

? EE 中間表示生成模塊

該模塊調用算法5 生成EE 規則.以上一步驟篩選輸出的事件E=(模式,狀態,{離家模式},{回家模式})、規 則組的不兼容條件為例,對于圖4 左下方中的4 個執行前提-動作序列對,都要判斷執行前提是否可能 滿足并生成規則.這里以4 對中的左上一對為例,由算法5 的第5 行得到的條件:“回家模式=回家模式 AND 溫濕度傳感器.溫度>28°C AND (電扇.開關!=開 OR 電扇.風速!=低) AND (電扇.開關!=開 AND 電扇.風速!=低)”作為動作執行的完整前提條件,同時也應當是E發生后為真的條件,結合事件發生前應當為真的條件!Ψ,得到關于系統狀態的斷言并判定是可滿足的,因此生成一條規則:

IF 模式.狀態 FROM {離家模式} TO {回家模式} WHILE 溫濕度傳感器.溫度>28°C AND

電扇.開關!=開 AND 電扇.風速!=低 THEN 電扇.開關 打開,電扇.風速 設定 低.

算法4 雖然和這里的算法5 都需要對一組系統狀態的斷言做可滿足性求解,但是算法4 不考慮動作序列的 執行前提,其篩選結果能夠被同一X的多個動作序列復用;且能夠通過算法4 篩選的只有較少數量事件,這些事 件至少能夠與一個動作序列組合成為規則.算法4 的存在,減少了轉譯過程中總的可滿足性判定的次數.若直接將候選事件集合與多種動作序列的組合輸入算法5,可能需要較多次數的不必要的求解.

4 方法評估

為了驗證SSRules 的系統設計的有效性,基于Python 開發了SSRules 運行時子系統和離線轉譯器;基于Javascript 開發了SSRules 前端用戶交互模塊,方便終端用戶設置SS 規則(如圖6 左上方);同時,結合已有用戶調查[15]構建智能家居使用情景,在這些場景下,就SSRules 系統運行情況和規則轉譯效果進行評估和討論.

4.1 智能家居實驗場景搭建

為了能夠評估SSRules,需要將一些設備連接到HA,并讓設備和環境產生足夠多的狀態轉移,以覆蓋各種可能的使用情形.但是,使用真實設備無法在短時間得到這樣的測試場景并且調試不便.為此,我們基于Unity 游戲引擎開發了一個能接入HA 的智能家居模擬器HA-Simulator(其界面如圖6 下方).利用HA-Simulator 可以將時間加速,以較高的速度發生系統的狀態變化,并對溫濕度/煙霧濃度等環境因素合理建模.這使得在短時間內測試大量的智能家居系統狀態變遷并驗證SSRules 成為可能.

在HA-Simulator 中模擬了12 種智能家居設備,布局和類型如圖6 右上方所示,這些設備通過HA 的MQTT Discovery 集成方式接入HA.此外,在HA 中以自定義方式提供模式、天氣和時鐘這3 種虛擬設備.在模擬器中,同一房間內的設備受同一組環境變量(溫度、濕度、煙霧濃度)的影響.模擬器可以設置環境變量改變的速度,進而間接改變虛擬傳感器的取值;同時,模擬器中的設備可以被手動調節或者由模糊測試程序隨機改變.

Fig.6 SSRules user interface,Smart home configuration and HA-simulator圖6 SSRules 用戶交互界面與智能家居場景配置和模擬器示意圖

4.2 實驗結果分析

? SS→HA 翻譯對比

首先參考以往用戶調查[15]中用戶的智能家居需求,構造了10 組SS 規則作為測試集,其中:編號為1~6 的規則組不含歷史狀態,編號為T1~T4 的規則組含有歷史狀態.每一組規則至少有一個動作實體(設備),規則中會引用多個相關實體的狀態.另外,規則組6、規則組T3、規則組T4 含有多個動作實體.按照當前的事件篩選策略,翻譯前后的規則條數比較見表8.最終生成的HA 規則條數均多于SS 規則條數,比例為2 倍~4 倍.

? HA 規則運行覆蓋率

在由SS 轉譯得到HA 規則之后,每一組HA 規則均在模擬器上運行20 分鐘.除第1 組規則(包含空調與溫濕度傳感器)和第3 組規則(包含排氣扇以及其他4 個相關實體)之外,其余組的HA 規則均全部被執行過.這說明SS→HA 轉譯器為其余8 組規則產生的HA 規則集中沒有多余的規則,當前的事件篩選策略對于多數測試樣例是比較合理的.對于含有多余規則的情形,而第1 組的4 條SS 規則為:

FOR 客廳空調

EXPECT (模式,制冷)(溫度,18°C) WHILE 客廳溫濕度傳感器.溫度>28°C

EXPECT (模式,制熱)(溫度,20°C) WHILE 客廳溫濕度傳感器.溫度<10°C

EXPECT (模式,干燥) WHILE 客廳空調.模式!=制熱 AND 客廳空調.模式!=制冷 AND 客廳溫濕度傳感器.濕度>65% EXPECT (模式,關) WHILE 客廳溫濕度傳感器.溫度<22°C AND 客廳溫濕度傳感器.溫度>14°C 而在轉譯出的13 條HA 規則中,沒有被執行過的(可能是多余的)一條HA 規則用EE 范式表達為:

IF 客廳溫濕度傳感器.溫度 FROM (-30°C,10°C)∪(28°C,70°C) TO [10°C,28°C] WHILE

客廳空調.模式!=制冷 AND 客廳空調.模式!=制熱 AND 客廳空調.模式!=干燥

AND 客廳溫濕度傳感器.濕度>65% THEN 客廳空調.模式設定干燥

Table 8 Comparison of SS and HA rules and test results表8 SS→HA 翻譯對比和測試運行

原因在于:當前的篩選策略沒有假設系統狀態在事件發生之前的瞬間與整個規則組GS的描述相符,而僅僅假設系統狀態與第3 條SS 規則的描述是兼容的(即第3 條規則未激活或者其期望狀態已滿足).但是在測試運行中,當溫度低于10°C 或者高于28°C 時,系統狀態持續與GS的描述相符,空調模式一定是制熱(第2 條SS 規則激活)或者制冷(第1 條SS 規則激活),所以該條EE 規則是多余的,通過使用更激進的事件篩選策略可將其消除.

? HA 規則運行異常檢測

表8 的后3 列分別是在20 分鐘的隨機測試下,各組的HA 規則的執行次數、異常檢測模塊發現的異常次數(系統狀態不滿足動作實體的SS 規則集合中激活的那一條SS 規則的期望狀態)與總檢測次數之比、是否存在連續兩次檢測到異常的情況.各組總的規則執行次數相差不大.異常檢測模塊目前以定時輪詢方式實現,在20分鐘內進行了1 200 次異常檢查,未發現連續出現異常的情形.對于單次檢測出現異常的情況,經過查看記錄的狀態日志和HA 規則的執行序列,這些異常均因網絡延遲(動作執行不及時)造成.

5 相關工作

智能家居目前在市場上受到了廣泛歡迎,越來越多的家庭配置了智能家居的設備.智能家居最吸引人的功能之一就是以應用程序的形式支持自定義自動化.但是由于用戶未經過專業的培訓,導致其自定義的規則存在一定的缺陷,甚至無法定制規則,這引起了人們對物聯網增強生活的風險的擔憂.這些風險遠非僅僅是學術上的,更緊迫的是對用戶的生命財產的威脅.Triger-Action 編程(TAP)是一種流行的終端用戶編程方式,可以讓用戶實現其智能設備和云服務的交互.然而,用戶有時并不能通過TAP 正確表達自己的意圖并實現相應的功能.隨著此類系統部署在越來越復雜的智慧家居場景中,用戶必須能夠識別編程錯誤并解決.

為了給終端用戶提供更高效的服務,首先需要理解用戶編程出現錯誤和規則沖突的原因.Huang 等人[6]認為,現有TAP 編程系統(如IFTTT)的過分簡化限制了程序的表達能力.提出了改進IFTTT 界面的建議,以減輕因心理模型不正確而引起的問題.Corno 等人[28]認為:現有的TAP 接口界面暴露了太多功能,并迫使用戶在眾多混亂的網格菜單中進行搜索,導致用戶無法得到原本需要的功能.為此,作者提出了EUDoptimizer,旨在以交互方式協助終端用戶使用循環中的優化器來組合 IF-THEN 規則,減少了編寫Triger-Action 規則所需的工作.Brackenbury 等人[17]提出了10 類常見的TAP 編程錯誤類型,作者發現:錯誤的存在,使參與者更難正確預測規則的行為.Davidoff 等人[29]發現,智能家居用戶的日?；顒优c編程任務并不匹配.論文描述了家庭想要的控制,并提出了有助于終端用戶編程系統實現這種控制的7 種設計原則.Brush 等人[20]認為:為使智能家居得到更廣泛的使用,需要解決成本高昂、設備不靈活、客觀理性差和安全保障這4 個障礙.論文還為進一步研究提供了幾個方向,包括消除變化結構的需要、為用戶提供簡單的安全原語并支持家庭設備的組合.

因此,為減少終端用戶編程的錯誤,TAP平臺需要對用戶生成TAP規則進行指導,并實現模型的檢查,自動發現規則漏洞或沖突.Wang 等人[14]利用IFTTT 平臺,探討了在Triger-Action 平臺中可能存在的規則漏洞,并借助于自然語言處理的方法推斷Triger-Action 信息,實現了一個模型檢查系統iRuler,用于發現物聯網中的規則間漏洞.Celik 等人[19,30,31]認為,物聯網中存在大量的設備交互.因此,不僅需要驗證單個設備,還需要對設備的聯合行為進行檢查.Soteria[30]是一種靜態分析系統,可從IoT 應用程序的源代碼中提取狀態模型,并通過模型檢查來驗證IoT 應用程序或IoT 環境是否符合已標識的屬性.考慮到靜態分析在估計物聯網狀態轉換方面的局限性,Celik 等人[19]繼續開發了一個動態分析系統IoTGuard,可通過在運行時監視設備執行行為,來強制執行已標識的屬性,并可以通過阻止違反屬性的設備操作,或在運行時要求用戶批準或拒絕違規操作來應對屬性違規.肖丁等人提出的基于知識圖譜的KGIID 算法[32]能夠檢測TAP 編程模型中沖突的動作(隱式沖突).孟巖等人提出的HODETECT 檢測工具[33]利用無線側信道技術從智能家居應用中提取工作邏輯,并用有限狀態自動機建模,通過在應用運行時監聽無線加密流量的元數據來推測應用的執行狀態,間接檢測惡意應用.陳星等人[34]提出了智能家居情境感知服務的運行時建模與執行方法,能夠降低開發者開發智能家居情境感知服務的難度和復雜度.

更進一步地,TAP 服務提供平臺還需要對存在缺陷的規則進行修復.Nandi 等人[26]注意到,終端用戶在編寫規則時所犯的一個常見錯誤是觸發器數量不足.因此,作者開發了TrigGen,它可以根據規則中的操作自動生成一組必要和充分的觸發器,來幫助終端用戶正確地編寫規則.這種做法在一定程度上減少了意外行為和安全漏洞的發生率,但是其對于潛在沖突的檢測還有提升空間.為幫助非專業的物聯網用戶系統地實現高置信度的實時HA-IoT 系統,Bu 等人[16]介紹了一種自動化端到端編程輔助框架MenShen,它能夠檢查自動化規則集是否違反規范,從而為用戶提供可能的解決方案.Zave 等人[24]建議在運行時通過優先級來減少設備管理和交互的成本,并通過組合機制實現了目標.Zhang等人[15]將用戶需要表達的屬性轉換為線性時序邏輯(LTL),自動合成滿足屬性的TAP 規則,并修復現有的TAP 規則.

6 總 結

基于規則的智能家居系統是目前流行的一種智能家居系統,而編寫瑣碎、修改困難、錯誤難以追蹤是以往用戶調查[15]所反映的問題.本文提出的SS 范式以及配套的SSRules 系統實現方式,使得用戶規則編寫和修改的復雜程度大為減低;同時,設計的SS 規則到HA 規則的轉譯算法使得輸入的SS 規則能夠在現有的智能家居系統HA 規則引擎上運行,并且通過輔助的SSRules 運行時模塊,能夠提供規則執行異常檢測的能力.

未來的工作重點在以下兩個方面:一方面,采用模型檢測技術實現對SS 范式無法避免的缺陷進行檢測,并設計輔助用戶編寫SS 規則和避免缺陷的實時反饋算法;另一方面,對于SS 范式目前不能夠表達的需求,進行用戶調查并尋找合適的多范式協同輸入對策.