基于時間自動機的ECA規則交互問題研究

趙 鑫 盧 濤

(大連理工大學管理與經濟學部 遼寧 大連 116024)

基于時間自動機的ECA規則交互問題研究

趙 鑫 盧 濤

(大連理工大學管理與經濟學部 遼寧 大連 116024)

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

ECA規則 時間自動機 轉換 UPPAAL

0 引 言

Event-Condition-Action(ECA)規則[1]首先在主動數據庫技術提出，目前已應用于相關領域，例如：普適計算環境下情境感知系統[2]、工作流[3]、物聯網數據分析平臺[4]等。ECA規則形式如下：On If Do，ECA規則含義是當檢測到事件發生時，如果條件成立，則執行動作。ECA規則特點如下：

(1) 規則由事件激活；

(2) 自動執行并且獨立于系統中其他規則；

(3) 包含一個保衛條件用來執行相應的行為。

由于ECA規則特點導致ECA規則在執行過程中規則間行為交互產生多種問題[5]，典型的問題有：

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

(2) 不一致性：常會發生在多條規則在同一時間激活，相互矛盾的行為發給相同的設備時會出現不一致性。它們的執行順序會導致系統出現不同的狀態。

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

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

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

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

1 時間自動機理論及驗證工具

1.1 時間自動機

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

定義 一個時間自動機可以表示為一個七元組TA=(S,S0,A,C,V,G,E)，其中S(State)表示有限狀態集合；S0∈S表示初始狀態；A(Act)動作的集合，包括輸入、輸出和內部三類動作；C(Clock)時鐘變量集合；V(varchar)數據變量集合；G(guard)稱為保衛公式，由變量集合、基本運算符和比較運算符按一定語法構成；E(Edge)表示從一個狀態到另一個狀態的有向邊。時間自動機之間不能通過信道進行傳值通信，因為輸入和輸出動作沒有附加任何數值和變量，但可以通過共享變量的方式來實現同步傳值通信，多個并發的時間自動機可以構成一個時間自動機網絡，同一網絡中多個時間自動機共享一些時鐘變量和數據變量，但都有各自的狀態。

1.2UPPAAL

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

2 ECA規則到時間自動機映射方法

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

2.1 事件映射

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

圖1 事件映射

2.2 條件和行動映射

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

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()

規則對應的時間自動機如圖2所示。規則1執行后狀態S0轉移至S1，規則1的行動產生的事件觸發規則2和規則3，兩條規則根據評估條件選擇其中之一執行，當條件guard==true，執行行動action S1toS2，狀態轉移至S2，當條件guard==false，執行行動action S1toS3，狀態轉移至S3。

圖2 條件和行動映射

2.3 規則映射

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

2.3.1 規則調度自動機

規則調度自動機中事件的發生根據某種排序策略(例如：先進先出)進行注冊，事件發生時狀態由初始狀態轉移至執行狀態，在執行狀態中評估條件后，按照規則的優先性執行規則，圖3是一個規則調度自動機例子。當接收到事件Ea!或接收到事件Eb!，狀態由初始狀態轉移至執行狀態，在執行狀態中事件Ea觸發規則R2，事件Eb觸發規則R1，計數變量R1c和R2c用來確保每條規則只有執行一次。

圖3 規則調度自動機

2.3.2 規則執行自動機

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

圖4 規則執行自動機

3 案例分析

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

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

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

第三部分：提醒服務，系統中提供6種基本的提醒服務用來幫助病人，提醒服務如下：

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

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

3) 洗澡沒有使用肥皂：病人由于記憶的缺少，時常忘記日常活動的執行步驟，在洗浴活動中，病人在打開水龍頭后忘記下一步要做什么，據護士報告一些病人洗澡很快，但是沒有使用肥皂，考慮到病人的個人衛生，病人呈現的行為需要得到幫助。

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

5) 忘記關掉水龍頭：癡呆病人淋浴后經常忘記關掉水龍頭，為了節約水，這個情景也應該被監測并在系統提醒。

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

表1 ECA規則集合

續表1

系統通過傳感器感知周圍環境信息觸發執行ECA規則，根據上文提出的ECA規則轉換方法，使用時間自動機建模驗證工具UPPAAL，將上述ECA規則集合轉換為對應的時間自動機模型，時間自動機模型部分如圖5所示。

圖5 癡呆老人智能輔助系統時間自動機網模型

使用UPPAAL對該模型進行活性和安全性分析驗證，從而驗證系統推理ECA規則集合是否存在終止性和不一致性問題。

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

形式化描述，例如：

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

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

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

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

形式化描述：A[] not deadlock

驗證結果：安全性驗證結果表明模型不存在死鎖問題，即系統推理規則集合不存在終止性問題。

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

表3 驗證評估結果

通過表3結果得知使用本方法分析和驗證ECA規則集合使用的內存量較小，因此使用本方法建模和分析ECA規則能夠在系統正式實施前有效地發現集合中規則交互問題并且具有較高的效率。

4 結 語

基于ECA規則建模的系統以其靈活、使用方便等特點已經應用于相關領域，但是由于規則間的交互問題導致還沒有在工業領域得到廣泛的應用。本文從實際需求出發，提出將ECA規則轉換為相應的時間自動機模型，利用形式化方法成熟的驗證工具對規則系統進行分析、驗證，充分發揮ECA規則建模方面的優勢，同時利用時間自動機驗證方面的優勢。

本文提出的方法還有不足之處，在今后的工作中，還需要進一步對方法進行優化和改進，提高方法的有效性和實用性。

[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] 盧濤,劉曉伶.普適服務沖突檢測方法研究[J].哈爾濱工程大學學報,2013,34(11):1402-1408.

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

[4] 耿盼盼,丁香乾,陶冶,等.一種通用物聯網數據分析平臺的設計與實現[J].計算機應用與軟件,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] 張立臣,王小明,竇文陽.基于擴展Petri網的ECA規則集表示及終止性分析[J].通信學報,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] 侯剛,周寬久,勇嘉偉,等.模型檢測中狀態爆炸問題研究綜述[J].計算機科學,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。國家自然科學基金項目(71271038)。趙鑫，碩士生，主研領域：時間自動機建模與仿真。盧濤，副教授。

TP391

A

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