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

劉磊

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

1.引言

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

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

2.CTL基本概念

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

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

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

3.有效性約束的建模

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.有效性約束的驗證

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

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

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

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

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

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

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

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

5.實例研究

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

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

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

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

6.結束語

隨著工作流系統(tǒng)的應用越來越廣泛，工作流系統(tǒng)中事務的時間有效性的問題越來越突出。在工作流系統(tǒng)中，如何保證恰當?shù)娜嗽谇‘數(shù)臅r間完成恰當?shù)娜蝿找殉蔀橄拗乒ぷ髁飨到y(tǒng)應用推廣的關鍵問題。本文探討了如何利用時序邏輯來控制工作流系統(tǒng)中信息的有效性。在實際系統(tǒng)中，可以采用時序邏輯來控制時間有效性。此外，本文還利用模型檢測給出了有效性的驗證方法，探討了模型檢測在工作流系統(tǒng)中的應用，實驗證明該方法是有效的。

參考文獻：

[1]李慧芳，范玉順.工作流系統(tǒng)時間管理[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.