Abstract
Traditional business process specification approaches such as BPMN are procedural, as they require specifying exact and complete process flow. In contrast, a declarative process is specified by a set of constraints that mark the boundary of any solution to the process. In this chapter, the authors propose a bounded model-checking-based approach for the verification of declarative processes using satisfiability solving (SAT). The proposed approach does not require exponential space and is very efficient. It uses the highly expressive event calculus (EC) as the modeling formalism, with a sound and complete EC to SAT encoding process. The verification process can include both the functional and non-functional aspects. The authors have also proposed a filtering criterion to filter the clauses of interest from the large set of unsatisfiable clauses for complex processes. The authors have discussed the implementation details and performance evaluation results to justify the practicality of the proposed approach.
TopIntroduction
A business process is a collection of related activities to accomplish a specific organizational goal. A business process can help an organization by improving agility, productivity, consistency, and can bring other important benefits such as repeatability or understanding. The methods used to manage business processes within an organization are collectively termed as Business Process Management (BPM). BPM involves methods to discover, model, analyze, improve, and automate business processes. First, the process designer needs to model the business process. The objective of business process modeling is to provide high-level specification independent from its implementation that should be easily understandable by the process modeler who creates the process, the developers responsible for implementing the process, and the business managers who monitor and manage the process. Then, the business process needs to be verified to identify any anomalies and conflicts (such as deadlocks) in the process specification before execution. Furthermore, the business process should be monitored while in execution to cater for unforeseen errors or for business process compliance monitoring (Gong, Knuplesch, Feng, & Jiang, 2017). In case of any monitored run-time conflicts, some recovery mechanisms should be provided (Babin, Ameur, & Pantel, 2017).
Web services are in the mainstream of information technology, paving way for inter and across organizational application integration. They can be defined as the software systems designed to support interoperable machine-to-machine interaction over a network. Web services allow heterogeneous systems based on heterogeneous platforms to not only communicate but to expose their operations to the rest of the world using Web services. In addition, the Web services can also be used to implement reusable application-components, such as currency conversion, weather reports etc. Web services are autonomous and they only present an interface that allows other systems to use the operations provided by them and internal implementation of these operations is hidden to the outside world. Web services can also be used to implement a Service Oriented Architecture (SOA), which is defined to be a flexible set of design principles for system development relying on the use of services. The vision associated with the SOA is to separate functions into services and compose them to support the development of distributed applications. As the Web services are autonomous, independent of platforms and programming languages, and are accessible over Internet, they can make functional building blocks of SOA. Business processes and SOA can converge as a business process can be executed using execution languages based on Web Services. Alternatively, from the services perspective, fine-grained services can be orchestrated into more coarse-grained value added processes. In this context, the business process can be considered as a Web services composition process and the terms will be uses interchangeably in this chapter.
BPM involves methods to discover, model (Du & Song, 2016), analyze (Zahoor, Munir, Perrin, & Godart, 2013), improve and automate business processes. In order to model business processes, they can be visualized as a flow chart of related activities and in this context, they are often modeled and specified using Business Process Model and Notation (BPMN). The BPMN specification provides a rich set of elements organized in Flow objects, Connecting objects, Swim lanes and Artifacts categories, and the specification also provides a partial mapping between the elements and the constructs of the execution language. However, BPMN requires specifying the exact and complete flow of the process.
Key Terms in this Chapter
Model Checking: A technique for automatically verifying correctness of finite-state systems. It refers to the algorithms for exhaustively and automatically checking the state space of a transition system to determine if a given model of the system meets a given specification.
Business Process Management (BPM): Set of methods to discover, model, analyze, improve and automate business processes. Process model involves high-level specification and can be visualized as a flow chart. The process needs to be analyzed (verified) to identify inconsistencies such as deadlocks.
Web Services: The software systems designed to support interoperable machine-to-machine interaction over a network. They allow heterogeneous systems to communicate and to expose their operations. They can also be used to implement reusable application-components, such as currency conversion, weather reports, and others.
DECReasoner: A tool to reason about EC models. It encodes the EC based process specification into a satisfiability problem and then invokes the SAT solver which either returns solution(s) or a set of unsatisfiable clauses.
Service-Oriented Architecture (SOA): A flexible set of design principles for system development relying on the use of services. The vision associated with the SOA is to separate functions into services and compose them to support the development of distributed applications. Web services can be functional building blocks of SOA.
Business Process: A collection of related activities to accomplish a specific organizational goal. A business process can help an organization by improving agility, productivity, consistency, and understandability of processes.
Event-Calculus (EC): A logic programming formalism for representing events and their effects. In EC, events are the core concept that triggers changes. A fluent is anything whose value is subject to change over time. EC uses predicates to specify actions and their effects.
Declarative Process Model: A flexible process specification approach which requires only specifying a set of constraints that mark the boundary of any solution to the process. Any solution that respects these constraints is considered as a valid solution.