摘要
建模与验证是业务过程生命周期管理中的重要环节。数据是业务过程的重要组成部分。现有业务过程建模语言都支持基于控制流维度进行数据建模。但是,在工作流中对数据进行形式化建模还存在很大挑战,进而影响在构造时对带有数据信息的工作流的形式化验证。本文通过扩展工作流网对工作流相关数据和应用数据进行了建模,在此基础上提出了数据感知的工作流合理性和一致性验证方法。本文主要工作包括：
·给出了数据感知工作流网DWF-nets (Data-aware Workflow nets)的形式化定义,主要包括三部分：控制流、相关数据感知和应用数据感知。控制流采用工作流网描述；相关数据感知采用任务上分配变迁条件和任务上分配数据读写操作来描述,并重点从语法和语义两方面定义了具体的变迁条件；应用数据感知则在任务上不但标注数据操作同时也标注数据的状态对集合。区分了不同类型的数据与控制流之间的交互特征。
·给出了一种数据感知工作流的合理性分析方法。在]DWF-nets理论基础之上,给出了在变迁条件影响下的行为语义。提出了一种符号可达分析方法验证]DWF-nets合理性属性。对可达分析面临的状态空间爆炸问题提出不同解决方案。
·给出了一种数据感知工作流的一致性分析方法。在]DWF-nets基础之上提出一种集成工作流模型、业务对象生命周期的形式化建模方法。从语法和行为两方面形式化定义了工作流与业务对象生命周期的一致性要求。提出了“转换-合理性验证-行为一致性推导”的行为一致性的验证方法,并从理论上证明了该方法的正确性。上述方法已工具实现(作为分析插件集成到开源的过程验证框架ProM中),应用开发的工具对上述方法已进行全面评估。
Workflow modeling formally and verification is a significant link in workflow lifecycle. Data is an important component in business process. Current modeling languagesof business process support to model data based on control flow perspective. However,there are still great challenges on formally modeling data perspective in workflow, furtherthe formal verification of workflow with data is influenced in building time. The thesisextends workflow nets with workflow relevant data and application data on workflowmodeling. Based on modeling workflow taking into account data perspective, the thesisgives solutions for the two open problems of analyzing process models with soundnessproperty and consistency property. The key contributions of the thesis are as follows:
The issue of data-aware workflow modeling was studied in detail. We have definedworkflow net with the aware of relevant data and application data. For the aware ofrelevant data aspect, conditions as well as data writing operations are assigned ontransitions, in addition, condition is formally defined from both a syntactic and asemantic point of view. For the aware of application data aspect, object operationsand object-state-pairs are taken into on tasks in the process model. Also, the objectbehaviour model was given.
The issue of soundness of workflow taking into account data perspective was stud-ied in detail. We have given the behavior semantics of DWF-nets with the influenceof transition condition in detail. Then we have presented an approach to verify theworkflow correctness based on symbolic reachability analysis and have proposedsome methods to solve the state space problems.
The issue of consistency between workflows and object lifecycles in informationsystems was studied in detail. Syntactical requirements for such consistency wereformalised as well as semantical requirements, i.e. requirements that ensure desir-able runtime behaviour. It was formally demonstrated that the problem of determin-ing behavioural consistency can be solved through a transformation to WF-nets andusing an established and already implemented approach to determining soundnessof these nets.
The approaches mentioned above were implemented as plug-ins of the frameworkfor process analysis named ProM. For DWF-net soundness analysis, this plug-in was usedto test soundness of a number of real-life models. The application of the plug-in to thesemodels shows that our approach was able to correctly assess the correctness of processdefinition with a concrete data refinement. For DWF-net consistency analysis, both thesyntactical and semantical requirements served as the basis for an analysis plug-in thatwas developed for the ProM framework. This plug-in was used to test properties of anumber of real-life models. The application of the plug-in to these models showed thepresence of a number of syntactical and semantical errors. An empirical evaluation ofthe tool was also performed with industrial partners using the well-known questionnaire-based method. The evaluation and feedback from practitioners further evidenced thepractical significance of this research issue in the PLM field and demonstrated that theproposed solution with its automated tool support possessed a high application potential.
引文
[1] Dumas M, van der Aalst W M, ter Hofstede A M. Process-aware information systems. Hobo-ken, New Jersey, USA: Wiley Online Library,2005.
[2] Ellis C A, Keddara K. A Workflow Change Is a Workflow. In: Aalst W M P, Desel J, OberweisA,(eds.). Proceedings of Business Process Management, Models, Techniques, and EmpiricalStudies, volume1806of Lecture Notes in Computer Science. Springer,2000.201–217.
[3] van der Aalst W M. The Application of Petri Nets to Workflow Management. Journal ofCircuits, Systems, and Computers,1998,8(1):21–66.
[4] van der Aalst W M. Verification of Workflow Nets. In: Aze′ma P, Balbo G,(eds.). Proceedingsof Application and Theory of Petri Nets1997,18th International Conference, ICATPN’97,Toulouse, France, June23-27,1997, Proceedings, volume1248of Lecture Notes in ComputerScience. Springer,1997.407–426.
[5] Wynn M T, van der Aalst W M, Hofstede A, et al. Verifying Workflows with CancellationRegions and OR-Joins: An Approach Based on Reset Nets and Reachability Analysis. In:Dustdar S, Fiadeiro J L, Sheth A P,(eds.). Proceedings of Business Process Management,4th International Conference, BPM2006, Vienna, Austria, September5-7,2006, Proceedings,volume4102of Lecture Notes in Computer Science. Springer,2006.389–394.
[6] Hee K M, Sidorova N, Voorhoeve M. Soundness and Separability of Workflow Nets in theStepwise Refinement Approach. Proceedings of Applications and Theory of Petri Nets2003,24th International Conference, ICATPN2003, Eindhoven, The Netherlands, June23-27,2003,Proceedings, volume2679of Lecture Notes in Computer Science. Springer,2003.337–356.
[7] Martens A. On compatibility of web services. Petri Net Newsletter,2003,65:12–20.
[8] Martens A. Analyzing Web Service Based Business Processes. In: Cerioli M,(eds.). Pro-ceedings of Fundamental Approaches to Software Engineering,8th International Conference,FASE2005, Held as Part of the Joint European Conferences on Theory and Practice of Soft-ware, ETAPS2005, Edinburgh, UK, April4-8,2005, Proceedings, volume3442of LectureNotes in Computer Science. Springer,2005.19–33.
[9] Dehnert J, van der Aalst W M. Bridging The Gap Between Business Models And WorkflowSpecifications. Int. J. Cooperative Inf. Syst.,2004,13(3):289–332.
[10] Puhlmann F, Weske M. Interaction Soundness for Service Orchestrations. In: Dan A, Lamers-dorf W,(eds.). Proceedings of Service-Oriented Computing-ICSOC2006,4th InternationalConference, Chicago, IL, USA, December4-7,2006, Proceedings, volume4294of LectureNotes in Computer Science. Springer,2006.302–313.
[11] Kappel G, Schrefl M. Object/Behavior Diagrams. Proceedings of Proceedings of the SeventhInternational Conference on Data Engineering, April8-12,1991, Kobe, Japan. IEEE ComputerSociety,1991.530–539.
[12] Engels G, Ku¨ster J M, Heckel R, et al. A methodology for specifying and analyzing consistencyof object-oriented behavioral models. Proceedings of ESEC/SIGSOFT FSE,2001.186–195.
[13] Verbeek H, Basten T, van der Aalst W M. Diagnosing Workflow Processes using Woflan.Comput. J.,2001,44(4):246–279.
[14] van der Aalst W M, ter Hofstede A H. Verification Of Workflow Task Structures: A Petri-net-baset Approach. Inf. Syst.,2000,25(1):43–69.
[15] ter Hofstede A H M, Orlowska M E, Rajapakse J. Verification Problems in Conceptual Work-flow Specifications. Data Knowl. Eng.,1998,24(3):239–256.
[16] ter Hofstede A H M, Orlowska M E. On the Complexity of Some Verification Problems inProcess Control Specifications. Comput. J.,1999,42(5):349–359.
[17] Alonso G, Mohan C. Advanced Transaction Models and Architectures. Kluwer AcademicPublishers,1997.
[18] Yang S J H, Chen C C. A Petri-Nets Based Approach for Workflow and Process Automation.International Journal on Artificial Intelligence Tools,1999,8(2):193–205.
[19] Baldan P, Corradini A, Ehrig H, et al. Compositional Modeling of Reactive Systems UsingOpen Nets. In: Larsen K G, Nielsen M,(eds.). Proceedings of CONCUR2001-ConcurrencyTheory,12th International Conference, Aalborg, Denmark, August20-25,2001, Proceedings,volume2154of Lecture Notes in Computer Science. Springer,2001.502–518.
[20] van der Aalst W M P, Hirnschall A, Verbeek H M W E. An Alternative Way to AnalyzeWorkflow Graphs. volume2348of Lecture Notes in Computer Science. Springer,2002.535–552.
[21] ter Hofstede A H M, Aalst W M P, Adams M, et al.,(eds.). Modern Business Process Automa-tion-YAWL and its Support Environment. Springer,2010.
[22] Adam N R, Atluri V, Huang W. Modeling and Analysis of Workflows Using Petri Nets. J.Intell. Inf. Syst.,1998,10(2):131–158.
[23] Choi I, Park C, Lee C. Task net: Transactional workflow model based on colored Petri net.European Journal of Operational Research,2002,136(2):383–402.
[24] Harel D. Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program.,1987,8(3):231–274.
[25] Harel D, Lachover H, Naamad A, et al. STATEMATE: A Working Environment for the Devel-opment of Complex Reactive Systems. IEEE Trans. Software Eng.,1990,16(4):403–414.
[26] Wodtke D, Wei enfels J, Weikum G, et al. The MENTOR Workbench for Enterprise-wideWorkflow Management.1997.576–579.
[27] Harel D, Pnueli A, Schmidt J P, et al. On the Formal Semantics of Statecharts (ExtendedAbstract). Proceedings of Proceedings, Symposium on Logic in Computer Science,22-25June1987, Ithaca, New York, USA. IEEE Computer Society,1987.54–64.
[28] Bussler C, Jablonski S. Implementing Agent Coordination for Workflow Management Sys-tems Using Active Database Systems. In: Jennifer Widom S C,(eds.). Proceedings of FourthInternational Workshop on Research Issues in Data Engineering: Active Database Systems,Houston, Texas, February14-15,1994. IEEE-CS1994,1994.53–59.
[29] Kappel G, Lang P, Rausch-Schott S, et al. Workflow Management Based on Objects, Rules,and Roles. IEEE Data Eng. Bull.,1995,18(1):11–18.
[30] Davulcu H, Kifer M, Ramakrishnan C R, et al. Logic Based Modeling and Analysis of Work-flows. Proceedings of Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGARTSymposium on Principles of Database Systems, June1-3,1998, Seattle, Washington. ACMPress,1998.25–33.
[31] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes, I. Inf. Comput.,1992,100(1):1–40.
[32] Milner R, Parrow J, Walker D. A Calculus of Mobile Processes, II. Inf. Comput.,1992,100(1):41–77.
[33] Y D, Z S. Approach for Workflow Modeling using Pi-calculus. Journal of Zhejiang UniversityScience,2003,(4):643–650.
[34] Puhlmann F, Weske M. Using the pi-Calculus for Formalizing Workflow Patterns. In: AalstW M P, Benatallah B, Casati F, et al.,(eds.). Proceedings of Business Process Management,3rd International Conference, BPM2005, Nancy, France, September5-8,2005, Proceedings,volume3649,2005.153–168.
[35] Lapadula A, Pugliese R, Tiezzi F. A WSDL-Based Type System for WS-BPEL. In: CiancariniP, Wiklicky H,(eds.). Proceedings of Coordination Models and Languages,8th InternationalConference, COORDINATION2006, Bologna, Italy, June14-16,2006, Proceedings, volume4038of Lecture Notes in Computer Science. Springer,2006.145–163.
[36] Zhang L, Yu Z. Web Process Dynamic Stepped Extension: Pi-Calculus-Based Model andInference Experiments. In: Meersman R, Tari Z, Hacid M S, et al.,(eds.). Proceedings of On theMove to Meaningful Internet Systems2005: CoopIS, DOA, and ODBASE, OTM ConfederatedInternational Conferences CoopIS, DOA, and ODBASE2005, Agia Napa, Cyprus, October31-November4,2005, Proceedings, Part I, volume3760of Lecture Notes in Computer Science.Springer,2005.202–219.
[37] Valette R. Analysis of Petri Nets by Stepwise Refinements. J. Comput. Syst. Sci.,1979,18(1):35–46.
[38] van der Aalst W M P. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. In: Aalst W M P, Desel J, Oberweis A,(eds.). Proceedings of BusinessProcess Management, Models, Techniques, and Empirical Studies, volume1806of LectureNotes in Computer Science. Springer,2000.161–183.
[39] Aalst W M P, Basten T. Inheritance of workflows: an approach to tackling problems related tochange. Theor. Comput. Sci.,2002,270(1-2):125–203.
[40] Voorhoeve M. Compositional Modeling and Verification of Workflow Processes. In: AalstW M P, Desel J, Oberweis A,(eds.). Proceedings of Business Process Management, Model-s, Techniques, and Empirical Studies, volume1806of Lecture Notes in Computer Science.Springer,2000.184–200.
[41] van der Aalst W M P. Verification of Workflow Nets. In: Aze′ma P, Balbo G,(eds.). Proceedingsof Application and Theory of Petri Nets1997,18th International Conference, ICATPN’97,Toulouse, France, June23-27,1997, Proceedings, volume1248of Lecture Notes in ComputerScience. Springer,1997.407–426.
[42] van der Aalst W M P. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. In: van der Aalst W M P, Desel J, Oberweis A,(eds.). Proceedings ofBusiness Process Management, Models, Techniques, and Empirical Studies, volume1806ofLecture Notes in Computer Science. Springer,2000.161–183.
[43] Verbeek H. Verification of WF-nets[D]. Eindhoven University of Technology, Eindhoven, TheNetherlands,2004.
[44] Lohmann N, Verbeek E, Dijkman R M. Petri Net Transformations for Business Processes-ASurvey. T. Petri Nets and Other Models of Concurrency,2009,2:46–63.
[45] Murata T. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE,1989,77(4):541–580.
[46] Sadiq W, Orlowska M E. Applying Graph Reduction Techniques for Identifying StructuralConflicts in Process Models. In: Jarke M, Oberweis A,(eds.). Proceedings of Advanced Infor-mation Systems Engineering,11th International Conference CAiSE’99, Heidelberg, Germany,June14-18,1999, Proceedings, volume1626of Lecture Notes in Computer Science. Springer,1999.195–209.
[47] Sadiq W, Orlowska M E. Analyzing Process Models Using Graph Reduction Techniques. Inf.Syst.,2000,25(2):117–134.
[48] Desel J, Esparza J. Free choice Petri nets, volume40. Cambridge Univ Pr,1995.
[49] Lin H, Zhao Z, Li H, et al. A novel graph reduction algorithm to identify structural conflict-s. Proceedings of System Sciences,2002. HICSS. Proceedings of the35th Annual HawaiiInternational Conference on. IEEE,2002.10–pp.
[50] EM Clarke O G, Peled D A. Model Checking. The MIT Press,1999.
[51] Eshuis H. Semantics and Verification of UML Activity Diagrams for Workflow Modelling[D].University of Twente, Enschede, The Netherlands,2002.
[52] Hollingsworth D. Workflow management coalition. The Workflow Reference,1995..
[53] Oberweis A, Schaetzle R, Stucky W, et al. INCOME/WF-a Petri net based approach to work-flow management. Wirtschaftsinformatik,1997,97:557–580.
[54] Hidders J, Kwasnikowska N, Sroka J, et al. DFL: A dataflow language based on Petri nets andnested relational calculus. Inf. Syst.,2008,33(3):261–284.
[55] Ellis C A, Nutt G J. Modeling and Enactment of Workflow Systems. volume691of LectureNotes in Computer Science. Springer,1993.1–16.
[56] Sun S X, Zhao J L, Nunamaker J F. Formulating the Data-Flow Perspective for BusinessProcess Management. Information Systems Research,2006,17(4):374–391.
[57] Eshuis R. Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng.Methodol.,2006,15(1):1–38.
[58] Fan S, Dou W C, Chen J. Dual Workflow Nets: Mixed Control/Data-Flow Representationfor Workflow Modeling and Verification. In: Chang K C C, Wang W, Chen L, et al.,(eds.).Proceedings of Advances in Web and Network Technologies, and Information Management,APWeb/WAIM2007International Workshops: DBMAN2007, WebETrends2007, PAIS2007and ASWAN2007, Huang Shan, China, June16-18,2007, Proceedings, volume4537of Lec-ture Notes in Computer Science. Springer,2007.433–444.
[59] Trcˇka N, van der Aalst W M, Sidorova N. Data-Flow Anti-Patterns: Discovering Data-FlowErrors in Workflows. In: Eck P, Gordijn J, Wieringa R,(eds.). Proceedings of Advanced In-formation Systems Engineering,21st International Conference, CAiSE2009, Amsterdam, TheNetherlands, June8-12,2009. Proceedings, volume5565of Lecture Notes in Computer Sci-ence. Springer-Verlag,2009.425–439.
[60] Bichler P, Preuner G, Schrefl M. Workflow Transparency. In: Olive′A, Pastor J A,(ed-s.). Proceedings of Advanced Information Systems Engineering,9th International ConferenceCAiSE’97, Barcelona, Catalonia, Spain, June16-20,1997, Proceedings, volume1250of Lec-ture Notes in Computer Science,1997.423–436.
[61] Ryndina K, Ku¨ster J M, Gall H. Consistency of Business Process Models and Object LifeCycles. In: Ku¨hne T,(eds.). Proceedings of Models in Software Engineering, Workshops andSymposia at MoDELS2006, Genoa, Italy, October1-6,2006, Reports and Revised SelectedPapers, volume4364of Lecture Notes in Computer Science. Springer,2007.80–90.
[62] Sadiq S W, Orlowska M E, Sadiq W, et al. Data Flow and Validation in Workflow Modelling.In: Schewe K D, Williams H E,(eds.). Proceedings of Database Technologies2004, Proceed-ings of the Fifteenth Australasian Database Conference, ADC2004, Dunedin, New Zealand,18-22January2004, volume27of CRPIT. Australian Computer Society,2004.207–214.
[63] Meda H S, Sen A K, Bagchi A. Detecting Data Flow Errors in Workflows: A SystematicGraph Traversal Approach. Proceedings of Proceedings of the17th Workshop on InformationTechnologies and Systems,2007.133–138.
[64] Meda H S, Sen A K, Bagchi A. On Detecting Data Flow Errors in Workflows. J. Data andInformation Quality,2010,2(1).
[65] Awad A, Decker G, Lohmann N. Diagnosing and Repairing Data Anomalies in Process Mod-els. In: Rinderle-Ma S, Sadiq S W, Leymann F,(eds.). Proceedings of Business Process Man-agement Workshops, BPM2009International Workshops, Ulm, Germany, September7,2009.Revised Papers, volume43of Lecture Notes in Business Information Processing. Springer,2010.5–16.
[66] Trcˇka N. Workflow soundness and Data Abstraction: Some negative results and some openissues. Proceedings of APNOC’09: International Workshop on Abstractions for Petri Nets andOther Models of Concurrency, Paris, France, June22,2009,2009.19–25.
[67] Sidorova N, Stahl C, Trcˇka N. Workflow Soundness Revisited: Checking Correctness in thePresence of Data While Staying Conceptual. In: Pernici B,(eds.). Proceedings of AdvancedInformation Systems Engineering,22nd International Conference, CAiSE2010, Hammamet,Tunisia, June7-9,2010. Proceedings, volume6051of Lecture Notes in Computer Science.Springer,2010.530–544.
[68] Sidorova N, Stahl C, Trcˇka N. Soundness verification for conceptual workflow nets with data:Early detection of errors with the most precision possible. Inf. Syst.,2011,36(7):1026–1043.
[69] van der Aalst W M, Hee K. Workflow Management: Models, Methods, and Systems. MITPress,2002.
[70] Aalst W. Information and Process Integration in Enterprises: Rethinking documents. TheKluwer International Series in Engineering and Computer Science. Kluwer Academic Publish-ers, Norwell,1998:161–182.
[71] Yuan C. Principles of Petri Nets (Chinese version). Publishing House of Electronics Industry,Beijing, China,1998.
[72] Verbeek H, van der Aalst W M. Woflan2.0: A Petri-net-based Workflow Diagnosis Tool. In:Nielsen M, Simpson D,(eds.). Proceedings of Application and Theory of Petri Nets2000,21stInternational Conference, ICATPN2000, Aarhus, Denmark, June26-30,2000, Proceeding,volume1825of Lecture Notes in Computer Science. Springer Berlin/Heidelberg.475–484.
[73] Russell N, Hofstede A t, Edmond D, et al. Workflow Data Patterns: Identification, Repre-sentation and Tool Support. In: Delcambre L, Kop C, Mayr H, et al.,(eds.). Proceedings ofProceedings of the24th International Conference on Conceptual Modeling (ER2005), volume3716of Lecture Notes in Computer Science, Klagenfurt, Austria: Springer,2005.353–368.
[74] Conradi R, Westfechtel B. Version Models for Software Configuration Management. ACMComput. Surv.,1998,30(2):232–282.
[75] Alonso G, Reinwald B, Mohan C. Distributed Data Management in Workflow Environments.Proceedings of RIDE,1997.82–90.
[76] Eder J, Lehmann M. Uniform Access to Data in Workflows. In: Bauknecht K, Bichler M, Pro¨llB,(eds.). Proceedings of E-Commerce and Web Technologies,5th International Conference,EC-Web2004, Zaragoza, Spain, August31-September3,2004, Proceedings, volume3182ofLecture Notes in Computer Science. Springer,2004.66–75.
[77] IBM. IBM WebSphere MQWorkflow[EB/OL]. http://www-01.IBM.com/software/integration/wmq/.Accessed Sep2010.
[78] TIBCO. TIBCO stafware process suite white paper [EB/OL].http://www.TIBCO.com/multimedia/idc-report-benifits-of-freestanding-bpm-softwaretcm82147.pdf. Accessed Oct2008.
[79] ATHENA P. BPM flower ondersteunde paltformen[EB/OL].http://us.pallas-athena.com/multimedia/ondersteunde%20platformen%20flower[1] tcm273895.pdf. Accessed Oct2008.
[80] COSA. COSA BPM5.7product description[EB/OL].http://www.cosa-de/project/docs/en/COSA57-Productdescription.pdf. Accessed Oct2008.
[81] Dittrich K R, Lorie R A. Version Support for Engineering Database Systems. IEEE Transac-tions on Software Engineering,1988,14(4):429–437.
[82] Meyer B. Introduction to the Theory of Programming Languages. Prentice-Hall,1990.
[83] van der Aalst W M, Hee K. Workflow Management: Models, Methods, and Systems. MITPress,2002.
[84] van der Aalst W M. Information and Process Integration in Enterprises: Rethinking documents.The Kluwer International Series in Engineering and Computer Science. Kluwer AcademicPublishers, Norwell,1998:161–182.
[85] Cytron R, Ferrante J, Rosen B K, et al. Efciently Computing Static Single Assignment Formand the Control Dependence Graph. ACM Trans. Program. Lang. Syst.,1991,13(4):451–490.
[86] King J C. Symbolic Execution and Program Testing. Commun. ACM,1976,19(7):385–394.
[87] Clarke L A. A System to Generate Test Data and Symbolically Execute Programs. IEEE Trans.Software Eng.,1976,2(3):215–222.
[88] Kumar V. Algorithms for Constraint-Satisfaction Problems: A Survey. AI Magazine,1992,13(1):32–44.
[89] Tsang E P K. Foundations of constraint satisfaction. Computation in cognitive science, Aca-demic Press,1993: I–XVIII,1–421.
[90] Ganzinger H, Hagen G, Nieuwenhuis R, et al. DPLL(T): Fast Decision Procedures. In: Alur R,Peled D,(eds.). Proceedings of Computer Aided Verification,16th International Conference,CAV2004, Boston, MA, USA, July13-17,2004, Proceedings, volume3114of Lecture Notesin Computer Science. Springer,2004.175–188.
[91] van Hee K M, Sidorova N, Voorhoeve M. Generalised Soundness of Workflow Nets Is Decid-able. In: Desel J, Pernici B, Weske M,(eds.). Proceedings of Business Process Management:Second International Conference, BPM2004, Potsdam, Germany, June17-18,2004. Proceed-ings, volume3080of Lecture Notes in Computer Science. Springer,2004.197–215.
[92] Wang Z, Wang J, Wen L, et al. Deriving Canonical Business Object Operation Nets fromProcess Models. In: Cordeiro J, Filipe J,(eds.). Proceedings of ICEIS2009-Proceedings ofthe11th International Conference on Enterprise Information Systems, Volume ISAS, Milan,Italy, May6-10,2009,2009.182–187.
[93] Schmidt K. Using Petri Net Invariants in State Space Construction. In: Garavel H, Hatclif J,(eds.). Proceedings of Tools and Algorithms for the Construction and Analysis of Systems,9thInternational Conference, TACAS2003, Held as Part of the Joint European Conferences onTheory and Practice of Software, ETAPS2003, Warsaw, Poland, April7-11,2003, Proceed-ings, volume2619of Lecture Notes in Computer Science. Springer,2003.473–488.
[94] Karp R M, Miller R E. Parallel Program Schemata. J. Comput. Syst. Sci.,1969,3(2):147–195.
[95] Franco J V. Typical case complexity of Satisfiability Algorithms and the threshold phe-nomenon. Discrete Applied Mathematics,2005,153(1-3):89–123.
[96] Dutertre B, Moura L M. A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball T, JonesR B,(eds.). Proceedings of Computer Aided Verification,18th International Conference, CAV2006, Seattle, WA, USA, August17-20,2006, Proceedings, volume4144of Lecture Notes inComputer Science. Springer,2006.81–94.
[97] Rushby J. Threatened by a Great Opportunity: Disruptive Innovation in Formal Verification.Proceedings of The2006Federated Logic Conference,2004.
[98] B Dutertre and L de Moura. The YICES SMT Solver. http://yices.csl.sri.com/tool-paper.pdf.Accessed Mar2011.
[99] Curran T, Keller G. SAP R/3Business Blueprint: Understanding the Business Process Refer-ence Model. Upper Saddle River: Prentice Hall PTR,1997.
[100] SIEMENS. Teamcenter Manufacturing User’s and Administrator’s Manual.http://www.cadfamily.com/download/CAD/Teamcenter8/TeamcenterManufacturingUserAndAdministratorManuaAccessed Sep2010.
[101] PTC. Configuring a Windchill ProjectLink7.0Workflow and Lifecycle.http://www.ptc.com/carezone/tutorials/files/configuring windchill projectlink workflowlifecycle.pdf. Accessed Sep2010.
[102] Wynn M. Semantics, Verification, and Implementation of Workflows with Cancellation Re-gions and OR-joins[D]. Queensland University of Technology, Brisbane, Australia,2006.
[103] Glabbeek R, Weijland W. Branching time and abstraction in bisimulation semantics. Journalof the ACM,1996,43:555–600.
[104] Werf J. Compositional design and verification of component-based information systems[D].Eindhoven University of Technology, Eindhoven, The Netherlands,2011.
[105] Milner R. Communication and Concurrency. Prentice Hall, London, England,1989.
[106] Verbeek H, Basten T, van der Aalst W M. Diagnosing Workflow Processes using Woflan.Computer Journal,2001,44(4):246–279.
[107] InfoTech. TiPLM-Product Lifecycle Management System of THsoft InfoTech (Chinese ver-sion). http://www.thit.com.cn/chanpinshijie/TiPLM.htm. Accessed Sep2010.
[108] Zha H, van der Aalst W M, Wang J, et al. Verifying workflow processes: a transformation-based approach. Software and System Modeling,2011,10(2):253–264.
[109] Wang Z, ter Hofstede A H, Ouyang C, et al. How to Guarantee Compliance between Workflowsand Product Lifecycles? Technical Report BPM Center BPM-11-10, BPMcenter.org,2011.
[110] van der Aalst W M, Dongen B, Gu¨nther C, et al. ProM: The Process Mining Toolkit. In:Medeiros A, Weber B,(eds.). Proceedings of Proceedings of the Business Process ManagementDemonstration Track (BPMDemos2009), Ulm, Germany, September8,2009, volume489ofCEUR Workshop Proceedings. CEUR-WS.org,2009.
[111] Pinsonneault A, Kraemer K. Survey research methodology in management information sys-tems: an assessment. Journal of Management Information Systems,1993,10(2):75–105.