趙 鑫 盧 濤

(大連理工大學(xué)管理與經(jīng)濟(jì)學(xué)部 遼寧 大連 116024)

基于時(shí)間自動機(jī)的ECA規(guī)則交互問題研究

趙 鑫 盧 濤

(大連理工大學(xué)管理與經(jīng)濟(jì)學(xué)部 遼寧 大連 116024)

Event-Condition-Action(ECA)規(guī)則的評估和執(zhí)行獨(dú)立于其他規(guī)則，但規(guī)則行為間交互作用可能導(dǎo)致系統(tǒng)行為不可預(yù)測或不安全。典型的問題有規(guī)則的不一致性和終止性。針對上述問題，提出將ECA規(guī)則轉(zhuǎn)換為時(shí)間自動機(jī)，對規(guī)則之間的交互進(jìn)行分析。采用時(shí)間自動機(jī)驗(yàn)證工具UPPAAL驗(yàn)證規(guī)則集合是否存在交互問題。以癡呆老人智能輔助系統(tǒng)為例，實(shí)驗(yàn)結(jié)果證明了該方法的可行性和有效性。

ECA規(guī)則 時(shí)間自動機(jī) 轉(zhuǎn)換 UPPAAL

0 引 言

Event-Condition-Action(ECA)規(guī)則[1]首先在主動數(shù)據(jù)庫技術(shù)提出，目前已應(yīng)用于相關(guān)領(lǐng)域，例如：普適計(jì)算環(huán)境下情境感知系統(tǒng)[2]、工作流[3]、物聯(lián)網(wǎng)數(shù)據(jù)分析平臺[4]等。ECA規(guī)則形式如下：On If Do，ECA規(guī)則含義是當(dāng)檢測到事件發(fā)生時(shí)，如果條件成立，則執(zhí)行動作。ECA規(guī)則特點(diǎn)如下：

(1) 規(guī)則由事件激活；

(2) 自動執(zhí)行并且獨(dú)立于系統(tǒng)中其他規(guī)則；

(3) 包含一個保衛(wèi)條件用來執(zhí)行相應(yīng)的行為。

由于ECA規(guī)則特點(diǎn)導(dǎo)致ECA規(guī)則在執(zhí)行過程中規(guī)則間行為交互產(chǎn)生多種問題[5]，典型的問題有：

(1) 冗余性：系統(tǒng)中有兩條或兩條以上的規(guī)則的功能是重復(fù)的，造成原因可能是由于規(guī)則由不同的人員編寫導(dǎo)致。

(2) 不一致性：常會發(fā)生在多條規(guī)則在同一時(shí)間激活，相互矛盾的行為發(fā)給相同的設(shè)備時(shí)會出現(xiàn)不一致性。它們的執(zhí)行順序會導(dǎo)致系統(tǒng)出現(xiàn)不同的狀態(tài)。

(3) 終止性：規(guī)則集合可能無法正常終止。

