基于智能家居的一致性模型融合技術研究

包曉安, 林 輝, 周建平, 桂 寧, 孫獻策, 張 娜

(1. 浙江理工大學信息學院, 杭州 310018; 2. 海鹽盛迪電子科技有限公司, 浙江嘉興 314300)

基于智能家居的一致性模型融合技術研究

包曉安1, 林 輝1, 周建平2, 桂 寧1, 孫獻策1, 張 娜1

(1. 浙江理工大學信息學院, 杭州 310018; 2. 海鹽盛迪電子科技有限公司, 浙江嘉興 314300)

在智能家居的自適應軟件設計中,往往采用傳統的模塊構建技術。但由于其適應邏輯存在著低復用性、高復雜度等問題,很難驗證模塊組合后的正確性及有效性。為了滿足開發過程中用戶的增量性需求,針對適應邏輯的組合難題,提出把部分行為模型的形式化方法引入到適應行為的描述中。通過三值邏輯KMTS模型描述語言,提出一致性模型的判斷方法以及融合算法,以提供明確的適應模型在線融合支持。最后通過智能家居中的一個模型實例來分析并驗證融合后的適應邏輯。

智能家居; 模型融合; 適應邏輯; KMTS; 一致性模型

0 引 言

隨著智能家居不斷地進入到人們的生活中,智能設備的自適應技術也越來越受到關注。在當前的自適應軟件設計中,主要是采用專用的適應模塊構建方式。這種方式是由多個模塊共同實現用戶需求,當用戶需求或是環境發生變化后,以模塊替換甚至模塊的重新組合來完成整體功能的設計。然而,由于原有軟件模塊與需求模塊的適應邏輯,往往因設計目標或者描述語言的不同,使得適應邏輯的組合設計顯得非常困難。一些知名研究者在適應邏輯組合上已經有深入的研究,如Maurel等[1]提出了基于投機的融合策略,該策略的核心是假設各個適應邏輯不會產生沖突,在這種假設下各個適應方案進行直接地疊加。Sicard等[2]提出了一種支持軟件自修復的自適應軟件框架,在該框架中,兩種不同的適應目標是通過設計一種特別的適應算法來進行融合,以消除可能存在的沖突。但是,這個專用的算法在兩個不同的適應邏輯中間構成了強耦合機制,使得適應模塊在不同上下文中很難被重用。接鈞靖等[3]實現了一種基于質量運行時動態評估的自主構件的自適應機制,通過對自主構件的性能監控,以評估自適應策略的優劣并進行調整,但沒有涉及如何構建適應邏輯過程。這些關于多模型融合的自適應軟件開發模式,大致分為三大類:簡單融合、專用算法融合方案和基于收益函數的融合方案。由于這些方案通常是采用經驗性的解決方式,因此很難驗證組合后模塊的正確性及有效性。

為了更好地解決模塊組合后適應邏輯的驗證性問題,本文借助了部分行為模型(partial behaviour model)[4]的數學工具,提出將部分行為模型的形式化方法引入到自適應軟件適應行為的描述中,使得適應邏輯組合的過程形式化。通過精確地描述建模中未知以及可重配置的信息,從而使得模型融合的實現及其驗證成為可能。把不同的自適應軟件模塊看成是不同的適應模型,以部分行為模型的不斷融合來滿足增量性的需求。在形式化描述的基礎上,設計部分適應模型之間的一致性判定方法,以及適應邏輯融合算法,為一致性模型的融合提供可靠支持。通過構建相應的模型融合實例,抽象的模型分析以及實際的開發應用,實現了融合結果的正確性及有效性驗證。

1 形式化描述語言的選擇和分析

