一種基于擴展UML狀態圖的并發工作流驗證方法

摘要：當并發執行工作流的多個實例時會導致數據流訪問時語義的不一致。首先擴展了傳統的UML狀態圖，用它進行工作流實例建模、然后把擴展的UML狀態圖建立的工作流模型轉化為Buchi自動機，并用Buchi自動機之間的積表示多個工作流實例的并發模型、接著給出了和證明了根據并發模型中標記的命題公式判定并發沖突的定理。最后，由于隨著實例數目的增加，并發模型中的狀態數也會按每個實例的狀態數倍增加，為了解決這一問題，在檢測并發沖突的算法中采用了on-the-fly技術。

關鍵詞：UML狀態圖；Buchi自動機；并發；工作流；模型檢測

中圖分類號：TP311 文獻標識碼：A 文章編號：1009－3044(2009)01－0153－04