基于BPMN的Web服務組合模型的形式化分析.pdf

1、面向服務計算(Service-Oriented Computing，SOC)代表著分布式計算和軟件開發(fā)的最新發(fā)展方向。Web服務組合技術為Web服務的重用以及增值提供了解決方案，是SOC的核心技術之一。BPMN是首個為基于消息交互的松耦合系統(tǒng)集成建模而設計的業(yè)務過程建模語言，提供基于業(yè)務流程的Web服務組合方法，是目前應用在Web服務組合方面極為重要的標準。
　　 基于BPMN的Web服務組合模型作為在分析時的交換依據(jù)，其語義正

2、確性是服務組合能夠得以實現(xiàn)、并以預期的方式工作的基礎。但是，由于BPMN不是形式化的建模語言，結構比較自由且缺乏精確的語義，加上Web服務組合本身是一個復雜的過程，使得BPMN模型比一般的基于圖形表示的流程更易于出現(xiàn)語義錯誤。BPMN模型的正確性需要在服務組合實施前得到保證。形式化方法是對系統(tǒng)進行分析的有效途徑，對BPMN模型進行形式化分析具有重要的理論和實際意義。
　　 本文通過應用形式化分析方法，采用COWS進程代數(shù)對BPM

3、N模型進行形式化描述和分析，并結合性質的SocL，時態(tài)邏輯表示，給出BPMN模型的形式化驗證過程。本文的主要工作有：
　　 (1)分析基于BPMN的Web服務組合方法，通過對面向服務系統(tǒng)的形式化方法的研究，提出一套基于COWS的BPMN元素建模規(guī)則，定義了BPMN模型的精確語義。同時對COWS的語法和操作語義進行擴展，為復雜的Web服務處理過程賦予清晰形式化語義。
　　 (2)對BPMN模型正確性分析，包括：對BPMN結