Management of Business Process has come out as a set of technologies aimed at supporting the execution of the business logic by means of modern business best practices [1], which include Workflow Management Systems (WFMS) for workflow execution and monitoring. To attain this, any organization should previously obtain, as result of the Business Process Modelling (BPM), the complete definition of the set of its[5] business processes (BPs), i.e., the set of 'different ways' by which companies conduct its (business) objectives or user goals. Nevertheless, BPM is a “non engineered” activity up to now, since there's still a lack of maturity of current methods and languages in BPTM, especially a lack of soundness and semantics richness. No formal definition of any logics exists up until now to describe the set of activities needed to achieve the user goals [2]. Business Process Modelling Notation (BPMN) [3] has become the “de facto" standard graphical notation for BPM, which describes processes in terms of order dependencies between subprocesses and atomic tasks. In a short time, BPMN has been supported by a variety of BPM tools [3], and thus companies start using it as a standard modeling technique. Existing verification tools cannot be directly applied to BPMN models, in spite of performing verification and validation of BPs is very important to improve their quality. BPMN is a graphical semi-formal notation different from the formal languages required by most existing verification tools, such as SMV, Design/CPN, Uppaal, Kronos, HyTech, FDR2, etc. which operate on models based on Petri nets or Process Algebras. In the literature we can find different directions regarding the verification and validation of a BP. There are formal methods for verifying BPD (Business Process Diagram) based on Π-calculus [4] or Petri Nets [5], tools which can debug syntactical errors in a BPD by transforming these diagrams into BPEL [6][7], and techniques for showing consistency of BPs written in Business Process Execution Language for Web Services (BPEL4WS) [8] based on Model-Checking (MC) [9]. In [8] an extended survey of existing proposals of BPD verification techniques is presented. Nevertheless, none of cited works combine modeling of BPs with analysis/design of BPTMs and verification techniques. Then, and differently from other research work, our approach is aimed at giving a systemic, integrated vision of analysis, design and verification tasks of BPs by promoting the use of MC tools within the BPTM
development cycle. The idea of obtaining a directly executable model from a BP
conceptual has led us to propose a software framework, called Formal Compositional
Verification Approach (FCVA). With our FCVA, the BPTMs correctness can be
model-checked for supporting temporal BP properties analysis and verification. We
propose the construction of a BPTM (i.e., a executable model of the BP) with
TimedAutomata (TA) semantics for modeling BPMN notational elements according to the
specification defined in [
This presentation will shortly describe the theoretical background (i.e., Kripke structures and Clocked Computation Tree Logic –CCTL-) that supports our approach. Then, we discuss the concepts related with modeling, specifying and verifying BPTMs and we give a brief description of BPMN. Afterwards, we present our definition of the TA semantics for some BPMN notational elements and our proposal in detail. Finally, we apply the scheme to a BPM case study related to the CRM business. The last section gives a conclusion and discusses future work. A brief list of references follows. Brief Biography
Manuel I. Capel-Tuñón is Full Professor of Computer Science at the Universidad de Granada– Granada (Spain) where he teaches Concurrent Programming and Realtime Systems and received the title of Ph.D. in CS in 1992. He leads the research group “Concurrent Systems” that counts with more than 100 publications on Formal Methods (Temporal Logics and Process Algebras) applied to the systematic development of embedded real-time systems.
His research interests are currently focused in the isomorphism between the formal
modeling of real-time systems and soft systems, such as social and biological
systems. Dr. Capel-Tuñón has recently proposed a new a formal software design
method, called MEDISTAM, based on systematic transformation of UML-RT
models. Recent results in this field also include an “on-the-fly” Model-Checking
algorithm for Future Interval Logic formulae and, most recently, a compositional
formal verification method of critical systems. His work appears in “Enterprise
Information Systems (EIS)”, “Lecture Notes in Business Information Processing”
(Springer-Verlag), Journal of “Science Of Computer Programming”, “Manufacturing
Engineering”, “International Journal Simulation and Process Modelling” and the
“International Conference on Enterprise Information Systems” (ICEIS). His recent
paper entitled “Automatic Compositional Verification of Business Processes”[