隨著現代商業流程的互動及組織愈來愈複雜，設計商業導向的系統時通常需要數次的模型轉換－由較高層的純商業模型轉換至較低層的應用相依的模型。但在這些模型的轉換之間，一些關鍵的特性必須被維持，為了確保這些特性在每個模型中都成立，我們使用了一套藉由model checking檢查系統的嚴謹的正式驗證程式Spin來驗證這些模型，並且以這種方式找出了模型間的不一致性。我們辨識出每個模型之活動及狀態後，將該模型轉換為Spin的語言－Promela所建構的驗証模型，並將欲驗証的特性區分為系統條件及特殊條件後進行驗証，在驗証過程中得以檢查這些模型是否符合使用者的需求條件及模型間是否一致。

Nowadays, the organization and interaction in business processes are becoming more and more complicated. So it usually needs multiple translations from the initial business model downward to the application dependent model when developing a business-oriented system. There are some key requirements must be held during the translations. In order to make sure the key requirements won't be missed in each model, we adopt model checker Spin, a rigorous formal verification tool via model checking, to verify the model, and find that inconsistency between models can be traced by such a way. After identifying the activities and states in each process, we built a verification model in Promela, the language used in Spin. And then we separate the requirements into two categories: systematic requirements and ad hoc requirements and using these requirements to verify the model. During the procedure of verification, we can find out whether the models can meet users’ expectation and whether the models are consistent to each other.

[AH02] Wil van der Alst and Kees van Hee. Workflow Management: Models, Methods, and Systems. MIT Press, 2002.

[AHLS05] Bonnie Brinton Anderson, James V. Hansen, Paul Benjamin Lowry, and Scott L. Summers. ] Model Checking for Design and Assurance of e-Business Processes. Decision Support Systems, 39: 333-344, 2005.

[BRJ98] Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addison Wesley, 1998

[CGP00] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.

[EJLT+99] Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter Teeuw, and Chris Vissers. A Business Process Design Language. Lecture Notes in Computer Science , 1708: 76-95, 1999.

[FRGM98] Mohsen M. Fathee, Ray Redd, Darcy Gorgas, and Batoul Modarres. The Effects of Complexity on Business Processes Reengineering: Values and Limitations of Modeling and Simulation Technologies. Proceedings of the 1998 Winter Simulation Conference, pages 1339-1345, 1998.

[GH99] Angelo Gargantini and Constance Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. Lecture Notes in Computer Science, 1687: 146-162, 1999.

[Hoz03] Gerald J. Holzmann. The Spin Model Checker. Addison-Wesley, 2003.

[JMMF+99] Wil Janssen1, Radu Mateescu, Sjouke Mauw, Peter Fennema1 ,and Petra van der Stappen. Model Checking for Managers. Lecture Notes in Computer Science, 1680: 92-107, 1999.

[JMMS98] Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld. Verifying Business Process Using SPIN. Proceedings of the 4th International SPIN Workshop. 1998

[KTK02] Jana Koehler, Giuliano Tirenni, and Santhosh Kumaran. From Business Process Model to Consistent Implementation: A Case for Formal Verification Methods. EDOC '02. Proceedings, p.96, 2002.

[LP99] Johan Lilius and Iv´an Porres Paltor. vUML: a Tool for Verifying UML Models. 14th IEEE International Conference on Automated Software Engineering, p.255, 1999.

[Mat02] P. Matousek , Verification of Business Process, 2002.

[PSGM+02] Adriano Pereira, Mark Song, Gustavo Gorgulho, Wagner Meira Jr. and Sergio Campos. A Formal Methodology to Specify E-commerce Systems. Lecture Notes in Computer Science, 2495: 180-191, 2002.

[SKM01] Timm Schafer, Alexander Knapp and Stephan Merz. Model Checking UML State Machines and Collaborations. Electronic Notes in Theoretical Computer Science, 47: 1-13, 2001.

[WAV04] M. Weske, W.M.P. van der Aalst,and H.M.W. Verbeek. Advances in Business Process Management. Data & Knowledge Engineering, 50(1): 1-8, 2004.

[WHBW01] Wenli Wang, Zolt´an Hidv´egi, Andrew D. Bailey, and Andrew B. Whinston. Model Checking – A Rigorous and Efficient Tool for E-Commerce Internal Control and Assurance. 2001.

[XPDL02] The Workflow Management Coalition. Workflow Process Definition Interface-- XML Process Definition Language, 2002.