如果沒有檢測到以上問題并作相應(yīng)處理，就會造成規(guī)則交互問題。本文目標(biāo)就是在ECA規(guī)則系統(tǒng)運(yùn)行之前提供有效的驗(yàn)證，在系統(tǒng)運(yùn)行之前驗(yàn)證系統(tǒng)是否存在上述問題。對于ECA規(guī)則存在的交互問題，Zhang 等[5]首先定義了冗余性、不一致性以及終止性等問題，并且基于這三種問題提出了三層結(jié)構(gòu)，第一層考慮規(guī)則集合，第二層考慮行動的執(zhí)行對規(guī)則造成影響，第三層考慮周圍環(huán)境所有可能的響應(yīng)，根據(jù)需要的信息的不同在不同的層次執(zhí)行某些驗(yàn)證。張立臣等[6]建立了一種可描述ECA規(guī)則集的擴(kuò)展Petri網(wǎng)EPN(extended Petri net)模型,在此基礎(chǔ)上研究并提出了一種ECA規(guī)則集終止性判定算法。Jin等[7]提出一種動態(tài)分析ECA規(guī)則的方法，該方法首先將ECA規(guī)則轉(zhuǎn)換為拓展Petri網(wǎng)，然后通過分析Petri網(wǎng)的性質(zhì)來分析規(guī)則間的動態(tài)行為。Cano等[8]針對目前存在的分布式設(shè)備都有自己的配置規(guī)則，容易導(dǎo)致規(guī)則間的沖突，故提出一種用工具來監(jiān)測和解決基于ECA規(guī)則的系統(tǒng)，但是該文只是描述架構(gòu)沒有真正的實(shí)施。Schordan等[9]提出了一種組合方法用來驗(yàn)證規(guī)則集合，該方法假定規(guī)則集合為有限狀態(tài)空間，通過系統(tǒng)分析狀態(tài)空間和狀態(tài)變遷用以分析規(guī)則集合可達(dá)屬性和行為屬性。

上述工作主要通過語義分析、算法和Petri網(wǎng)等方法分析規(guī)則的冗余性和不一致性等問題，一定程度上解決了規(guī)則靜態(tài)分析驗(yàn)證問題，然而由于規(guī)則之間交互導(dǎo)致分析一系列ECA規(guī)則是一個復(fù)雜的任務(wù)，例如：一個規(guī)則可能觸發(fā)其他規(guī)則，導(dǎo)致連鎖反應(yīng)。而且由于缺乏成熟的工具做支撐，驗(yàn)證需要耗費(fèi)一定時(shí)間，如果規(guī)則集合規(guī)模較大，則所用時(shí)間較長不符合實(shí)際業(yè)務(wù)需求。

針對以上方法不足，本文采用形式化方法時(shí)間自動機(jī)理論，將驗(yàn)證的規(guī)則轉(zhuǎn)換為時(shí)間自動機(jī)模型。通過時(shí)間自動機(jī)模型模擬仿真規(guī)則的評估和執(zhí)行，用來對規(guī)則進(jìn)行動態(tài)分析。通過基于時(shí)間自動機(jī)理論的模型驗(yàn)證工具UPPAAL[10]中流程活性和安全性等用來驗(yàn)證規(guī)則集合中是否存在不一致性和終止性等問題，為后期系統(tǒng)的改進(jìn)提供幫助。

1 時(shí)間自動機(jī)理論及驗(yàn)證工具

1.1 時(shí)間自動機(jī)

時(shí)間自動機(jī)是最早是由Alur等[11]提出的，是一種用來描述和分析實(shí)時(shí)系統(tǒng)行為的形式化模型，是基于有限狀態(tài)自動機(jī)基礎(chǔ)上拓展時(shí)間變量，用來刻畫實(shí)時(shí)系統(tǒng)連續(xù)變化的時(shí)間行為，目前已經(jīng)研發(fā)多種仿真及驗(yàn)證工具，如UPPAAL，這些工具為時(shí)間自動機(jī)的模擬仿真和驗(yàn)證提供了有力的支持。時(shí)間自動機(jī)定義如下：

定義 一個時(shí)間自動機(jī)可以表示為一個七元組TA=(S,S0,A,C,V,G,E)，其中S(State)表示有限狀態(tài)集合；S0∈S表示初始狀態(tài)；A(Act)動作的集合，包括輸入、輸出和內(nèi)部三類動作；C(Clock)時(shí)鐘變量集合；V(varchar)數(shù)據(jù)變量集合；G(guard)稱為保衛(wèi)公式，由變量集合、基本運(yùn)算符和比較運(yùn)算符按一定語法構(gòu)成；E(Edge)表示從一個狀態(tài)到另一個狀態(tài)的有向邊。時(shí)間自動機(jī)之間不能通過信道進(jìn)行傳值通信，因?yàn)檩斎牒洼敵鰟幼鳑]有附加任何數(shù)值和變量，但可以通過共享變量的方式來實(shí)現(xiàn)同步傳值通信，多個并發(fā)的時(shí)間自動機(jī)可以構(gòu)成一個時(shí)間自動機(jī)網(wǎng)絡(luò)，同一網(wǎng)絡(luò)中多個時(shí)間自動機(jī)共享一些時(shí)鐘變量和數(shù)據(jù)變量，但都有各自的狀態(tài)。

