Verifying Environment-Aware BPMN Collaborations

Abstract

Business processes, particularly collaborations, define how diferent participants interact and behave to achieve specific objectives. These participants operate within an environment: they interact with it, can change it, and are influenced by it in turn. This interplay underscores the importance of explicitly representing the environment, enabling business processes to benefit from its awareness. In this context, BPMN is a widely accepted standard for modeling business process collaborations. However, BPMN and its extensions lack native support for incorporating the environment and its aspects, as well as verifying correctness properties involving both the business process collaborations and their environment. To address these limitations, this project aims to develop a formal approach for modeling BPMN collaboration models integrated with environmental aspects and for enabling the verification of their environment-aware properties. Specifically, the approach involves extending BPMN collaboration models through the integration of an explicit environment model, resulting in the definition of environment-aware BPMN collaborations. To provide a deeper understanding of their behavior, the BPMN metamodel is extended, along with a formal account of its semantics. In addition, to assess the correctness of environment-aware BPMN collaborations, the project focuses on conceptualizing and implementing environment-aware properties that reflect the influence of the environment on process execution.

Keywords

• BPMN collaboration
• Environment model
• Modeling
• Verification

1. Introduction

Modern organizations are continuously exploring more eficient ways to model and execute their business processes. One of the most widely adopted standards for process modeling is BPMN [ 1 ]. In particular, the so-called BPMN collaboration diagrams illustrate how diferent participants, such as humans, software systems, and robots, interact and exchange information within a shared environment to achieve a common goal. A crucial aspect of business process modeling is the consideration of the context where participants operate [ 2 ]. Context, as defined in the literature, comprises all variables influencing the design and execution of a process [ 3 ]. In this research, the focus goes on the environmental context, which includes: (i) the space where process participants move and act, and (ii) the attributes characterizing that space. For the sake of presentation, the term environment is used to refer to this combination of space and attributes.

Awareness of the environment is crucial in business process execution [ 4 ]. Indeed, participants are often part of the environment [ 5, 6 ], as they may occupy specific positions, move, react to situations, or even modify the environment. Consequently, activities, decisions, and events can be influenced by environmental conditions and, in turn, afect them. More precisely, the status of the environment can (i) constrain the execution of an activity, e.g., a machinery can only operate when a required resource is in place; (ii) drive decision points, e.g., an autonomous vehicle waits in an area if a charging station is occupied; (iii) trigger events, e.g., an alarm triggers the termination of an activity. Concurrently, a process activity can influence the status of the environment by (iv) involving the movement of a participant in the space, e.g., a truck that reaches the loading area; (v) changing the environment, e.g., a human that closes a door. Despite the importance of linking business processes to the environment, existing

CEUR

ceur-ws.org research provides partial support for modeling the interplay between BPMN and the environment. Previous works dealing with the concept of environment within BPMN [ 7, 8, 9, 10, 11 ] often propose extensions to the BPMN graphical notation, but none of them provides an environment model and a formal approach to explicitly represent the environment and how BPMN elements relate to it. In this regard, integrating BPMN collaborations with an explicit environment model enables reasoning on environmental aspects not present in business data (such as reachability of places), while also supporting graphical visualization. For this reason, the first research question addressed by this project is:

RQ1: How can BPMN be bridged with the environmental context and how can the interaction between process participants and the environment be modeled?

Besides modeling, it is also crucial to consider how environmental conditions may afect process execution. In this regard, a formal representation of the interplay between BPMN collaboration and the environment enables the verification of behavioural properties related to the environment. For instance, traditional correctness properties like soundness [ 12 ] guarantee the successful termination of the process for all possible executions. However, they overlook possible environmental aspects that may influence the process behaviour. More precisely, a process might be sound from a control-flow perspective but still encounter issues if, for instance, a participant is unable to reach the required location in the environment to perform a task, or if they are expected to be in two diferent places at the same time. To address this gap, it is necessary to define new correctness properties aware of the environment. Although the literature on verifying BPMN collaborations is a widely investigated domain [ 13, 14, 15 ], there are no comprehensive studies on how correctness is impacted by integrating the environment within BPMN collaborations. To achieve this, the following research question is addressed:

RQ2: What environment-aware properties are relevant to ensure the correct execution of BPMN collaborations integrated with the environment, and how can they be verified?

Motivated by these findings, this Ph.D. project aims to define a formal approach for modeling BPMN collaboration models integrated with environmental aspects and for enabling the verification of their environment-aware properties.

The rest of this paper is organized as follows. Sec. 2 discusses the methodology and proposed solution of the project. Sec. 3 presents the literature analysis. Sec 4 presents the actual status of the project. Finally, Sec. 5 concludes the paper with a road map and future works.

2. Methodology

To address RQ1, the research question was structured in two main phases: (i) a comprehensive literature review and (ii) the conceptualization and formalization of BPMN collaboration and the environment.

First, a literature review was conducted to identify existing works that explore the interplay between the environment and BPMN. This review revealed that most related works [ 7, 8, 9, 10, 11 ] extend the BPMN notation with environmental constraints without providing an environment model that explicitly captures the environmental context and its relation to BPMN elements. To bridge this gap, the literature on spatial modeling techniques was investigated [ 16, 17, 18 ] to find a suitable way to represent an environment model which reflects the same level of abstraction as BPMN. In this field, spatial models can be divided into three main categories: geometric models (such as cell-based and boundary-based representations), symbolic models (like topological structures and graphs), and hybrid models, which are a combination of geometrical and symbolic ones. Among these, semantically-enriched place graphs were identified as the foundational model for representing the environment. Semantically-enriched place graphs are hybrid models that ofer an abstraction of the spatial topology, where places denote predefined areas e.g., rooms or buildings, and edges represent connections between these places. Having identified a suitable environment model, the next phase focused on its conceptual integration with BPMN collaborations. To this end, a study of the BPMN meta-model was conducted, in order to extend it with the proposed environment model by leveraging BPMN’s extensibility mechanism [ 19 ]. This extension is useful for understanding which new elements to introduce into the newly proposed model and can serve as a starting point for defining a formal account of it, guiding its implementation, and facilitating the definition of environment-aware properties.

To address RQ2, the research question was structured in two main phases: (i) conceptualizing and formalizing environment-aware properties that influence the correctness of BPMN collaborations integrated with the environment and (ii) exploring suitable verification techniques to formally check the identified environment-aware properties.

Traditional verification approaches for BPMN focus on control-flow correctness, typically through properties such as soundness and safeness [ 20 ]. However, these properties do not consider environmental conditions, such as participant positioning e.g., a task requiring a participant to be in a specific location, environmental changes triggered by process actions e.g., opening an airport gate to enable passenger access, or the unreachability of places due to spatial conflicts e.g., parallel tasks requiring mutually exclusive locations. These limitations highlight the need to identify and conceptualize novel properties that are sensitive to the interaction between processes and their environmental context.

In this regard, to identify relevant environment-aware properties, we will analyze both academic case studies from the literature and real-world scenarios provided by companies operating in highly environment-driven domains, such as logistics and transportation. These investigations could highlight how environmental aspects, such as participant location, environmental conditions, or the reachability of places, can directly afect the execution of BPMN collaborations. Based on these observations, a set of environment-aware properties will be identified and then formally conceptualized to enable precise reasoning. Second, once these properties are defined, the research will focus on how to verify them. To this end, a literature review of existing verification techniques will be conducted to select the most suitable approach for analyzing the behaviour of BPMN collaboration integrated with the environment. Using the formalization of the model and environment-aware properties, the selected technique will be implemented to support the verification of the environment-aware properties within an environment integrated with BPMN collaborations.

In parallel with both research questions, a tool is being developed to enable the modeling, animation, and verification of BPMN collaborations integrated with environmental context. Once developed, the tool will be validated through a set of illustrative case studies designed by the research team, as well as through applications in real-world industrial scenarios, particularly within companies whose operations are strongly influenced by environmental factors, such as those in the logistics and infrastructure maintenance sectors.

3. Literature Analysis

