A rigorous methodology for specification and verification of business processes

摘要

Both specification and verification of business processes are gaining more and more attention in the field. Most of the existing works in the last years are dealing with important, yet very specialized, issues. Among these, we can enumerate compensation constructs to cope with exceptions generated by long running business transactions, fully programmable fault and compensation handling mechanism, web service area, scope-based compensation and shared-labels for synchronization, and so on. The main purpose of this paper is to present a semi-automatized framework to describe and analyse business processes. Business analysts can now use a simple specification language (e.g., BPMN [Obj06]) to describe any type of activity in a company, in a concurrent and modular fashion. The associated programs (e.g., BPDs [Obj06]) have to be executed in an appropriate language (e.g., BPEL4WS [ACD~+03]). Much more, they have to be confirmed to be sound, via some prescribed (a priori) conditions. We suggest how all the issues can be embedded in a unifying computer tool. We link our work with similar approaches and we justify our particular choices (besides BPMN and BPD): the TLA+ language for expressing the imposed behavioural conditions and Petri Nets ([EB87], [EB88]) to describe an intermediate semantics. In fact, we want to manage in an appropriate way the general relationship diagram (Fig. 1). Examples and case studies are provided.