為了支持適應模型增量性的融合以及解決融合過程中所產生的沖突,適應模型必須支持對當前未知信息的明確建模。傳統的建模語言kripke structure,如圖1(a)所示,使用kripke架構定義了所有的狀態和轉換,并不支持可能的狀態轉換或求精。為了更好地支持增量式的軟件開發模式,一些研究者提出部分行為模型的概念,把每一個需要進行融合的模型都作為系統整體的一個部分,通過不斷融合多個部分模型來嚴格描述整體行為,并判斷其特性。它對“分而治之”[5]的開發模式有著良好的支持,并逐漸成為行為模型形式化研究的熱點。目前出現了許多基于部分行為模型的形式化語言和架構,如部分標記變遷系統(partial labelled transition systems,PLTSs)[6], multi-valued state machines[7]等。如圖1(b)使用了基于三值邏輯的KMTS(kripke modal transition system),增加了可能的狀態轉換(虛線表示)和可能的狀態(p=m意味著p的狀態未知)支持,可以有效地提供對未知和可重配信息的描述,并且一些非確定的描述可以在行為模型設計中逐步求精或者多部分模型融合過程中逐步去除,從而為適應行為模型的融合描述提供了良好支持。

圖1 基于狀態機的形式化描述

KMTS是一個元組(S,s0,Rmust,Rmay,L,AP),定義了所有的狀態和轉換,包括可能的狀態和轉換。其中S是狀態集,s0是初始狀態,Rmust?S×S表示狀態之間的確定性關系,Rmay?S×S表示狀態之間的可能性關系。而L→3AP表示一個三值標記功能,以t(true)、f(false)、m(maybe)三值標記狀態中的每個事件是否發生。AP則表示一個模型中事件的集合,在模型融合時,以APu表示融合模型的事件總集。

用KMTS形式化描述語言對圖1(b)進行如下定義:

a)S={t0,t1,t2},其中t0是初始狀態;

b)Rmust={(t0,t1),(t1,t2),(t2,t0)};

c)Rmay={(t0,t1),(t1,t2),(t2,t0),(t0,t2)};

d)L(t0)={(p,t),(q,t)},L(t1)={(p,m),(q,t)},L(t2)={(p,t),(q,f)};

e)AP={p,q}

KMTS描述時,令Rmust?Rmay,轉移關系Rmust用實心箭頭表示,而RmayRmust用虛線箭頭表示。

在自適應軟件開發中,用戶需求以及自適應環境往往會隨時發生變化,模型之間的關系很難被預先判斷,從而影響模型的融合策略以及融合效果。本文所研究的模型融合過程,是針對于一致性模型之間,并且基于不變的環境以及需求,以保證模型融合過程中的穩定性。對于需要進行融合的兩個適應模型,首先需要確定模型間的關系。由于設計的目標和設計角度不同,不同模型可能采用不同的描述語言,很難判斷模型間關系[8]。本文統一所有模型的形式化描述語言為KMTS,以基于狀態機的運行方式綜合判斷模型間是否具有相關性,而在相關模型中,根據模型間有無沖突又可區分為一致性與非一致性。其次,針對模型間關系,從而采取不同的融合策略[9]來比較并且融合這些相關模型。在一致性模型融合時,關鍵在于確定相同性質的狀態以及轉移關系,為融合行為提供切入點。最后我們需要對融合結果進行分析,以確保模型融合是否實現了融合目標。

2 適應行為模型融合

模型融合是模型之間的最小共同求精(least common refinement, LCR)[10]的過程。在模型融合之前,需要對各個模型采用KMTS描述。若模型之間的KMTS語言描述無關,則可認為模型融合時不產生干擾,產生的LCR唯一,即作為模型融合結果。

若模型之間的KMTS語言描述相關時,在模型融合過程中,將產生多個無法相互比較的極小共同求精。為此,本文進一步研究了獲得最小共同求精的方法。

2.1 相關模型的統一描述

對于需要進行融合的適應模型,都是內在不完整的模型。這些模型都只描述整個系統某些極少的事件。例如,設一個系統中有兩個模型K1、K2,KMTS形式化描述如下:

K1:{S1={s0,s1};Rmust={(s0,s1)};

Rmay={(s0,s1)};L(s0)={(p,t)},L(s1)={(p,t);AP={p}}。

K2:{S2={u0,u1,u2};Rmust={(u0,u1),(u1,u2)};Rmay={(u0,u1),(u1,u2)};L(u0)=(q,f),L(u1)=(q,f),L(u2)=(q,f);AP={q}}。

其中系統的事件總集APu={p,q}。為了比較并融合這些不完整的模型,需要統一它們的描述。模型描述的統一可以分為以下兩個部分。

a) 行為統一。在單一的KMTS模型描述中,所有的狀態轉移都是確定的,此時Rmust與Rmay是等同的。每一個模型都只單獨地描述其所涉及到的狀態。但在統一的描述中,每一個模型必須描述所有與之相關或者可能相關的狀態。因此需要增加這些未被描述的狀態以及狀態之間可能的轉移關系。在K1中,為了與K2中的狀態以及轉移關系相對應,修改其KMTS部分描述為{S1={s0,s1,s2};Rmust={(s0,s1)};Rmay={(s0,s1),(s1,s2)}}。