1.2UPPAAL

基于時(shí)間自動機(jī)理論的模型檢測形式化工具UPPAAL由丹麥的Aalborg大學(xué)和瑞典的Uppsala大學(xué)聯(lián)合開發(fā)。工具主要通過窮舉被檢驗(yàn)系統(tǒng)的狀態(tài)空間和時(shí)間約束來驗(yàn)證特定的屬性，驗(yàn)證屬性包括以下三個主要方面，可達(dá)性(即對于一個給定的狀態(tài)是否能夠到達(dá))、安全性(即驗(yàn)證是否存在死鎖等問題)和流程活性(即驗(yàn)證某些特定的屬性是否會發(fā)生)。

2 ECA規(guī)則到時(shí)間自動機(jī)映射方法

時(shí)間自動機(jī)是由許多相互作用的自動機(jī)構(gòu)成，每個自動機(jī)模型都可以模擬一個過程的執(zhí)行，由于ECA規(guī)則中規(guī)則和事件可以在不同的線程內(nèi)執(zhí)行，故本文采用分別將事件和規(guī)則映射為時(shí)間自動機(jī)。這種映射方法具有良好的柔性，轉(zhuǎn)換的規(guī)則和事件都可以分別驗(yàn)證。此外，該方法還具有很多的拓展性，例如：額外增加的操作符、不同語義的規(guī)則執(zhí)行都可以很容易地整合到目前的模型中。

2.1 事件映射

本文將事件類型Ei映射為時(shí)間自動機(jī)中動作，Ei!表示接收事件，Ei?表示發(fā)送事件。事件發(fā)生建模一個時(shí)間自動機(jī)，在沒有限制情況下，事件可以在任何時(shí)間以任意次序發(fā)生，圖1代表事件類型Ea、Eb發(fā)生時(shí)構(gòu)建時(shí)間自動機(jī)模型。

圖1 事件映射

2.2 條件和行動映射

本文將ECA規(guī)則中Condition映射為時(shí)間自動機(jī)中保衛(wèi)公式(Guard)，Action映射為時(shí)間自動機(jī)中有向邊(Edge)中的方法。規(guī)則的優(yōu)先級映射為時(shí)間自動機(jī)中的數(shù)據(jù)變量(Varchar)，數(shù)據(jù)變量從1到10，1代表最高優(yōu)先級，10代表最低優(yōu)先級，下面以具體規(guī)則說明映射過程：

Rule1 S0 to S1 (priority==1)

ON EarriveToS0

DO action S0toS1()

Rule2 S1 to S2 (priority==2)

ON EarriveToS1

IF guard==true

DO action S1toS2()

Rule3 S1 toS3 (priority==2)

ON EarriveToS1

IF guard==false

DO action S1toS3()

規(guī)則對應(yīng)的時(shí)間自動機(jī)如圖2所示。規(guī)則1執(zhí)行后狀態(tài)S0轉(zhuǎn)移至S1，規(guī)則1的行動產(chǎn)生的事件觸發(fā)規(guī)則2和規(guī)則3，兩條規(guī)則根據(jù)評估條件選擇其中之一執(zhí)行，當(dāng)條件guard==true，執(zhí)行行動action S1toS2，狀態(tài)轉(zhuǎn)移至S2，當(dāng)條件guard==false，執(zhí)行行動action S1toS3，狀態(tài)轉(zhuǎn)移至S3。

圖2 條件和行動映射

2.3 規(guī)則映射

