Business process modeling and implementation of process supporting infrastructures are two challenging tasks that are not fully aligned. On the one hand, languages such as Business Process Modeling Notation (BPMN) exist to capture business processes at the level of domain analysis. On the other hand, programming paradigms and technologies such as Service-Oriented Computing (SOC) and web services have emerged to simplify the development of distributed web systems that underly business processes. BPMN is the most recognized language for specifying process workflows at the early design steps. However, it is rather declarative and may lead to the executable models which are incomplete or semantically erroneous. Therefore, an approach for expressing and analyzing BPMN models in a formal setting is required. In this paper we describe how BPMN diagrams can be represented by means of a semantically precise channel-based coordination language called Reo which admits formal analysis using model checking and bisimulation techniques. Moreover, since additional requirements may come from various regulatory/legislative documents, we discuss the opportunities offered by Reo and its mathematical abstractions for expressing process-related constraints such as Quality of Service (QoS) or time-aware conditions on process states.
Springer Berlin Heidelberg
Communications in Computer and Information Science
Compliance-driven Models, Languages and Architectures for Services
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
Computer Security

Arbab, F., Kokash, N., & Sun, M. (2008). Towards Using Reo for Compliance-aware Business Process Modelling. In Leveraging Applications of Formal Methods, Verification and Validation (pp. 108–123). Springer Berlin Heidelberg. doi:10.1007/978-3-540-88479-8_9