A literature review was conducted to identify existing works that explore the interplay between the environment and BPMN. In this regard Decker et al. [ 9 ], Grefen et al. [ 21 ] and Zhu et al. [ 8 ] propose BPMN extensions that allow modeling location-based tasks whose execution is constrained by the participant’s location; in addition, the latter introduce location-dependent gateways whose conditions are based on environmental information. Similarly, Mazhar et al. [ 11 ] propose a new type of element to represent participant movements and group task elements based on the location where they are performed. Diferently, Dorndorfer et al. [ 22 ] discuss the use of environmental information to trigger conditional boundary events and thus handle exceptional behaviors. Similarly, Chiu et al. [23] introduce a new type of event called location event triggered by environmental conditions captured by IoT sensors. Also, Poss et al. [ 10 ] adopt location-based events and, in addition, define location data, i.e., data objects used to store and retrieve environmental information, and introduce the possibility of allocating resources to tasks based on the location. Tomas Kozel [ 7 ] does a step forward, proposing, in addition to location-based events, the possibility to use specific markers for participants that can move in the environment and track their position. However, all of these works primarily focus on extending the BPMN notation with environmental constraints, without providing an environment model that captures the environmental context. To overcome this limitation, Saddem-Yagoubi et al. [ 6 ] extend and formalize the BPMN notation with environmental aspects. They introduce location-based gateways and location-based tasks and provide a graph-based environment model, but they do not provide any graphical representation, and they only focus on how the environment afects process execution while neglecting the impact of process activities on the environment.

Even though the literature deals a bit with the concept of the environment within BPMN, the approach we want to define advances the current state of the art for diferent aspects. It extends BPMN collaborations by incorporating a graphical representation of the environment, using semantically enriched place-graph. Moreover this approach is fully formalized, enabling analysis and verification of environment-aware process behaviors.

Concerning verification works, the literature is currently under investigation as part of our ongoing research. So far, none of the reviewed approaches investigates how the integration of environmental context impacts the correctness of BPMN collaborations. Existing verification works have mainly focused on the control-flow perspective, without considering environmental factors such as spatial constraints or changes in the state of the environment. For instance, Corradini et al. [ 13 ] provide a formal characterization of BPMN collaborations and some of the most significant correctness properties in the business process domain; namely, well-structuredness, safeness, and soundness. Similarly, Corradini et al. [ 14 ] propose a formal verification framework for BPMN collaborations that supports the verification of safeness and soundness properties, taking into account distinctive characteristics introduced by message exchanges and sub-process elements. However, while these contributions address important aspects of formal verification, they do not consider the influence of the environment. Therefore, additional literature needs to be explored, especially in relation to identifying the most suitable verification techniques for the new environment-aware properties that will be defined.

4. Achieved Results

The research work conducted has already obtained some results. From an environmental and collaboration perspective, we have successfully defined an extended BPMN meta-model that also considers the environment. In particular, the connection between the environment and a BPMN collaboration happens through the fact that each participant of the collaboration holds a position (place) on the environment model (semantically-enriched place graph). Another connection lies in BPMN tasks, as they may depend on the environment and afect it. In this regard, BPMN process tasks have two new attributes, assignment and guard, used to modify and constrain the execution to the environment’s state, respectively. These new attributes are defined through expressions, which may refer to places and their attributes. In the same way, as XOR gateways specify conditions through expressions, the decisions they take may also depend on the environment’s state. Moreover, we also define a new type of task that represents a movement in the environment since it has a new attribute called destination which is used to set the place to reach. Following these modifications, we developed a formal definition of the extended BPMN model, which we call environment-aware BPMN collaboration. It includes a well-defined syntax and semantics to ensure its correct interpretation and execution. We validated this model through multiple case studies that demonstrated its efectiveness in representing complex environmental interactions within business processes. The described results [24, 25] were published in the proceedings of the 22 and 23 International Conference on Business Process Management. Additionally, we developed BEAR (BPMN Environmental AnimatoR) [26], a BPMN animator tool that allows users to model and animate environmental BPMN collaborations, visualize token flows, and monitor environmental attribute changes in real time. This year, we also introduced BEAR 2.0 [27], a new version of the tool with extended functionality and improvements. Currently, the proposed environment-aware BPMN collaboration is being extended to support multi-instance participants. Furthermore, the environment model is being refined to enable a more suitable representation of both indoor and outdoor environments, addressing its scalability.