規(guī)則映射和事件映射遵循相同的原則，事件觸發(fā)規(guī)則發(fā)生時(shí)，規(guī)則的狀態(tài)從空閑狀態(tài)到激活狀態(tài)，評估條件是否滿足然后執(zhí)行。為了檢測規(guī)則集合間是否存在不一致性和終止性等問題，分別建模規(guī)則調(diào)度自動機(jī)和規(guī)則執(zhí)行自動機(jī)。

2.3.1 規(guī)則調(diào)度自動機(jī)

規(guī)則調(diào)度自動機(jī)中事件的發(fā)生根據(jù)某種排序策略(例如：先進(jìn)先出)進(jìn)行注冊，事件發(fā)生時(shí)狀態(tài)由初始狀態(tài)轉(zhuǎn)移至執(zhí)行狀態(tài)，在執(zhí)行狀態(tài)中評估條件后，按照規(guī)則的優(yōu)先性執(zhí)行規(guī)則，圖3是一個規(guī)則調(diào)度自動機(jī)例子。當(dāng)接收到事件Ea!或接收到事件Eb!，狀態(tài)由初始狀態(tài)轉(zhuǎn)移至執(zhí)行狀態(tài)，在執(zhí)行狀態(tài)中事件Ea觸發(fā)規(guī)則R2，事件Eb觸發(fā)規(guī)則R1，計(jì)數(shù)變量R1c和R2c用來確保每條規(guī)則只有執(zhí)行一次。

圖3 規(guī)則調(diào)度自動機(jī)

2.3.2 規(guī)則執(zhí)行自動機(jī)

規(guī)則執(zhí)行自動機(jī)開始處于初始狀態(tài)等待觸發(fā)事件發(fā)生，當(dāng)檢測到事件發(fā)生，初始狀態(tài)轉(zhuǎn)移至激活狀態(tài)(與此同時(shí)調(diào)度自動機(jī)進(jìn)入執(zhí)行狀態(tài))，規(guī)則自動機(jī)評估執(zhí)行條件(條件映射為激活狀態(tài)和評估狀態(tài)之間的保衛(wèi)公式)，如果評估條件為真，規(guī)則自動機(jī)轉(zhuǎn)移至評估狀態(tài)，如果評估條件為假，規(guī)則自動機(jī)轉(zhuǎn)移至初始狀態(tài)。規(guī)則的執(zhí)行包含三種不同的活動，執(zhí)行行為、執(zhí)行時(shí)間和產(chǎn)生新的事件。執(zhí)行行為指的是ECA規(guī)則中A(action)，執(zhí)行時(shí)間指的是規(guī)則執(zhí)行在限定的時(shí)間內(nèi)執(zhí)行，圖4是一個規(guī)則執(zhí)行自動機(jī)例子。當(dāng)執(zhí)行自動機(jī)進(jìn)入評估狀態(tài)后，執(zhí)行時(shí)間指的是當(dāng)extime(執(zhí)行時(shí)間)==time(時(shí)鐘變量)條件為真后才能進(jìn)入執(zhí)行狀態(tài)，在執(zhí)行狀態(tài)中如果規(guī)則的行動部分觸發(fā)新的事件發(fā)生，計(jì)數(shù)變量ca用來確保觸發(fā)事件的正確性。

圖4 規(guī)則執(zhí)行自動機(jī)

3 案例分析

