Verifying Controllability of Time-Aware Business Processes

We consider time-aware business processes, that is, business processes where time constraints on the activities are explicitly taken into account. Business processes are specified by using a graphical notation, similar to BPMN (Business Process Model and Notation) and, in addition, durations of activities are defined by constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that enacts the process, while others are uncontrollable, that is, they are determined by the external world. We develop a method to verify controllability properties of this type of business processes, that is, properties that guarantee the completion of the execution of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Our method is based on a formalization of the semantics of business processes using Constrained Horn Clauses (CHCs), a fragment of first order logic that combines Horn logic and Linear Integer Arithmetics. We present a transformation technique that generates CHCs from the specification of the business process and the controllability property we want to verify. Then we present two algorithms that make use of CHC solving techniques for verifying two kinds of controllability problems, called weak and strong controllability, respectively.