時序邏輯在有效性控制中的應用研究

劉磊

(廣東工業大學，廣東廣州510006)

1.引言

作為宇宙間所有事物具有的一種屬性，時間貫穿著事物的發展過程。各式各樣與時間緊密相關的數據、信息及其聯系無不深深影響著人類社會生活的方方面面。在日常事務的處理過程中，人們不僅僅需要關注數據和信息本身，更要了解和研究它們在影響事務處理的時序、有效性等時間問題。在工作流系統中，各種事務同樣有時間屬性[1]。有些事務在一個時間段內是有效的，而超出這個時間段就是無效的。比如在采購系統中，規定下訂單后的一周內雙方必須簽合同，如果一周內雙方沒有簽署，那么該訂單就是無效的；有的系統還會規定在每個季度的最后一個工作日提交統計報表。這些事務都是與時間有緊密關系的。

工作流系統中活動的有效性可分為兩種：一種是由工作流邏輯結構和活動執行延遲而產生的，如一個活動必須在其所有前序活動完成時才能啟動；另一種是由過程設計者根據業務策略及法律法規來設定，如某個事件必須要在某個日期前完成，在某個月某個固定日期執行某個動作等。后一個有效性是與時間因素有關的，在本文中我們只研究后者，考慮如何有效地控制各事務的時間屬性，以保證工作流系統中各事務按時有序地完成。

2.CTL基本概念

本文中將采用的時序邏輯是計算樹邏輯(Computation Tree Logic，CTL)，CTL是一種分支時序邏輯[2]。它的時間模型是一個樹狀結構，未來有不同的路徑，其中任何一個都可能是現實的實際路徑。由于行為的不確定性，它可以有多個可能的后繼狀態，每個這樣的狀態又可以有多個可能的后繼狀態，依此類推可以產生一顆狀態樹。

定義1 CTL有下列用Backus-Naur范式給出的語法：

其中p是取自某原子集的任意命題原子。

3.有效性約束的建模

[3]提出了工作流系統中時序約束的三種主要形式，根據這里對有效性的定義，以及在實際系統中碰到的有關時間有效性的問題，可以把時間有效性約束歸納分成以下三類：

(1)最長時間距離約束：指活動A和其后繼活動B之間的時間距離最長不能超過某一指定時間值。如本文剛開始提到的下訂單后的一周內必須簽署合同，否則逾期訂單失效，就屬于此類約束。

(2)最短時間距離約束：指活動A和其后繼活動B之間的時間距離最短不能小于某一指定時間值。如在采購系統中，中標公告必須公示一段時間后，采購雙方才能簽訂合同。

(3)固定時間約束：在固定的日期執行某些活動。如每月的第一個周一系統自動發布職位空缺公告。

為了對時間有效性約束建模，在一階邏輯系統中定義常量Start，End，I，J，K，…分別表示工作流的開始節點、結束節點以及工作流模型中的各項活動，系統中變量的定義如下：

(1)向量s[k]，k=0，1，…，n+1，其中，n是工作流模型中除去開始和結束節點外的實際活動數量，s[k]取1或0，分別表示活動處于執行或非執行狀態。

(2)全局時鐘變量c，c的取值為整數，值域為[-1，N]，N為一個大于工作流模型執行總時間的整數，c的變化表示系統時鐘的運行。實際系統中在不考慮時間約束和活動執行延遲的情況下可令，其中n為工作流活動的總數量，dk是活動k的執行時間。

(3)局部時鐘向量lc[k]，k=0，1，…，n+1。lc[k]的值域與變量c的值域相同，lc[k]的變化表示和活動k相關的局部時鐘運行。

下面用該邏輯系統來為三類時間有效性約束分別建模。

(1)最長時間距離約束的CTL公式描述：

上式表示對于任意路徑，活動k和活動j之間的時間距離都不大于指定時間，其中活動j是活動k的后繼，dk是活動k的執行時間，lc[j]和lc[k]分別是活動j和k局部時鐘。

(2)最短時間距離約束的CTL公式描述：

上式表示對于任意路徑，活動k和活動j之間的時間距離不小于指定時間，其中活動j是活動k的后繼，dk是活動k的執行時間，lc[j]和lc[k]分別是活動j和k局部時鐘。

(3)固定時間約束的CTL公式描述：

上式表示對于任意路徑，活動k都在指定時間開始執行，其中c為全局時鐘。如果在指定時間有多個活動，如j、k、i并行執行，可用如下公式表示：

上述時序邏輯公式只是在時間層面上對有效性約束進行描述，沒有涉及到活動的邏輯結構。在本文中，有效性約束模型可以在一個一階邏輯系統描述的Kripke結構上進行語義解釋。

國網電力調控自動化機房中的布線工作是較為復雜的工作，并且有很多的線路都是在地下或者是建筑物頂端位置，所以，布線的工作難度也是相對較大的。在實際施工過程中，還會有很多的突發事情，比如線路長度的差異，機房中線路布置出來的美觀性等諸多方面的問題，都會影響到布線的實際施工。目前，我國有很多供電企業在機房布線方面都是存在很大問題的。因此，在實際國網電力自動化機房布線工作當中，必須要在前期的設計階段，設計出科學合理具有實用性的布線線路，還需要保證線路的使用效率，以及后期的線路維護、管理等問題，只有這樣才能在一定程度上提高國網電力自動化機房的安全性和效率性，從而去實現機房所帶來的經濟價值。