目前人口老齡化的問題已成為社會關(guān)注熱點(diǎn)，老年癡呆癥發(fā)病率逐年提高，癡呆老人的看護(hù)和照顧給家人和社會帶來較大的負(fù)擔(dān)，加上看護(hù)者本身缺乏相關(guān)醫(yī)療護(hù)理經(jīng)驗(yàn)，使得癡呆老人看護(hù)質(zhì)量不高[12]。隨著普適計(jì)算和情境感知等新技術(shù)的興起給傳統(tǒng)的醫(yī)療看護(hù)模式帶來了革新，下面我們以AMUPADH Healthcare System[13]為例來驗(yàn)證本文提出的方法，該系統(tǒng)用來監(jiān)測和輔助上了年紀(jì)的癡呆病人的日常生活。年紀(jì)大的癡呆病人通常記憶衰退并且經(jīng)常忘記日常生活中基本活動，系統(tǒng)使用活動識別技術(shù)(傳感器和推理ECA規(guī)則)用來監(jiān)測病人的行為并且通過制動器例如：揚(yáng)聲器等發(fā)出提醒。目前應(yīng)用于智能臥室(臥室里安裝多種傳感器獲取周圍環(huán)境信息)，臥室里兩張床和一套洗浴設(shè)備。系統(tǒng)共有三部分組成。

第一部分：環(huán)境數(shù)據(jù)獲取，系統(tǒng)中應(yīng)用多種傳感器獲取周圍環(huán)境信息，例如：如果病人關(guān)掉淋浴頭，震動傳感器將會被觸發(fā)，改變狀態(tài)。系統(tǒng)中共有如下三種主要的傳感器，RFID reader：用來識別和跟蹤病人的位置信息，系統(tǒng)中每個病人佩戴一個RFID手環(huán)。壓力傳感器：用來監(jiān)測床上活動，例如：坐著或躺著。震動傳感器：用來監(jiān)測震動，用來感知使用水龍頭和肥皂。

第二部分：情境的處理和推理(ECA規(guī)則)，系統(tǒng)接收到傳感器上傳的情境信息(此情境信息為低級情境信息)，通過對情境信息的處理和推理后形成高級情境信息即活動，這個任務(wù)執(zhí)行通過評估預(yù)先定義的活動識別規(guī)則，這些規(guī)則制定是基于用戶行為的先驗(yàn)知識。ECA推理規(guī)則集合如表1所示，例如：一個典型的規(guī)則如下，如果壓力傳感器改變狀態(tài)為sitting，并且持續(xù)時(shí)間超過30分鐘，一個不正常的活動，即床上坐的時(shí)間過長產(chǎn)生。

第三部分：提醒服務(wù)，系統(tǒng)中提供6種基本的提醒服務(wù)用來幫助病人，提醒服務(wù)如下：

1) 使用錯誤的床：上了年紀(jì)的人，尤其是癡呆的病人很容易上錯床。

2) 坐在床上的時(shí)間太久：病人經(jīng)常出現(xiàn)失眠癥狀，他們很容易被周圍的環(huán)境打擾和激怒，一個典型的癥狀就是病人經(jīng)常在午夜起床，長時(shí)間坐在床上，直到護(hù)士或看護(hù)者協(xié)助后才能繼續(xù)入睡。

3) 洗澡沒有使用肥皂：病人由于記憶的缺少，時(shí)常忘記日?；顒拥膱?zhí)行步驟，在洗浴活動中，病人在打開水龍頭后忘記下一步要做什么，據(jù)護(hù)士報(bào)告一些病人洗澡很快，但是沒有使用肥皂，考慮到病人的個人衛(wèi)生，病人呈現(xiàn)的行為需要得到幫助。

4) 洗澡時(shí)間過長：一些病人站在淋浴頭下面很長時(shí)間，一個關(guān)鍵問題是淋浴時(shí)間過長容易導(dǎo)致病人虛脫，如果處理不及時(shí)容易出現(xiàn)危險(xiǎn)。

5) 忘記關(guān)掉水龍頭：癡呆病人淋浴后經(jīng)常忘記關(guān)掉水龍頭，為了節(jié)約水，這個情景也應(yīng)該被監(jiān)測并在系統(tǒng)提醒。

6) 浴室徘徊：病人在洗澡過程中忘記了洗澡的步驟，因此，會出現(xiàn)一個典型癥狀就是在浴室徘徊的行為，這種行為需要得到協(xié)助。