b) 事件統一。對于模型中的每一個狀態,需要把其中的事件與事件總集APu進行比較并進行調整,使得每一個狀態的事件與APu中的事件完全相同。而對于所補充的事件,其屬性都以m賦值,表示事件可能發生。通過在K1、K2中分別增加事件q和p,則修改的部分KMTS描述為:

K1:L(s0)={(p,t),(q,m)},L(s1)={(p,t),(q,m)},L(s2)={(p,m),(q,m)};AP={p,q};

K2:L(u0)={(p,m),(q,f)},L(u1)={(p,m),(q,f)},L(u2)={(p,m),(q,f)};AP={p,q}。

2.2 一致性模型的判斷以及融合條件

設有兩個模型K1、K2,在統一KMTS描述后,對K1和K2模型進行一致性關系判斷。現定義一致性關系標記符～?S1×S2,設s與u分別表示K1與K2中的狀態,若s～u,則需滿足以下幾個條件:

a) ?p∈APu·(L1(s,p)=t?L2(u,p)≠f)∧(L2(u,p)=t?L1(s,p)≠f);

其中p表示APu中的事件,s′、u′分別表示模型K1、K2中的狀態。以上模型一致性的判斷是具有遞歸效應的,若s～u,則s與u狀態中的所有事件都保持一致性,并且它們的后繼者也保持一致性。因此,若是對于模型的初始狀態s0、u0,滿足s0～u0,則可以推出K1～K2,即兩模型保持一致性。

a)S+={(s,t)|s～u};

2.3 模型融合算法

對于兩個相關的適應模型,在融合前經過判斷并確定滿足一致性后,分析對應的融合條件,則本文基于部分行為模型的一致性模型融合的算法流程如圖2所示。

圖2 行為模型融合流程

在融合過程中,主要關鍵步驟為:

a) 對原有模型和需求模型進行廣度優先搜索,統一狀態中的事件集,使得每個狀態都包含APu中的所有事件。對于狀態中新增的事件p,以m表示其真值。

b) 以原有模型的初始狀態s0為出發點,遍歷需求模型的所有狀態,找出與之保持一致性的某個狀態,反之亦可。若都未成功找尋,則說明兩模型并非一致性,無法使用本文的融合方法。若找尋成功,則補充兩模型之間未形成對應的狀態,并以虛線箭頭表示為可能性轉移關系。

c) 統一保持一致性關系的對應狀態s,t中的事件到融合狀態(s,t)中,以及保持一致性的對應轉移關系到融合模型中。

d) 對融合的模型進行最小求精,分析狀態中真值為m的事件,修改真值為t或是f。模型融合完成后,再對照相應的適應邏輯進行驗證。

3 實例研究與分析

3.1 模型融合過程實例研究

以智能家居中一個簡單的適應模塊組合為例,整個控制系統由模塊“數據采集”和“窗簾控制”共同構成。自適應窗簾采用感應控制,當室外光照強度大于設定值時,窗簾自動打開可實現室內照明,反之則自動關閉。窗戶玻璃采用特殊材料,可隔絕室外熱量傳遞,但是為了方便室內人員觀看室外風景,用戶增加了自適應窗戶的需求,通過感應人窗距離從而實現窗戶的打開與關閉。因此,在控制策略上需要發生調整,以適應窗簾以及窗戶的共同控制需求。

窗簾控制模型中有兩個事件,即電源以及窗簾是否開啟。以符號Power表示電源開啟,┐Power表示電源關閉;Curtain表示窗簾打開狀態,┐Curtain表示窗簾關閉。KMTS描述如圖3(a)所示。對于窗戶控制需求模型,同理,用Window表示窗戶打開,┐Window表示窗戶關閉。在窗簾打開的前提下,只要室內有人距離窗戶距離小于設定值時,窗戶便能自動打開,反之窗戶則處于關閉狀態,該需求模型KMTS描述如圖3(b)所示。