Regarding the verification of environment-aware BPMN collaborations, the research is currently focused on a literature review and the analysis of use cases to identify environment-aware properties. At this stage, a preliminary hypothesis has been developed concerning the types of environment-aware properties that can be formally verified to assess process correctness. In particular, several classes of R1

BEAR Tool development (modeling and animation)

Environmentaware BPMN collaboration extension R2

Areccaaald-sweemosrtilcuddauynsde aewnDaveriefrionpnirtmoiopenenrottafiel-s avLneiartilefyirscaiatsutirooenn techniques

BEAR tool update for formal verification Formal account of environmentaware properties

Validation in real-world scenarios environment-aware properties are being considered as candidates, including (i) position-based soundness, which ensures that the position of participants allows the process to reach completion e.g., all required participants are in the correct place when needed; (ii) destination safeness, which prevents position conflicts e.g., a participant cannot move synchronously in two diferent destinations; (iii) reachability soundness which verify whether specific areas are eventually reached e.g., a participant has to reach a destination before to do other tasks, if not there is a deadlock. These hypotheses represent an initial step toward understanding which properties are most relevant for verification, but they remain provisional. Further research is needed to consolidate their formal definitions and assess their applicability in practical scenarios.

5. Conclusion and Future Works

This study proposes an extension of BPMN for incorporating environmental context, addressing existing gaps in modeling the interplay between business processes and the environment. Alongside the modeling contribution, we discussed the importance of formal verification in ensuring that the integration of the environment does not compromise process correctness. Traditional properties such as soundness and safeness overlook spatial aspects, which can lead to inconsistencies during execution. For this reason, the research highlights the need to define and verify new environment-aware properties that reflect the influence of the environmental context on business process collaborations.

As illustrated in the Ph.D. project roadmap in Figure 1, structured around the defined research questions, the ongoing work continues with a study of the literature on BPMN and its integration with environmental aspects. Looking ahead, the project will finalize the extension of environment-aware BPMN collaborations, including exception handling support. The remaining research activities will mainly focus on the verification part. Specifically, future work will aim to identify and conceptualize relevant environment-aware properties, formally define them, and leverage the formal semantics of the proposed model to enable their verification through appropriate techniques, such as model checking. The BEAR tool will also be extended to support the verification of environment-aware properties, allowing users to assess the environmental correctness of environment-aware BPMN collaborations. Finally, the proposed approach and the tool will be validated in real-world scenarios through collaborations with companies whose operations are strongly environment-aware, such as the logistics or transportation sectors.

Declaration on Generative AI

The author has not employed any Generative AI tools. [23] H.-H. Chiu, M.-S. Wang, Extending event elements of business process model for internet of things, in: CIT/IUCC/DASC/PICOM, IEEE, 2015, pp. 783–788. [24] F. Corradini, J. Piccioni, B. Re, L. Rossi, F. Tiezzi, On the Interplay Between BPMN Collaborations and the Physical Environment, in: International Conference of Business Process Management, BPM2024, Springer-Verlag, 2024, p. 93–110. [25] F. Corradini, L. Mozzoni, J. Piccioni, B. Re, L. Rossi, F. Tiezzi, Modeling, Formalizing, and Animating Environment-Aware BPMN Collaborations, in: International Conference of Business Process Management, BPM2025 To Appear, 2025. [26] F. Corradini, L. Mozzoni, J. Piccioni, B. Re, L. Rossi, F. Tiezzi, BEAR: BPMN and Environment AnimatoR, in: Proceedings of the Best Dissertation Award, Doctoral Consortium, and Demonstration & Resources Forum at BPM, volume 3758, 2024, pp. 121–125. [27] F. Corradini, L. Mozzoni, J. Piccioni, B. Re, L. Rossi, F. Tiezzi, BEAR 2.0: enhancing the environment model for animating environment-aware BPMN collaborations, in: Proceedings of the Best Dissertation Award, Doctoral Consortium, and Demonstration & Resources Forum at BPM To Appear, 2025.

References

[1] OMG , Business process model and notation , BPMN V2 . 0 ( 2011 ).

