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

趙 鑫 盧 濤

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

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

趙 鑫 盧 濤

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

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

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

0 引 言

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

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

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

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

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

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

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

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

如果沒(méi)有檢測(cè)到以上問(wèn)題并作相應(yīng)處理，就會(huì)造成規(guī)則交互問(wèn)題。本文目標(biāo)就是在ECA規(guī)則系統(tǒng)運(yùn)行之前提供有效的驗(yàn)證，在系統(tǒng)運(yùn)行之前驗(yàn)證系統(tǒng)是否存在上述問(wèn)題。對(duì)于ECA規(guī)則存在的交互問(wèn)題，Zhang 等[5]首先定義了冗余性、不一致性以及終止性等問(wèn)題，并且基于這三種問(wèn)題提出了三層結(jié)構(gòu)，第一層考慮規(guī)則集合，第二層考慮行動(dòng)的執(zhí)行對(duì)規(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]提出一種動(dòng)態(tài)分析ECA規(guī)則的方法，該方法首先將ECA規(guī)則轉(zhuǎn)換為拓展Petri網(wǎng)，然后通過(guò)分析Petri網(wǎng)的性質(zhì)來(lái)分析規(guī)則間的動(dòng)態(tài)行為。Cano等[8]針對(duì)目前存在的分布式設(shè)備都有自己的配置規(guī)則，容易導(dǎo)致規(guī)則間的沖突，故提出一種用工具來(lái)監(jiān)測(cè)和解決基于ECA規(guī)則的系統(tǒng)，但是該文只是描述架構(gòu)沒(méi)有真正的實(shí)施。Schordan等[9]提出了一種組合方法用來(lái)驗(yàn)證規(guī)則集合，該方法假定規(guī)則集合為有限狀態(tài)空間，通過(guò)系統(tǒng)分析狀態(tài)空間和狀態(tài)變遷用以分析規(guī)則集合可達(dá)屬性和行為屬性。

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

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

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

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

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

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

1.2UPPAAL

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

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

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

2.1 事件映射

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

圖1 事件映射

2.2 條件和行動(dòng)映射

本文將ECA規(guī)則中Condition映射為時(shí)間自動(dòng)機(jī)中保衛(wèi)公式(Guard)，Action映射為時(shí)間自動(dòng)機(jī)中有向邊(Edge)中的方法。規(guī)則的優(yōu)先級(jí)映射為時(shí)間自動(dòng)機(jī)中的數(shù)據(jù)變量(Varchar)，數(shù)據(jù)變量從1到10，1代表最高優(yōu)先級(jí)，10代表最低優(yōu)先級(jí)，下面以具體規(guī)則說(shuō)明映射過(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ī)則對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)如圖2所示。規(guī)則1執(zhí)行后狀態(tài)S0轉(zhuǎn)移至S1，規(guī)則1的行動(dòng)產(chǎn)生的事件觸發(fā)規(guī)則2和規(guī)則3，兩條規(guī)則根據(jù)評(píng)估條件選擇其中之一執(zhí)行，當(dāng)條件guard==true，執(zhí)行行動(dòng)action S1toS2，狀態(tài)轉(zhuǎn)移至S2，當(dāng)條件guard==false，執(zhí)行行動(dòng)action S1toS3，狀態(tài)轉(zhuǎn)移至S3。

圖2 條件和行動(dòng)映射

2.3 規(guī)則映射

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

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

規(guī)則調(diào)度自動(dòng)機(jī)中事件的發(fā)生根據(jù)某種排序策略(例如：先進(jìn)先出)進(jìn)行注冊(cè)，事件發(fā)生時(shí)狀態(tài)由初始狀態(tài)轉(zhuǎn)移至執(zhí)行狀態(tài)，在執(zhí)行狀態(tài)中評(píng)估條件后，按照規(guī)則的優(yōu)先性執(zhí)行規(guī)則，圖3是一個(gè)規(guī)則調(diào)度自動(dòng)機(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用來(lái)確保每條規(guī)則只有執(zhí)行一次。

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

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

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

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

3 案例分析

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

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

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

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

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

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

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

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

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

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

表1 ECA規(guī)則集合

續(xù)表1

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

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

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

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

形式化描述，例如：

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

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

表2 不一致性問(wèn)題檢測(cè)列表

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

形式化描述：A[] not deadlock

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

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

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

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

4 結(jié) 語(yǔ)

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

本文提出的方法還有不足之處，在今后的工作中，還需要進(jìn)一步對(duì)方法進(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ù)沖突檢測(cè)方法研究[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ù)分析平臺(tái)的設(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] 張立臣,王小明,竇文陽(yáng).基于擴(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] 侯剛,周寬久,勇嘉偉,等.模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[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。國(guó)家自然科學(xué)基金項(xiàng)目(71271038)。趙鑫，碩士生，主研領(lǐng)域：時(shí)間自動(dòng)機(jī)建模與仿真。盧濤，副教授。

TP391

A

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