Procesos de verificacion

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 morimoto-syoichi@aiit.ac.jp

Abstract. Information systems have to respond well to the changing business environment. Thus, they must have architecture which withstands the change.To design such systems, business process modeling is effective, however, the models include often abstractness and arbitrariness. 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 theefforts. We also discuss the prospect of the solutions. The establishment of the verification will be surely helpful toward solving the problems on business process reengineering, business process management, service-oriented architecture, and so on.

1

Introduction

Recently, enterprise information systems are designed based on service-oriented architecture. The solution against the changingbusiness environment is construction 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 andintuitively understandable 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 differentdiagrams 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 provingconsistency 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

withrespect 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
2.1

Formal Verification of Business Process Models
Basic Logics of the Verification

To verifyformally 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 onestate to another. Many specification models to express system behavior derive from automata. In the reference [16], the authors propose a framework to analyze and verify properties of BPMN diagrams converted into the BPEL format that communicate via asynchronous XML messages. The framework first converts the processes to a particular type of automata whose every transition is equipped with a...