構件化業務流程重組應用服務器可信屬性建模方法研究

摘 要：針對面向業務流程重組的應用服務器在可信屬性建模方面的不足，基于組成應用服務器的構件屬性和構件組合行為特征，利用進程代數等相關方法進行抽象，從構件之間的運算角度，定義BPRAS構件運算算子，從而建立BPRAS代數模型，并基于該代數模型，進一步對其支撐的業務流程應用軟件可信屬性建模，提出多種可信范式，為可信BPRAS軟件設計提供理論模型支撐。最后介紹了一個應用實例。

關鍵詞：業務流程重組； 應用服務器； 可信屬性； 建模方法

中圖分類號：TN91934； TP311 文獻標識碼：A 文章編號：1004373X（2012）22004605

伴隨著業務流程重組（Business Process Reengineering，BPR）的相關理論與技術在農業、工業和服務業信息化領域廣泛的應用，用戶普遍認可其為業務流程應用軟件研發引入較高靈活性和可維護性等優點，同時也對其提高應用軟件可信性方面提出了更高的要求。可信軟件通常是指在特定環境下其運行行為及其結果符合人們預期，并在受到干擾時仍能提供連續服務的軟件［1］。當前學術界和產業界從不同角度，采用不同方法對可信軟件相關理論展開大量研究，同時作為研究成果，已有大量相應工具出現。但是上述成果大部分關注于通用軟件可信性研究［23］，且還未形成較統一的理解和認識，因而對包括業務流程重組應用服務器（BPR oriented Application Server，BPRAS）在內的特定領域軟件可信性指導性和適用性尚顯不足。

基于以上研究背景，本文重點針對BPRAS這一特定領域軟件，以出具驗證的業務流程重組為該類領域軟件問題域，以該類領域軟件所支撐的業務流程應用軟件為解域，深入研究業務流程應用軟件可信性的形式化方法，對可信業務流程應用軟件進行建模，從而提高業務流程應用軟件可信性，為可信BPRAS軟件設計提供理論模型支撐，并為相關工具軟件研發提供方法與技術支持。

具體而言，本文采用以下方法完成上述研究工作。首先給出BPRAS元構件和分層構件形式化定義，并在此基礎上構建構件運算算子，進而基于構件定義和構件算子給出構件組合的形式化定義；其次，基于構件組合和進程代數理論，建立BPRAS代數模型，并給出基于BPRAS的業務流程應用軟件可信性模型的形式化定義，以及由多種可信范式構成的可信業務流程應用軟件規范化等級理論模型。

毫無疑問，構造可信業務流程應用軟件需要系統性的理論與方法，僅依靠BPRAS自身難以完成可信業務流程重組應用軟件的研發任務，其關鍵原因在于BPRAS處理的是已完成重組的業務流程，而重組后的業務流程是否滿足用戶業務流程重組需求需要流程開發工具出具驗證；另一方面，經過對業務流程可信性分析后確定的規范化等級可反饋至流程開發工具，供用戶參考，并完善業務流程至更高規范化等級。由此形成BPRAS與出具驗證工具［45］協作模型如圖1所示。

圖1 BPRAS與出具驗證工具協作模型1 BPRAS構件模型

1.1 元構件與分層構件

1.1.1 元構件

定義1 元構件可定義為四元組C=，其中：

（1） id是構件的標識；

（2） type={I；II；III；...}是構件類型；

（3） body=（Input，Output，Exec： {ExecI；ExecII；ExecIII；...}）是構件運行體；執行體Exec的各種枚舉類型分別對應各種構件類型。

（4） envi=（Protocal_type，Communi_body）是構件通信環境體。

1.1.2 表示層構件

定義2 表示層構件可定義為四元組CPr=，其中：

（1） Pr_id是構件的標識；

（2） Pr_type={I；II；III}是構件類型；其中I型代表與BPRAS格式保持一致系統需設置報文格式解析模塊；II型代表受BPRAS格式控制系統需設置報文格式解析模塊；III型代表獨立于BPRAS設計報文格式系統；