圖3 單一的KMTS描述

但在圖3(a)中各個狀態中,只包含事件Power以及Curtain,缺少了需求模型中的事件Window,同時也缺少了對于感應人窗距離后所可能發生的狀態轉移。因此可以把它補充完整,如圖4(a)所示。同理,圖4(b)為窗戶控制需求模型的統一KMTS描述。

圖4 統一的KMTS描述

在統一窗簾控制模型以及窗戶控制需求模型的KMTS描述后,根據前文所給出的適應模型融合算法,判斷兩模型的一致性關系,從而進行模型融合,融合結果如圖4(c)所示。

3.2 模型融合開發展示

以安卓平臺為開發工具,對本文實例進行簡單開發,界面如圖5所示,主要把整個系統分為三個部分:a) 顯示區,可顯示窗簾、窗戶事件,并以紅、綠指示燈表示關閉、開啟狀態。在現實生活中,只有顯示區是呈現在人們眼前的。b) 感應區,由各類傳感器組成,以指示燈顯示感應狀況。例如窗簾傳感器開啟時,可以感應窗外的光照強度;同理,窗戶傳感器可以感應室內的人窗距離。c) 控制區,可以根據感應區產生的反饋,采用固定的適應邏輯,以控制相應事件的開啟與關閉。控制區處于整個系統的控制中樞,對于系統的成功運作起著至關重要的作用。

圖5 實例圖

圖5(a)表示了整個系統只需要實現窗簾的控制,控制區固有的適應邏輯就是根據窗簾感應器的狀態實現對窗簾的控制。在適應邏輯不變的情況下,窗簾控制與其相應的感應器是保持一致的。當增加自適應窗戶的需求時,如圖5(b)所示,若未進行模型融合或者融合的模型不正確時,控制區的適應邏輯是不正確的。因此,即使窗戶傳感器感應到人窗距離小于設定值時,也不能使得對應的窗戶打開,其旁邊的指示燈仍然是紅色的。只有適應邏輯進行正確的改變,整個系統的控制功能才能發生作用,使得窗簾與窗戶均能開啟或關閉,如圖5(c)所示。

在實際操作過程中,把窗簾與窗戶抽象成兩個部分行為模型,分別進行建模。通過第二節的融合算法,若兩者能夠相互融合,則它們的適應邏輯也會同時發生融合。完整融合之后的適應邏輯便能夠正確并且有效地控制整個系統。

3.3 融合結果分析

融合的模型必須在理解模型結果的前提下,從約束和場景兩方面進行分析。

在模型中,每一個事件都可以看成是其行為表現,而融合的模型在事件上必定有所關聯。窗簾和窗戶的模型融合,都要保證電源的開啟。同時,只有在窗簾打開的狀態下,才能正常地實現窗戶的打開與關閉。但是對于融合模型的每個狀態,包含的事件數有最低和最高約束。一般來說,很少可以包含所有事件。那么,對于融合模型中所有取值為m的事件,如果不能從相連事件中確定它的確切真值,則需要從狀態中去除。該實例中,在模型融合后,窗簾關閉狀態中的Window真值為m,由前提設定中可知窗簾關閉時不實現窗戶的自適應控制,因此可分析得到它的確切真值是f,應該保留。同時,對于相同事件,在同一個狀態中也不應該重復出現。

原始模型和需求模型,對應不同的場景。如窗簾控制模型,為了滿足房間內的照明需求。而窗戶控制需求模型,則為了方便室內人員觀看室外風景。從場景分析中發現,窗戶可以實現自適應開關的前提是窗簾已經打開。因此,當模型融合之后,融合結果也必須符合兩者的相關關系。

4 結 論