表1 ECA規(guī)則集合

續(xù)表1

系統(tǒng)通過傳感器感知周圍環(huán)境信息觸發(fā)執(zhí)行ECA規(guī)則，根據(jù)上文提出的ECA規(guī)則轉(zhuǎn)換方法，使用時(shí)間自動機(jī)建模驗(yàn)證工具UPPAAL，將上述ECA規(guī)則集合轉(zhuǎn)換為對應(yīng)的時(shí)間自動機(jī)模型，時(shí)間自動機(jī)模型部分如圖5所示。

圖5 癡呆老人智能輔助系統(tǒng)時(shí)間自動機(jī)網(wǎng)模型

使用UPPAAL對該模型進(jìn)行活性和安全性分析驗(yàn)證，從而驗(yàn)證系統(tǒng)推理ECA規(guī)則集合是否存在終止性和不一致性問題。

(1) 不一致性問題驗(yàn)證(活性驗(yàn)證)

形式化描述，例如：

A[]Rule(Person lying on wrong bed)+Rule(Person sat on Bed for too long)≤1

檢測類型及結(jié)果如表2所示，從表中的實(shí)驗(yàn)結(jié)果我們可以發(fā)現(xiàn)有很多種情況導(dǎo)致規(guī)則間出現(xiàn)不一致性問題。例如：當(dāng)老人在浴室徘徊的時(shí)候觸發(fā)執(zhí)行徘徊提醒規(guī)則，然后他忽略徘徊提醒然后打開淋浴玩水(癡呆老人典型癥狀)，打開淋浴一段時(shí)間后觸發(fā)執(zhí)行沒有使用肥皂的提醒規(guī)則，因此導(dǎo)致系統(tǒng)同一時(shí)間內(nèi)觸發(fā)兩條提醒規(guī)則。

表2 不一致性問題檢測列表

(2) 終止性問題驗(yàn)證(安全性驗(yàn)證)

形式化描述：A[] not deadlock

驗(yàn)證結(jié)果：安全性驗(yàn)證結(jié)果表明模型不存在死鎖問題，即系統(tǒng)推理規(guī)則集合不存在終止性問題。

模型驗(yàn)證會窮盡研究模型的所有可能狀態(tài)空間，對于所有的模型驗(yàn)證方法來說一個關(guān)鍵的問題就是內(nèi)存限制和狀態(tài)爆炸問題[14]，本方法驗(yàn)證使用的內(nèi)存如表3所示。

表3 驗(yàn)證評估結(jié)果

通過表3結(jié)果得知使用本方法分析和驗(yàn)證ECA規(guī)則集合使用的內(nèi)存量較小，因此使用本方法建模和分析ECA規(guī)則能夠在系統(tǒng)正式實(shí)施前有效地發(fā)現(xiàn)集合中規(guī)則交互問題并且具有較高的效率。

4 結(jié) 語

基于ECA規(guī)則建模的系統(tǒng)以其靈活、使用方便等特點(diǎn)已經(jīng)應(yīng)用于相關(guān)領(lǐng)域，但是由于規(guī)則間的交互問題導(dǎo)致還沒有在工業(yè)領(lǐng)域得到廣泛的應(yīng)用。本文從實(shí)際需求出發(fā)，提出將ECA規(guī)則轉(zhuǎn)換為相應(yīng)的時(shí)間自動機(jī)模型，利用形式化方法成熟的驗(yàn)證工具對規(guī)則系統(tǒng)進(jìn)行分析、驗(yàn)證，充分發(fā)揮ECA規(guī)則建模方面的優(yōu)勢，同時(shí)利用時(shí)間自動機(jī)驗(yàn)證方面的優(yōu)勢。

本文提出的方法還有不足之處，在今后的工作中，還需要進(jìn)一步對方法進(jìn)行優(yōu)化和改進(jìn)，提高方法的有效性和實(shí)用性。