（3） Pr_body=（Input，Output，Exec：{Split；Explain；Translate}）是構件運行體；執行體Exec的三種枚舉類型分別對應I，II，III三種構件類型；

（4） Pr_envi=（Protocal_type，Communi_body）是構件通信環境體。

1.1.3 功能層構件

定義3 功能層構件可定義為四元組CFu=，其中：

（1） Fu_id是構件的標識；

（2） Fu_type={I；II；III}是構件類型；其中I型代表通訊子層；II型代表平臺子層；III型代表應用子層；

（3） Fu_body=（Input，Output，Exec： {Comm；Plat；Appl}）是構件運行體。執行體Exec的三種枚舉類型分別對應I，II，III三種構件類型。其中：

① Comm=（Input，Output，Exec：{；SynCom}），即執行體Exec的通信子層Comm同構于其母體執行體Exec，且自身執行體Exec的兩種枚舉類型分別為異步通信和同步通信SynCom模塊；

② Plat=（Input，Output，Exec：（MainControl；）），即執行體Exec的平臺子層Plat同構于其母體執行體Exec，且自身執行體Exec的兩類模塊分別為主控模塊MainControl和輔助模塊，即安全控制；格式轉換和基本功能支撐3種模塊；

③ Appl=（Input，Output，Exec：（Business_conf；Mech_conf；Common_conf）），即執行體Exec的平臺子層Plat同構于其母體執行體Exec，但是應用子層特殊之處在于，其輸入來自于BPR配置工具出具驗證后的業務流程；其輸出為業務流程執行日志；且自身執行體Exec的三類配置模塊分別為業務流程配置模塊Business_conf；商戶配置模塊Mech_conf和公共配置模塊Common_conf；實際上，上述三類配置模塊并無執行代碼，僅為配置信息。

（4） Fu_envi=（Protocal_type，Communi_body）是構件通信環境體。

1.1.4 數據層構件

定義4 數據層構件可定義為四元組CDa=，其中：

（1） Da_id是構件的標識；

（2） Da_type={I；II；III}是構件類型；其中I型代表INSERT解析模塊；II型代表與UPDATE解析模塊；III型代表DELETE解析模塊；

（3） Da_body=（Input，Output，Exec：{Insert；Update；Delete}）是構件運行體；執行體Exec的三種枚舉類型分別對應I，II，III三種構件類型。

（4） Da_envi=（Protocal_type，Communi_body）是構件通信環境體。

由上述定義可知BPRAS各層均同構于元構件C。即{CPrCFuCDaC}。

1.2 構件算子

在本節中，設上述分層構件全體組成論域為U。

1.2.1 激發與使用算子

定義5 設A，B是論域Dom（U）中的2個構件，若＼[x∈Input.body（A）∧y∈Output.body（B）＼]∧＼[（yx）∧（Protocal（A）=Protocal（B））＼]∧

＼[Communi_body（A）→Communi_body（B）＼]

即構件A通過同類協議向構件B發送一個消息“激發”構件B中的Exec.body并通過Output.body實現功能需求，則稱A，B進行了一次“激發”運算，記作A| →B。

定義6 設A，B是論域Dom（U）中的兩個構件，若＼[x∈Input.body（A）∧y∈Output.body（B）＼]∧＼[（yx）∧（y∈Exec.body（A））＼]，即構件A通過“使用”構件B的Output.body實現其內部的Exec.body功能需求，則稱A，B進行了一次“使用”運算，記作AB。“激發”與“使用”是最基本的構件組合運算，可統稱為“調用”運算，簡記為A↓B。

1.2.2 反饋與協同算子

定義7 設A，B是論域Dom（U）中的2個構件，若＼[x∈Input.body（A）∧y∈Output.body（B）＼]∧＼[（yx）∧（Protocal（A）=Protocal（B））＼]∧

＼[Communi_body（B）Communi_body（A）＼]

即構件B通過同類協議向構件A“反饋”一個消息，則稱A，B進行了一次“反饋”運算，記作AB。

