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

包曉安, 林 輝, 周建平, 桂 寧, 孫獻(xiàn)策, 張 娜

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

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

包曉安1, 林 輝1, 周建平2, 桂 寧1, 孫獻(xiàn)策1, 張 娜1

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

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

智能家居; 模型融合; 適應(yīng)邏輯; KMTS; 一致性模型

0 引 言

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

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

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

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

圖1 基于狀態(tài)機(jī)的形式化描述

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

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

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

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描述時(shí),令Rmust?Rmay,轉(zhuǎn)移關(guān)系Rmust用實(shí)心箭頭表示,而RmayRmust用虛線箭頭表示。

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

2 適應(yīng)行為模型融合

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

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

2.1 相關(guān)模型的統(tǒng)一描述

對(duì)于需要進(jìn)行融合的適應(yīng)模型,都是內(nèi)在不完整的模型。這些模型都只描述整個(gè)系統(tǒng)某些極少的事件。例如,設(shè)一個(gè)系統(tǒng)中有兩個(gè)模型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}}。

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

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

b) 事件統(tǒng)一。對(duì)于模型中的每一個(gè)狀態(tài),需要把其中的事件與事件總集APu進(jìn)行比較并進(jìn)行調(diào)整,使得每一個(gè)狀態(tài)的事件與APu中的事件完全相同。而對(duì)于所補(bǔ)充的事件,其屬性都以m賦值,表示事件可能發(fā)生。通過在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 一致性模型的判斷以及融合條件

設(shè)有兩個(gè)模型K1、K2,在統(tǒng)一KMTS描述后,對(duì)K1和K2模型進(jìn)行一致性關(guān)系判斷。現(xiàn)定義一致性關(guān)系標(biāo)記符～?S1×S2,設(shè)s與u分別表示K1與K2中的狀態(tài),若s～u,則需滿足以下幾個(gè)條件:

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中的狀態(tài)。以上模型一致性的判斷是具有遞歸效應(yīng)的,若s～u,則s與u狀態(tài)中的所有事件都保持一致性,并且它們的后繼者也保持一致性。因此,若是對(duì)于模型的初始狀態(tài)s0、u0,滿足s0～u0,則可以推出K1～K2,即兩模型保持一致性。

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

2.3 模型融合算法

對(duì)于兩個(gè)相關(guān)的適應(yīng)模型,在融合前經(jīng)過判斷并確定滿足一致性后,分析對(duì)應(yīng)的融合條件,則本文基于部分行為模型的一致性模型融合的算法流程如圖2所示。

圖2 行為模型融合流程

在融合過程中,主要關(guān)鍵步驟為:

a) 對(duì)原有模型和需求模型進(jìn)行廣度優(yōu)先搜索,統(tǒng)一狀態(tài)中的事件集,使得每個(gè)狀態(tài)都包含APu中的所有事件。對(duì)于狀態(tài)中新增的事件p,以m表示其真值。

b) 以原有模型的初始狀態(tài)s0為出發(fā)點(diǎn),遍歷需求模型的所有狀態(tài),找出與之保持一致性的某個(gè)狀態(tài),反之亦可。若都未成功找尋,則說明兩模型并非一致性,無法使用本文的融合方法。若找尋成功,則補(bǔ)充兩模型之間未形成對(duì)應(yīng)的狀態(tài),并以虛線箭頭表示為可能性轉(zhuǎn)移關(guān)系。

c) 統(tǒng)一保持一致性關(guān)系的對(duì)應(yīng)狀態(tài)s,t中的事件到融合狀態(tài)(s,t)中,以及保持一致性的對(duì)應(yīng)轉(zhuǎn)移關(guān)系到融合模型中。

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

3 實(shí)例研究與分析

3.1 模型融合過程實(shí)例研究

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

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

圖3 單一的KMTS描述

但在圖3(a)中各個(gè)狀態(tài)中,只包含事件Power以及Curtain,缺少了需求模型中的事件Window,同時(shí)也缺少了對(duì)于感應(yīng)人窗距離后所可能發(fā)生的狀態(tài)轉(zhuǎn)移。因此可以把它補(bǔ)充完整,如圖4(a)所示。同理,圖4(b)為窗戶控制需求模型的統(tǒng)一KMTS描述。

圖4 統(tǒng)一的KMTS描述

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

3.2 模型融合開發(fā)展示

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

圖5 實(shí)例圖

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

在實(shí)際操作過程中,把窗簾與窗戶抽象成兩個(gè)部分行為模型,分別進(jìn)行建模。通過第二節(jié)的融合算法,若兩者能夠相互融合,則它們的適應(yīng)邏輯也會(huì)同時(shí)發(fā)生融合。完整融合之后的適應(yīng)邏輯便能夠正確并且有效地控制整個(gè)系統(tǒng)。

3.3 融合結(jié)果分析

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

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

原始模型和需求模型,對(duì)應(yīng)不同的場景。如窗簾控制模型,為了滿足房間內(nèi)的照明需求。而窗戶控制需求模型,則為了方便室內(nèi)人員觀看室外風(fēng)景。從場景分析中發(fā)現(xiàn),窗戶可以實(shí)現(xiàn)自適應(yīng)開關(guān)的前提是窗簾已經(jīng)打開。因此,當(dāng)模型融合之后,融合結(jié)果也必須符合兩者的相關(guān)關(guān)系。

4 結(jié) 論

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

本文所研究的模型融合方法,主要是針對(duì)一致性的適應(yīng)模型之間。并且,在基于固定需求的模型融合時(shí),需保持自適應(yīng)環(huán)境的穩(wěn)定。我們將進(jìn)一步針對(duì)非一致性模型之間的融合以及多變環(huán)境的適應(yīng)情況進(jìn)行研究。

[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] 接鈞靖, 史庭訓(xùn), 焦文品, 等. 自主構(gòu)件自適應(yīng)策略的在線定制及動(dòng)態(tài)評(píng)估[J]. 軟件學(xué)報(bào), 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]. 計(jì)算機(jī)學(xué)報(bào), 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.

(責(zé)任編輯： 陳和榜)

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

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

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

TP311.5

A