Verification of Business Process Implementations via Model Checking

摘要

A recent IBM Academy study discussed the "Tooling Gap" problem in Business Process Management. This refers to the chasm between the activities related to the business process modeling and the development of IT artifacts that implement these business processes. Different sets of tools, models, and expertise are employed on both sides of this rift and no formal mappings exist between these models. This gap leads to costly and long development cycles and correctness issues. A major prerequisite for bridging this gap is to ensure that the IT implementation of each of the subprocesses and the communication between them corresponds to the business analyst's view and process model in reality. In our work, we address this gap in three steps: (1) we start from a well-defined business process model satisfying a clearly identified set of properties, (2) we define transformations that will preserve these properties, (3) we obtain an IT model based on communicating automata that allows us to describe the IT implementation at a higher level than native code. Their precise semantics allows these automata models to be executable (e.g. as Controllers of Adaptive Documents in WebSphere Application Server 5.0.) or translated into other executable formalisms. In this paper, we discuss the application of model checking techniques for verifying the transformation of BP models to automata models.