定義8 設A，B是論域Dom（U）中的2個構件，若x∈Input.body（A），y∈Output.body（B），使得（x∧Input.body（A））→（y∧Output.body（B）），反之，若x∈Output.body（A），y∈Input.body（B），使得（y∧Input.body（B））→（x∧Output.body（A）），即構件A的運行必導致構件B的運行，反之亦成立，則稱A，B是“協同”運算，記作AB。

1.2.3 并行、重復與選擇算子

定義9 設A，B是論域Dom（U）中的2個構件，若（AB）∧（Input.body（A）∧Input.body（B）=），即構件A與構件B在無依賴關系前提下“協同”運算，則稱A，B是“并行”運算，記作A| |B。

定義10 設A，B是論域Dom（U）中的2個構件，若x1∈Input.body（A），y1∈Output.body（A），x2∈Input.body（B），y2∈Output.body（B），若＼[Output.body（A）∧Input.body（B）∧y2→x1＼]＼[Input.body（A）∧Output.body（B）∧y1→x2＼]即構件A與構件B在滿足運行條件下，相互觸發對方，則稱A，B進行了一次“重復”運算，記作A⊙B。特別的，當A=B時，稱A重復執行，簡記為⊙A。

定義11 設A，B是論域Dom（U）中的2個構件，若x∈Output.body（A），y∈Output.body（B），使得＼[Input.body（A）∧x＼]∨＼[Input.body（B）∧y＼]即構件A和構件B在滿足運行條件下，有且僅有一個構件可獲得執行權，則稱A，B是“選擇”運算，記作A⊕B。

1.3 構件組合

定義12 BPRAS構件組合是上述BPRAS構件運算的實現。在BPRAS中構件組合有特定的語義，即它是在平臺子層Plat的執行體Exec的主控模塊MainControl控制下根據出具驗證的BPR流程完成的一次構件運算。可定義為6元組，其中：

（1） Id是組合標識；

（2） Step是組合與構件交互點的序列集合，每個Step=。其中，Sid是標識，Sname是名稱，Scode是構件及運算算子代碼，Stype是類型，Senvi是環境變量的集合；

（3） Beha是組合行為語義描述；

（4） Logs是組合中各個Step的行為日志描述集合；

（5） Envi是組合環境變量的集合；

（6） Cons為保證BPRAS構件組合的自定義約束條件的集合，例如，為確保功能層構件必須參與運算，可規定＼[c′（c′∈Scode.Step∧c′∈CFu）＼]Cons。

2 BPRAS應用軟件可信屬性建模

2.1 可信性模型

2.1.1 BPRAS應用軟件體系結構

BPRAS是支撐BPR應用軟件運行的平臺軟件，其體系結構已在上節給出其構件及構件組合的形式化描述，下面給出其所支撐的BPR應用軟件體系結構代數模型。

定義13 設全體BPR應用軟件組成論域為U，則：

（1） BPR構件是一個BPR應用軟件體系結構；

（2） BPRAS構件組合是一個BPR應用軟件體系結構；

（3） 由BPRAS構件經由有限次組合（構件運算）后是一個BPR應用軟件體系結構。

BPR應用軟件體系結構，記為AS=，簡稱應用軟件。其中C{CPr，CFu，CDa}表示組成應用軟件的構件集合，O{| →，，，，‖，⊙，⊕}表示構件運算的集合。可以證明AS對任意一個運算構成代數系統，具備封閉性，即：c1∈C，c2∈C，o∈O，c1oc2∈C。

定理1 設AS=是應用軟件，則AS對O中任意一個運算都構成代數系統。

證明 由應用軟件組合運算封閉性可得定理1正確性。

將AS=稱為BPR應用軟件的代數模型，也稱為BPR應用軟件的代數表達式。

2.1.2 BPRAS應用軟件可信性模型

