Please check the files attached below
LNCS 5102 - A Survey of Formal Verification for Business Process Modeling A Survey of Formal Verification for Business Process Modeling Shoichi Morimoto School of Industrial Technology, Advanced Institute of Industrial Technology 1-10-40, Higashi-oi, Shinagawa-ku, Tokyo, 140-0011, Japan
[email protected] Abstract. Information systems have to respond well to the changing business environment. Thus, they must have architecture which with- stands the change. To design such systems, business process modeling is effective, however, the models include often abstractness and arbitrari- ness. Therefore, there have been efforts that validate rigorousness of the models. They have defined semantics of the models and applied various logics and formal methods to verification of the rigorousness. This paper focuses on formal verification of the models and surveys the efforts. We also discuss the prospect of the solutions. The establishment of the ver- ification will be surely helpful toward solving the problems on business process reengineering, business process management, service-oriented ar- chitecture, and so on. 1 Introduction Recently, enterprise information systems are designed based on service-oriented architecture. The solution against the changing business environment is con- struction of flexible business processes, which is the core of enterprise information systems development. It is common knowledge that business process modeling (BPM) is effective for the development. Developers can generally model business processes with modeling notation, e.g., BPMN [38], activity diagrams of UML [22]. The diagram, modeled with the notation, is simple and intuitively under- standable at a glance. The notation is also designed so that anyone can easily model. Moreover, the notation is closely relevant to web services; the diagram can be converted into the BPEL XML format [40]. However, work of general modeling includes arbitrariness and lacks strictness. A diagram modeled with the notation may have various interpretations and one or more different diagrams may denote one process. Thus, before utilizing BPM, we must define strict semantics of the models and verify formally them. There have been many efforts that validate strictness of the diagrams; automation tools which can debug grammatical errors of BPMN and convert diagrams into BPEL [23], formal methods for verifying diagrams based on the π calculus [34] or Petri Net [42], techniques proving consistency with model-checking [5], and so on. In this paper we present a survey of existing proposals for formal verification techniques of business process diagrams and compare them among each other M. Bubak et al. (Eds.): ICCS 2008, Part II, LNCS 5102, pp. 514–522, 2008. c© Springer-Verlag Berlin Heidelberg 2008 A Survey of Formal Verification for Business Process Modeling 515 with respect to motivations, methods, and logics. We also discuss some conclusive considerations and our direction for future work. We hope the survey contributes to designers and developers of enterprise information systems for solving issues on their section and satisfying the industrial needs. 2 Formal Verification of Business Process Models 2.1 Basic Logics of the Verification To verify formally business process models, it is firstly required to give the formal semantics to the models. The logical bases and researches using them are roughly classified as follows. Automata. Automata are a public and base model of formal specifications for systems [21]. An automaton consists of a set of states, actions, transitions between states, and an initial state. Labels denote the transition from one state to another. Many specification models to express system behavior derive from automata. In the reference [16], the authors propose a framework to analyze and ver- ify properties of BPMN diagrams converted into the BPEL format that com- municate via asynchronous XML messages. The framework first converts the processes to a particular type of automata whose every transition is equipped with a guard in an XPath format, after which these guarded automata are trans- lated into Promela (Process or Protocol Meta Language) for the SPIN model checker [20]. Consequently, SPIN can be used to verify whether business process models satisfy properties formalized in LTL (Linear Time Temporal Logic). In the reference [8], the authors show a case study to convert automatically business processes written in BPEL-WSCDL to timed automata and to verify subsequently them by the UPPAAL model checker [49]. The authors are cur- rently implementing a tool for the automatic translation that utilizes UPPAAL. In the reference [10], the authors propose a framework to verify automatically business processes that are modelled in Orc [35]. The authors define a formal timed-automata semantics for Orc expressions, which verifies to the Orc’s opera- tional semantics. Accordingly, one can verify formally Orc models with UPPAAL. The paper also shows a simple case study. Thus, to verify business process diagrams the efforts utilizing automata con- vert the diagrams to XML formats (e.g., BPEL, XPDL, WS-CDL, Orc) for the present. After that, they accommodate automata to XML formats and then model-checking tools can verify them (Fig. 1). Besides the above automata mod- els, team automata [12] and I/O automata [30] may be helpful for the verification. Team automata allow one to specify separately the components of a system, to describe their interactions, and to reuse the components. Their advantage is a flexible description for communication services among distributed systems, ex- tending I/O automata. This advantage enables team automata to describe the formal model of secure web service compositions. 516 S. Morimoto Fig. 1. Verification of business process models with automata Petri Net. Petri Net is a framework to model concurrent systems. Petri Net can identify many basic aspects of concurrent systems simply, mathematically and conceptually. Therefore, many theories of concurrent systems derive from Petri Net. Moreover, because Petri Net has easily understandable and graphical notation, it has been widely applied. Petri Net often become a topic in BPM and is related to capturing process control flows [50]. Petri Net can specially detect the dead path of business process models whose preconditions are not satisfied. The paper [9] shows how to cor- respond all BPMN diagrams constructs into labeled Petri Net. This output can subsequently be used to verify BPEL processes by the open source tools BPEL2PNML and WofBPEL [41]. In the reference [36], the authors define the semantics of relation BPEL and OWL-S [51] in terms of first-order logic. Based on this semantics they formalize business processes in Petri Net, complete with an operational semantics. They also develop a tool to describe and automatically verify composition of business processes. In the reference [17], the authors apply a Petri-net-based algebra to modeling business processes, based on control flows. The paper [52] proposes a Petri-net-based design and verification tool for web service composition. The tool can visualize, create, and verify business processes. The authors are now improving the graphical user interface which can be used to aid the business process modeling and to edit Petri Net and BPEL in a lump. The paper [53] introduce a Petri-net-based architectural description language, named WS-Net, in which web-service-oriented systems can be modeled, and presents a simple example. To handle real applications and to detect errors in business processes, the authors are currently developing an automatic translation tool from WSDL to WS-Net. The paper [18] proposes a formal Petri Net semantics for BPEL which as- sures exception handling and compensations. Moreover, the authors present the parser which can automatically convert business process diagrams into Petri Net. Consequently, the semantics enabled many Petri Net verification tools to automatically analyze business processes. In the reference[45], the authors propose a framework which can translate Orc into colored Petri Net. Colored Petri Net has been proposed to model large scale systems more effectively. The framework and tool deal with recursion and data A Survey of Formal Verification for Business Process Modeling 517 handling. Moreover, because the framework and tool can simulate and verify the behavior of process models at the design phase of information systems, users of them can detect and correct errors beforehand. Therefore, they contribute to raise the reliability of business process diagrams. Petri Net is the traditional and well-established technique, thus there have been many verification methods and tools. The essentials of the above efforts are how to translate business process diagrams into Petri Net. After that, we have a rich variety of tools for the verification. However, all the components in business process modeling notation cannot change into Petri Net. For instance, BPMN has various gateways, event triggers, loop activities, control flows, and nested/embedded sub-processes. It is difficult to define the correspondence of these objects to Petri Net. There is room for argument on the translation. Process Algebras. Process algebras are a diverse family of related approaches to formally modeling concurrent systems. Their semantic foundation is based on automata. Many derivative algebras have been defined and many references about them exists. The representative process algebras are Milner’s Calculus of Communicating Systems (CCS [33]), Hoare’s Calculus of Sequential Processes (CSP [19]), the Algebra of Communicating Processes (ACP [1]) by Bergstra and Klop, and the Language of Temporal Ordered Systems (LOTOS [2]) ISO stan- dard. Process algebras are strict and well-established theories that support the automatic verification of properties of systems behavior as well as Petri Net. They also provide a rich theory on bisimulation analysis. The analysis is helpful to verify whether a service can substitute another service in a composition or the redundancy of a service[3]. Among these, the π calculus is a process algebra that influences business process description languages, e.g., XLANG, BPEL. In respect of automatic verification, the π calculus is far superior to Petri Net. From a compositional perspective, the π calculus offers constructs to compose activities in terms of sequential, parallel, and conditional execution, combina- tions of which can lead to compositions of arbitrary complexity. The followings are process-algebraic approaches to specify and verify secure compositions of business processes. In the reference [46], the authors discuss the application of process algebras to describe, compose, and verify business processes, with a particular focus on their interactions. They show an example in which they use CCS to specify and compose business processes. They also use the Concurrency Workbench [6] to validate properties such as correct business process composition. If the π calculus is used instead of CCS, this approach can be useful in practical application. It may solve real issues, e.g., the exchange of messages during business process interactions. In the reference [14], the authors define correspondence between BPEL and LOTOS. The advantage of this proposal is that it includes compensations and exception handling. Thus, it enables the verification of temporal properties with the CADP model checker [13]. 518 S. Morimoto Thus, process algebraic approaches are suitable for verification of the reliabil- ity of information systems, because they can simulate the behavior of business process models and correct their error at the design phase as well as Petri-net- based verification. 2.2 Aims