值得說明的是，在工作流系統中CTL能描述的有效性約束不僅僅只是上面三種，很多復雜的約束都可以用CTL來描述。

4.有效性約束的驗證

上述用CTL描述的有效性約束可用模型檢查的方法來進行驗證。模型檢查的研究始于八十年代初，經過二十多年的發展，現已廣泛應用于計算機硬件、通信協議、控制系統、安全認證協議等方面的分析與驗證，而且已發展出了很多優秀的模型檢查工具，如SMV、SPIN、CWB等[4]。模型檢查的主要思想是檢測用狀態遷移系統描述的有窮狀態系統的行為是否滿足用時序邏輯描述的系統的性質。

我們采用SMV模型檢查工具，SMV基本原理如圖1所示：

利用SMV進行模型檢查的基本步驟為[5]：

(1)用SMV自帶的系統描述語言，給出系統的形式化模型，包括系統狀態和狀態間的遷移關系；

(2)用CTL給出待驗證的屬性描述；

(3)將系統的SMV描述和待驗證屬性的CTL描述輸入檢測系統；

(4)若結果為TRUE，則系統滿足該性質，否則不滿足，系統給出反例。

如果用SMV來驗證工作流系統的有效性約束，需要用SMV自帶的描述語言來對工作流系統建模，SMV模型檢查工具是基于Kripke結構的，而實際工作流系統大多是用工作流過程定義語言(Workflow Process Definition Language，WPDL)來描述的[6]，所以我們需要將工作流過程模型轉換為Kripke遷移系統模型。具體的轉換方法請參考文獻[7]。

5.實例研究

本文研究的工作流系統是一個采購系統，其業務流程如圖2所示。在這個采購系統中，采購單位先制作訂單，然后提交部門內部負責人審核，若審核通過后，可以選擇供應商，也就是向供應商下單。待商家確認訂單后，即可簽署合同。在業務流程圖中，每個節點由三部分組成：一部分為活動標識，另一部分為活動的名字，最后一部分為活動執行的時間。

根據上面給出的驗證方法，首先將WPDL描述的工作流模型轉換成SMV語言描述的系統，限于篇幅，這里不再給出該采購系統的WPDL描述。下面我們給出其對應的狀態遷移圖，如圖3所示，遷移弧上有兩部分內容：一個標識遷移動作，另一個標識該動作持續的時間。

要驗證的有效性約束為：訂單通過審核后，在一周內必須要簽署合同，否則訂單失效。其對應的時序邏輯描述如下：

將SMV語言描述的采購系統模型和有效性約束輸入SMV后的系統主界面如圖4所示。在該界面中已經打開了模型文件，點擊主界面Prop菜單中的Verify all來驗證有效性約束，驗證結果如圖5所示。由圖5可知，驗證結果為false，即該模型未滿足此有效性約束。從狀態跟蹤結果來看，工作流系統可能處于這樣一種狀態：當系統時鐘運行到5個時間單位時，訂單審核完畢，此時lc[2]為3個時鐘單位；當系統時鐘運行到13個時鐘單位時，lc[5]為0，即開始執行簽署合同，而此時lc[2]為11個時間單位，lc[2]-3〉7，故有效性約束不滿足。

6.結束語

隨著工作流系統的應用越來越廣泛，工作流系統中事務的時間有效性的問題越來越突出。在工作流系統中，如何保證恰當的人在恰當的時間完成恰當的任務已成為限制工作流系統應用推廣的關鍵問題。本文探討了如何利用時序邏輯來控制工作流系統中信息的有效性。在實際系統中，可以采用時序邏輯來控制時間有效性。此外，本文還利用模型檢測給出了有效性的驗證方法，探討了模型檢測在工作流系統中的應用，實驗證明該方法是有效的。

參考文獻：

[1]李慧芳，范玉順.工作流系統時間管理[J].軟件學報，2002，13(4)：1-8.

[2]Edmund M，Clarke J，Orna G，Doron AP.Model Checking.Cambridge：MIT Press，2001.

[3]Eder J.，Panagos E.，Rabinovich M..Time Constraints in WorkflowSystems[C].In：Proc.11thConferenceonAdvanced Information Systems Engineering，Heidelberg，Germany，1999，1-14.

[4]林惠民，張文輝.模型檢測：理論、方法和應用[J].軟件學報，2002，30(12)：1907-1912.

[5]McMillan KL.The SMV language.2001.http：//www.cs.cmu.edu/～modelcheck/smv.html.

[6]范玉順.工作流管理技術基礎[M].北京：清華大學出版社，2001.

[7]閆志華，李成，鄭艷萍.工作流模型檢測研究[J].計算機應用，2007，27(6)：1448-1451.

[8]王遠，范玉順.工作流時序約束模型分析與驗證方法[J].軟件學報，2007，18(9)：2153-2161.

[9]Eder J.，Panagos E.，Pozewaunig H.，Rabinovich M..Time Management in Workflow Systems.In：Abramowicz W，Orlowska M E，BIS’993rdInternational Conference on Business Information Systems，Heidelberg：Springer Verlag London Berlin，1999：265-280.