定義14 設AS=是應用軟件，若（c′∈C）→（（c∈C，o∈O）∧（c′oc∈C∨coc′∈C））則稱c′為AS的候選核，簡記為Cker（AS），若|Cker（AS）|>1，可選定一個為其主核，簡稱核，簡記為ASker。

2.1.2 1NF范式

定義15 設AS=是一個應用軟件，若滿足（c1∈C）→（（c2∈C，o∈O）∧（c1oc2∈C∨c2oc1∈C）），則稱AS滿足第一范式，簡記為1NF。顯然，為滿足1NF范式，對軟件體系結構設計上的約束等價于物理意義上不允許存在孤立構件，這是可信軟件設計的最低要求。

2.1.3 2NF范式

定義16 設AS=是一個應用軟件，若滿足AS中存在核，則稱AS滿足第二范式，簡記為2NF。例如在1.3節“構件組合”定義中介紹的Cons約束的c′即為一個核。

定理2 設AS=是一個應用軟件，若AS滿足第二范式，則AS必滿足第一范式，即2NF1NF。

證明由2NF和核的定義可知，設c′為AS的核，則對c1∈C，至少c′∈C，有（c1oc′∈C∨c′oc1∈C），即AS滿足第一范式。

證畢。

2.1.4 3NF范式

定義17 設AS=是一個應用軟件，若（c1∈C，c2∈C）＼[（o∈O，c1oc2∈C）→（F（c2）→F（c1））＼]，F（c）（（c∈C）（Input（c）=1∧Output（c）=0））。即對任意兩個構件c1，c2之間所有運算有：若c2不可信，c1必不可信。則稱構件c1可信性依賴于c2。簡記為c2c1。

定義18 設AS=是一個應用軟件，若（C1C）∧（C1∈Cker（AS）），則稱C1中任意一個構件c為AS的候選核因子，簡記為Cker（c）。特別的，當C1=ASker時，稱其為主核因子，或核因子，簡記為cker。

定義19 設AS=是一個應用軟件，若：

（AS∈2NF）∧（c∈C，c′，c″，c，o∈O）（Cker（c））∨

＼[（Cker（c′，c″））∧coc→（c=c′）＼]∨

＼[（Cker（c′，c″））∧coc→（c=c″）＼]

即物理意義上，AS為2NF且其任一個候選核有且僅有最多1個入口運算構件和1個出口運算構件。則稱AS滿足第三范式，簡記為3NF。顯然3NF2NF1NF。

定義20 設AS=是一個應用軟件，若（（c∈C）（（Input（c）=1）（Output（c）=1））），則稱c為AS的一個可信構件，簡記為T（c），若（（c∈C）T（c）），則稱AS是一個可信應用軟件，簡記為T（AS）。根據對c或AS可信性度量結果，記其可信性分別為t（c）和t（AS），且t（c）∈＼[0，1＼]，t（AS）∈＼[0，1＼]。

推論1 若c2c1，則t（c2）≥t（c1）。

定理3 設AS=是一個應用軟件，則AS的可信性與所屬范式關系為：t（AS∈3NF）≥t（AS∈2NF）≥t（AS∈1NF）。

證明分兩步證明：

第1步： t（AS∈2NF）≥t（AS∈1NF）：

（2NF1NF）（（AS∈2NF）→（AS∈1NF））

（1）

（AS∈2NF）c′∈Cker（AS）

（2）

（2）（c∈AS→c′c）（t（c′）≥t（c））

（3）

∑（c∈（AS∈2NF）|t（c））=

＼[∑（c∈Cker（AS））+（cCker（AS）|t（c））＼]

（4）

（3）+（4）t（AS∈2NF）≥t（AS∈1NF）

（5）

第2步： t（AS∈3NF）≥t（AS∈2NF）：

（3NF2NF）（（AS∈3NF）→（AS∈2NF））

（6）

∑（c∈（AS∈3NF）|t（c））=

∑（c∈Cker（AS））+cCker（AS）∧

（c′∈Cker（AS））

（c∧c′=）∨

（c∧c′≠）|t（c）

（7）

（6）+（7）t（AS∈3NF）≥t（AS∈2NF）