在智能家居中的自適應軟件開發過程中,模塊組合可以有效解決復雜的建模問題。然而,由于專用模塊適應邏輯存在著高復雜度、低復用性等問題,很難驗證其組合后適應邏輯的有效性和正確性。針對此問題,本文通過將部分行為模型的形式化方法引入到自適應軟件的適應行為的描述中,從系統的局部行為來分析適應邏輯的動態組合過程,使得模型融合形式化,并為融合結果的驗證提供了有力基礎。本文采用的KMTS描述語言,增加了對可能行為和可能狀態的支持,可以有效地提供模型對未知和可重配置信息的描述。因此,當兩KMTS模型具有一致性時,它們的融合便可以看作生成最小共同求精LCR模型的過程。本文提出的一致性模型判斷以及融合算法也為融合模型的驗證提供了有效依據。

本文所研究的模型融合方法,主要是針對一致性的適應模型之間。并且,在基于固定需求的模型融合時,需保持自適應環境的穩定。我們將進一步針對非一致性模型之間的融合以及多變環境的適應情況進行研究。

[1] Maurel Y, Diaconescu A, Lalanda P. Creating complex, adaptable management strategies via the opportunistic integration of decentralised management resources[C]//Proceedings of the 2009 International Conference on Adaptive and Intelligent Systems. Washington: IEEE Computer Society, 2009: 86-91.

[2] Sicard S, Boyer F, De Palma N. Using components for architecture-based management: the self-repair case [C]//Proceedings of the 30th International Conference on Software Engineering. New York : ACM , 2008: 101-110.

[3] 接鈞靖, 史庭訓, 焦文品, 等. 自主構件自適應策略的在線定制及動態評估[J]. 軟件學報, 2012, 23(4): 802-815.

[4] Uchitel S, Alrajeh D, Ben D S, et al. Supporting incremental behaviour model elaboration[J]. Computer Science-Research and Development, 2013, 28(4): 279-293.

[5] Gui N, Florio V D, Blondia C. Transformer: an adaptation framework with contextual adaptation behavior composition support[J]. Software Practice &Experience, 2013, 43(8): 937-967.

[6] Uchitel S, Kramer J, Magee J. Behaviour model elaboration using partial labelled transition systems[J]. ACM SIGSOFT Software Engineering Notes, 2003, 28(5): 19-27.

[7] Redondo R P D, Pazos A J J. Reuse of verification efforts and incomplete specifications in a formalized, iterative and incremental software process[C]//Proceedings of the 23rd International Conference on Software Engineering. Toronto: IEEE Computer Society, 2001: 801-802.

[8] Nejati S, Sabetzadeh M, Chechik M, et al. Matching and merging of variant feature specifications[J]. Software Engineering, IEEE Transactions on, 2012, 38(6): 1355-1375.

[9] 易 立, 趙海燕, 張 偉, 等. 特征模型融合研究[J]. 計算機學報, 2013, 36(1): 1-9.

[10] Fischbein D, Uchitel S. On correct and complete strong merging of partial behaviour models[C]//Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York : ACM, 2008: 297-307.

(責任編輯： 陳和榜)

Research on Consistency Model Fusion Technology Based on Smart Home

BAOXiao-an1,LINHui1,ZHOUJian-ping2,GUINing1,SUNXian-ce1,ZHANGNa1

(1. The School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China; 2. Haiyan Shengdi Electrical Technical Co., Ltd., Jiaxing 314300, China)

In the self-adaptive software design of smart home, the traditional module construction technology is often adopted. However, due to its low reusability and high complexity in adaptive logics, it is very difficult to confirm the correctness and effectiveness of module combination. In order to meet users’ incremental demand in development process, this paper proposes to introduce formalization method of partial behavioral model into the description of adaptive behavior based on combination difficulty of adaptive logics. Through three-valued logic KMTS model description language, this paper proposes judgment method and fusion algorithm of consistency model to provide clear online fusion support for adaptive model. Finally, this paper takes a smart home model as an example to analyze and confirm the adaptive logics after fusion.

smart home; model fusion; adaptive logics; KMTS; consistency model

1673- 3851 (2015) 01- 0109- 06

2014-04-28

國家自然科學基金資助項目(61202050,61379036);浙江省自然科學基金資助項目(Y13F020175);浙江理工大學521人才培養計劃資助項目;浙江省錢江人才計劃資助項目(2013R10015);浙江省新苗計劃項目(2013R406070)

包曉安(1973-),男,浙江東陽人,教授,主要從事自適應軟件及軟件測試等方面的研究。

TP311.5

A