Data Aware Business Process Models: A Framework for the Analysis and Verification of Properties

Well before the computer age, Herbert A. Simon was a pioneer in extending systems thinking to business organizations, identifying and analyzing systemic business processes, and introducing flow diagrams as a representation of processes. Today Business Process Management is a discipline that provides a systematic approach to the development of more efficient and effective organizations, enabling quick adaptation to the changes of the business environment. For this reason modeling languages such as BPMN (Business Process Modeling and Notation, [ 1]) have a wide adoption in modern organizations. Such modeling languages are used for the design and reengineering of business processes and have the advantage of having a representation that is not only easy to understand by all the stakeholders but also machine processable, with tasks assigned to software or human agents based on the workflow and rules defined using BPMN. It is desirable to have tools that give to the designer of the process the possibility of discovering potential problems in processes, ranging from the correctness of the model to the verification of properties of the model, such as conformance to business rules. This paper presents a logic framework that enables the possibility of studying the properties of data-aware business processes, and gives directions for open research challenges.