（8）

證畢。

3 BPRAS應用研究

3.1 出具驗證業務流程重組模型

為實現上述驗證技術，本文采用的實驗環境基于開放平臺Visual Paradigm（一種免費商業UML建模工具，可從http：//ed.fbk.eu/vlpm下載）。基于該平臺提供的APIs，在此開發了出具驗證的可視化建模工具，圖2是利用該工具完成后某裝備制造業鑄鋼業務流程重組的一個驗證實例。

圖2 某裝備制造業鑄鋼業務流程重組驗證實例圖根據圖2所示，設在出具驗證后業務流程為AS=<{Sp1，Np4，Np5，Np6，Np7，Sp3；

Np4↓（Sp1，Sp3，Np5，Np7），Np6↓Np5}，↓>；其中{Sp1，Np4，Np5，Np6，Np7，Sp3}分別代表原業務流程1，新業務流程4，新業務流程5，新業務流程6，新業務流程7，原業務流程3；↓代表構件調用算子。

3.2 業務流程應用軟件可信性模型

首先，不失一般性，設圖2中所屬構件可信性為均值0.5，即：{c∈AS|t（c）=0.5}，則按照構件依賴關系，有：{Np4（Sp1，Sp3，Np5，Np7）；Np6Np5}。根據規范化定義，顯然，圖2中業務流程無孤立節點，且無候選核，屬于1NF范式。為提高其可信性，改造后的模型如圖3所示。

圖3 改選后模型即將新業務流程4和新業務流程6以并行算子進行構造，有AS′=<{Sp1，Np4‖Np6，Np5，Np7，Sp3；（Np4‖Np6）↓（Sp1，Sp3，Np5，Np7）}，{↓，‖}>，則AS′屬于2NF范式，其中（Np4‖Np6）是其惟一候選核。更進一步提高AS′可信性，進行新的構造，如圖4所示。

圖4 新構造的模型即新增新業務流程8，并控制新業務流程4和新業務流程6以并行方式運行，有AS″=<{Sp1，Np4，Np6，Np5，Np7，Np8，Sp3；（Np8↓（Np4‖Np6））↓（Sp1，Np5，Np7，Sp3）}，{↓，‖}>，則AS″屬于3NF范式，Np8↓（Np4‖Np6）是唯一候選核。

4 結 語

構件化BPR應用服務器可信屬性建模方法是針對出具驗證業務流程，提高其可信性的一種形式化方法。它與出具驗證業務流程方法協同工作，初步實現了業務流程重組需求所代表的問題域到業務流程應用系統所代表的解域之間映射的可信解決方案問題。同時，通過出具驗證業務流程重組工具與可信屬性建模方法聯合應用到一個實例，表明該方法可用于指導業務流程重組的可信應用軟件構造與設計。后續工作包括可信屬性建模理論深入研究與工具研發。

參 考 文 獻

［1］ 陳火旺，王戟，董威.高可信軟件工程技術［J］.電子學報，2003，31（12A）：19331938.

［2］ 趙會群，孫晶.面向服務的可信軟件體系結構代數模型［J］.計算機學報，2010，33（5）：890899.

［3］ 張帆，江敏，吳懷廣，等.一種基于無干擾的軟件動態行為可信性分析方法［J］.計算機科學，2012，39（1）：101103.

［4］ HAN Qiang， QIAN Youshi. VIMPM： a tool to support BPR in Integrated Manufacturing ＼[C＼]// Proceedings of 2011 TMEE. Changchun， China： TMEE， 2011：910913.

［5］ 韓強.一個銀行中間業務軟件支撐平臺的設計與實現［D］.北京：北京大學，2009.

［6］ 李聰玲.液氧/煤油發動機試驗控制系統軟件架構與設計＼[J＼].火箭推進，2009，35（2）：4653.

作者簡介： 韓 強 男，1973年出生，博士，系統分析師，CCF高級會員。主要研究方向為業務流程重組、可信軟件。2012年11月15日第35卷第22期