[2] N. Aoumeur , J. Fiadeiro , C. Oliveira , Towards an architectural approach to location-aware business process , in: Enabling Technologies: Infrastructure for Collaborative Enterprises , volume 13 , IEEE, 2004 , pp. 147 - 152 .

[3] M. Rosemann , J. Recker , Context-aware process design: Exploring the extrinsic drivers for process lfexibility , in: Proceedings of the Workshops and Doctoral Consortium , Namur University Press, 2006 , pp. 149 - 158 .

[4] L. Poss , S. Schönig , A generic approach towards location-aware business process execution , in: Enterprise, Business-Process and Information Systems Modeling , volume 479 of LNCS , Springer, 2023 , pp. 103 - 118 .

[5] L. Poss , L. Dietz , S. Schönig , Labpmn: Location-aware business process modeling and notation , in: Cooperative Information Systems , volume 14353 of LNCS , Springer, 2024 , pp. 198 - 216 .

[6] R. Saddem-Yagoubi , P. Poizat , S. Houhou , Business processes meet spatial concerns: the sbpmn verification framework , in: Formal Methods, LNPSE , Springer, 2021 , pp. 218 - 234 .

[7] T. Kozel , Bpmn mobilisation , in: International Conference on Mobile Business and Global Mobility Roundtable, World Scientific and Engineering Academy and Society , 2010 , p. 307 - 310 .

[8] X. Zhu , et al., Exploring location-dependency in process modeling , BPMJ ( 2014 ).

[9] M. Decker , et al., Modeling mobile workflows with BPMN, in: ICMB-GMR , IEEE, 2010 , pp. 272 - 279 .

[10] L. Poss , S. Schönig , Location-aware business process modeling and execution , SoSyM ( 2024 ) 1 - 31 .

[11] S. Mazhar , P. Wu , M. Rosemann , Designing complex socio-technical process systems - the airport example , BPMJ 25 ( 2018 ).

[12] W. M. Van der Aalst , A class of petri nets for modeling and analyzing business processes , Computer Science reports 9526 ( 1995 ) 1 - 25 .

[13] F. Corradini , A. Morichetta , C. Muzi , B. Re , F. Tiezzi , Well-structuredness, safeness and soundness: A formal classification of bpmn collaborations , Journal of Logical and Algebraic Methods in Programming 119 ( 2021 ) 100630 .

[14] F. Corradini , A. Morichetta , A. Polini , B. Re , L. Rossi , F. Tiezzi , Correctness checking for bpmn collaborations with sub-processes , Journal of Systems and Software 166 ( 2020 ) 110594 .

[15] H. Groefsema , D. Bucur , A survey of formal business process verification from soundness to variability , International Symposium on Business Modeling and Software Design ( 2013 ) 198 - 203 .

[16] I. Afyouni , C. Ray , C. Christophe , Spatial models for context-aware indoor navigation systems: A survey , Journal of Spatial Information Science 1 ( 2012 ) 85 - 123 .

[17] C. Becker , F. Dürr , On location models for ubiquitous computing , Personal and Ubiquitous Computing 9 ( 2005 ) 20 - 31 .

[18] H. Hu , D.-L. Lee , Semantic location modeling for location navigation in mobile environment, in: Mobile Data Management , IEEE, 2004 , pp. 52 - 61 .

[19] L. J. R. Stroppi , O. Chiotti , P. D. Villarreal , Extending BPMN 2 . 0: Method and Tool Support, in: Business Process Model and Notation , LNBIP, Springer, 2011 , pp. 59 - 73 .

[20] W. M. P. van der Aalst , Workflow verification: Finding control-flow errors using petri-net-based techniques , in: Business Process Management, Models, Techniques, and Empirical Studies , volume 1806 of Lecture Notes in Computer Science , Springer, 2000 , pp. 161 - 183 .

[21] P. Grefen , N. Brouns , H. Ludwig , E. Serral, Co-location specification for IoT-aware collaborative business processes , in: CAiSE , volume 350 of LNCS , Springer, 2019 , pp. 120 - 132 .

[22] J. Dörndorfer , C. Seel , A framework to model and implement mobile context-aware business applications , in: Modellierung 2018 , Gesellschaft für Informatik e .V., 2018 , pp. 23 - 38 .