[1] Dittrich K R,Gatziu S,Geppert A.The active database management system manifesto:a rulebase of ADBMS features[C]//Second Workshop on Rules in Database Systems.Springer,1995:1-17.

[2] 盧濤,劉曉伶.普適服務(wù)沖突檢測方法研究[J].哈爾濱工程大學(xué)學(xué)報(bào),2013,34(11):1402-1408.

[3] 孫政.一種基于ECA規(guī)則的審批工作流模型的淺析[J].電子技術(shù)與軟件工程,2015(15):77-79.

[4] 耿盼盼,丁香乾,陶冶,等.一種通用物聯(lián)網(wǎng)數(shù)據(jù)分析平臺的設(shè)計(jì)與實(shí)現(xiàn)[J].計(jì)算機(jī)應(yīng)用與軟件,2013,30(11):115-118.

[5] Zhang J,Moyne J,Tilbury D.Verification of ECA rule based management and control systems[C]//2008 IEEE International Conference on Automation Science and Engineering,2008:1-7.

[6] 張立臣,王小明,竇文陽.基于擴(kuò)展Petri網(wǎng)的ECA規(guī)則集表示及終止性分析[J].通信學(xué)報(bào),2013,34(3):157-164.

[7] Jin X,Lembachar Y,Ciardo G.Symbolic termination and confluence checking for ECA rules[M]//Transactions on Petri Nets and Other Models of Concurrency IX.Springer,2014:99-123.

[8] Cano J,Delaval G,Rutten E.Coordination of ECA rules by verification and control[C]//Proceedings of the 16th IFIP WG 6.1 International Conference on Coordination Models and Languages.Springer,2014:33-48.

[9] Schordan M,Prantl A.Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges[J].International Journal on Software Tools for Technology Transfer,2014,16(5):493-505.

[10] Larsen K G,Pettersson P,Yi W.UPPAAL in a nutshell[J].International Journal on Software Tools for Technology Transfer (STTT),1997,1(1):134-152.

[11] Alur R,Dill D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(2):183-235.

[12] Lotfi A,Langensiepen C,Mahmoud S M,et al.Smart homes for the elderly dementia sufferers:identification and prediction of abnormal behaviour[J].Journal of Ambient Intelligence and Humanized Computing,2012,3(3):205-218.

[13] Moshnyaga V,Osamu T,Ryu T,et al.An intelligent system for assisting family caregivers of dementia people[C]//Computational Intelligence in Healthcare and e-health (CICARE),2014 IEEE Symposium on.IEEE,2014:85-89.

[14] 侯剛,周寬久,勇嘉偉,等.模型檢測中狀態(tài)爆炸問題研究綜述[J].計(jì)算機(jī)科學(xué),2013,40(6A):77-86,111.

RESEARCH ON ECA RULES INTERACTION PROBLEMS BASED ON TIMED AUTOMATA

Zhao Xin Lu Tao

(FacultyofManagementandEconomics,DalianUniversityofTechnology,Dalian116024,Liaoning,China)

The evaluation and execution of each Event-Condition-Action (ECA) rule is considered to be independent from the others. But interactions of rule actions can cause the system behaviors to be unpredictable or unsafe. Typical problems are inconsistencies, and termination problems among rules. In response to these problems, the ECA rule is proposed to be converted into timed automata to analyze the interaction of rules. Then, a verification tool of timed automata which is named UPPAAL is used to verify the interaction problem among the rules set. A case of smart assisting system for dementia is used to prove this method. Experimental results demonstrate the feasibility and effectiveness of this method.

ECA rules Timed automata Conversion UPPAAL

2015-12-04。國家自然科學(xué)基金項(xiàng)目(71271038)。趙鑫，碩士生，主研領(lǐng)域：時(shí)間自動機(jī)建模與仿真。盧濤，副教授。

TP391

A

10.3969/j.issn.1000-386x.2017.02.013