Keywords

1 Introduction

Cyber-physical systems (CPS) enable the development of complex real-world applications through the integration of computation, communication, control, and physical activities. Embedded computers and networks monitor and control physical functionalities. These functionalities when executed affect the physical world and computations. The design of such systems, therefore, rise new design challenges such as the composition of the cyber and physical functionalities [1]. Solutions for this challenge have been proposed to represent the software and hardware functionalities of CPS in the form of interoperable services [2].

A CPS service can be either a cyber or physical service. Cyber-computational resources, which reside either in static or dynamic host computers in CPS network, provide cyber services. Physical devices (sensors or actuators) provide physical services that monitor or make changes in the real-world environment. Hence, CPS is more complex than web-based applications [3] that only consider software services. In fact, the services offered by cyber-physical resources and computational resources differ in their non-functional properties. The non-functional properties characterize the abstract behavior of CPS and define restrictions on their real-time execution [4]. Since CPS can be applied in a variety of domains - such as medical, transportation, smart home, etc. - we differentiate between two types of non-functional properties; the domain-independent and domain-dependent properties. The domain-independent properties represent general desirable features of different domains, such as the execution time and the cost of executed functionality. The domain-dependent properties, on the other hand, stem from peculiar features of the specified domain and regard its components functionalities. For example, the dimensions of space are important characteristics for many transport systems.

Time-related properties are domain-independent constraints on the CPS behavior over time. They are crucial for the correct functioning of the CPS. In addition, time-related properties can be affected by some physical properties. For example, the velocity can affect the arrival time of a flying drone. The physical properties are the constraints on the environment, physical entities, devices or their behavior in CPS. In fact, the specification of physical properties is related to the application domain of the system. To resume, modeling cyber-physical processes requires capturing important particular CPS aspects such as cyber elements, physical elements and their non-functional properties.

The characteristics of the CPS processes and their associated non-functional properties are arguably more difficult to capture in business process modeling [5, 6]. To overcome such limitation, in our previous work, we proposed BPMN4CPS [7, 8]; a CPS-aware BPMN 2.0 extension with CPS aspects. Our aim is to allow designers to accurately and efficiently model CPS processes. We introduced additional concepts to represent the process logic, different types of activities, CPS resources, real-world elements, time related properties and physical properties. Given a set of inter-organizational CPS processes modeled using BPMN4CPS, it is important to set up a verification technique for checking the consistency of the model against the specified properties, i.e., the constraints of each process comply with the different constraints of the different processes.

The modeling of inter-organizational processes is a complex and error-prone step that introduces inconsistencies or errors to the processes, e.g., “dead-lock”. In fact, many approaches have addressed this problem and have proposed some solutions for the verification of the structural correctness of the processes [9] and the satisfaction of the time-related properties [10,11,12]. However, as described before, CPS activities are constrained by physical restrictions. These physical properties, which affect greatly the cyber-physical behavior, have not been treated yet, when verifying such processes. In this context, when studying the possible impact of the specified structural, time-related and physical properties on the inter-organizational CPS processes, we found that implicit conflicts may arise that makes the model inconsistent.

To address these issues, we define a novel verification approach based on a constraint satisfaction model to enable the verification of inter-organizational CPS processes. In order to achieve that, we propose a set of transformation rules for the mapping of BPMN4CPS into a constraint satisfaction model.

In this paper, we begin in Sect. 2 by presenting a review of related literature. We introduce our motivating example in Sect. 3. Then, Sect. 4 presents BPMN4CPS. Next, in Sect. 5, we propose our verification approach. In Sect. 6, we describe our BPMN4CPS tool, and we illustrate its use to model and verify the CPS processes. Finally, Sect. 7 concludes the paper.

2 Related Work

Models play an essential role in the design of cyber-physical systems because they allow a designer to analyze, verify, and detect defects of the system early and efficiently. To address this need, researchers have proposed several verification approaches. Unlike the existing verified models, the BPMN4CPS allows specifying a very rich set of structural, time-related, and physical properties.

In the service oriented computing research field, the authors, in [3, 13], describe the CPS functionalities as services to facilitate the composition task. The authors specify the composition of the CPS services as a CPS workflow pattern, which is a sequence of actions that move the system from the initial state to the desired goal. Since physical properties may impact the operation of the services and affect their availability and functionality, the proposal in [14, 15] effectively support the specification of the physical properties. The above approaches consider the structural, physical and some time-related properties. Recently, authors use BPMN to model CPS processes. In [6], the authors extend BPMN to model resources of the real-world entities that perform CPS activities and specify resource-related non-functional properties such as the performance and reliability for each component. In order to model self-adaptive workflows for cyber-physical systems. Seiger et al, in [16, 17], present a process-based framework in which the abstract system behavior is modeled using BPMN. Furthermore, to consider real-world context situations, in [18], the authors introduce SmartPM which is a framework for automated process adaptation in case of unanticipated exceptions. In fact, in the above approaches, the designer uses the BPMN to define the process control flows among a set of tasks. These approaches show the strong need for modeling complex collaborative behavior of distributed CPS and expressing both sets of structural properties and complex flows of data (event-based) within high-level CPS processes. Despite the fact that these models consider structural, physical and some time-related properties, however, they do not take into account a detailed set of richer time-related properties that can affect the composition of cyber and physical functionalities, as well. Most importantly, these approaches do not apply any verification guidelines for the analysis of the correctness of the workflow. In short, the use of BPMN was only for CPS modeling needs, so verifying the correctness of such models have not been investigated.

Some modeling approaches focus on the specification of CPS using mathematical languages to be checked. To this end, formal verification of CPS, such as a model checking technique, is widely used with the aim of verifying different goals. The authors, in [19], propose a probabilistic approach to formally describe and analyze the reliability and cost-related properties of a composed set of services in IoT. Formal techniques have also been applied to verify the deadlock, livelock [2], reachability and safety [20,21,22] of a cyber-physical model. In particular, in service-oriented or business systems, works have shown the importance of the temporal consistency analysis, by applying either static (e.i., at-design-time) [11, 23] or dynamic (at-run-time) [24] verification. These temporal verification approaches check whether a temporal violation occurs or not, based on formal methods. Nevertheless, these approaches are limited to discover only some time-related inconsistencies, and they do not consider other eventual physical-related conflicts that can arise when concurrent behavioral cyber-physical processes interact together (i.e., inter-organizational processes). In general, the model checker examines all possible system scenarios to identify if a given model truly satisfies certain properties. However, they may not be capable to prove physical property and to find their possible values. Hence, this technique is insufficient to handle our problem that consists of verifying and finding the possible combinations of the different attribute values [25]. This problem can be solved through using the constraint satisfaction problems. A constraint satisfaction problem is a mathematical specification to represent and solve a combinatorial problem. This technique has been used for scheduling problems [26], service selection problems [27], etc. and it can address our verification requirements.

3 Motivating Example

When a hurricane, earthquake, or other natural disaster strikes, lives depend on the response, delivery of supplies and assistance on time. The disaster recovery systems is a communication between the search system and the delivery system. The designer specifies such behavior using two inter-organizational cyber-physical processes, as shown in Fig. 1. First, the search system encompasses a set of sensor drones, installed car cameras and outdoor cameras that monitor the environment. The sensor drones are equipped with wireless routers and antennas to set up a WiFi network in the damaged area. Other water-level sensors installed in the scene, collect information about the environment. The cyber part of such system allows the analysis and the communication with the delivery system. Second, the delivery system encompasses a set of delivery drones and self driving vehicles that carry supplies to the damaged location. The cyber part of such system allows displaying incoming requests on a map using Google earth, and compute an optimal mission plan.

Fig. 1.
figure 1

Processes of the disaster recovery systems

Full size image

Before executing such systems, using BPMN4CPS, the designer models their collaborative behavior, with considering some time-related and physical requirements. The aim is to verify the correctness of the behavior and whether or not the execution will satisfy the specified properties. The associated time related properties are as follows:

  • The duration of each activity in the process, such as the duration of carrying items (i.e., movement-of-the-drone) activity is between 100 to 600 s.

  • The detect-water-level activity has a recurrent behavior that must be repeated every 10 s and no more that 5 times. The aim is to check if the level is increasing.

  • The start time of the match-delivery-equipment activity must be between 5 to 20 s from the finish time of the display-on-google-earth activity.

  • The communication is synchronous and takes 1 to 2 s.

  • The deadline of the collaborative behavior is 400 s.

In addition, the designer specifies as physical properties; (1) a constraint on the drones battery consumption that must ensure its return to the depot after delivering the items, and (2) a global physical property that represents a relationship between two physical attributes in different processes. The first property is specified as a must happen at finish time property. The second property indicates that the drone has to be far away from the water covered region. So, the position of the executed water-level sensors must be different from the position of the drone: \(P_{drone}\ne P_{WaterS}\). We note that the position is \(P(x_i,y_i)\) or a whole area, according to the designer specification. Next, we will give a brief overview of the BPMN4CPS.

4 BPMN4CPS: A BPMN Extension for Modeling Time-Aware CPS Processes

In order to enable the modeling of CPS processes, we proposed, in [7], an extended version of BPMN. The proposed extensions introduce new key concepts related to the CPS functional and non-functional properties. We also supply the modeler with the possibility to visually specify these different CPS aspects and non-functional properties [8]. In what follows, we present the CPS concepts supported by BPMN4CPS, and we describe the newly improved and refined concepts.

4.1 Modeling CPS Aspects

For modeling CPS, we introduce additional concepts, with the purpose of specifying the logic of the CPS processes, CPS activity types, resource roles and real-world elements.

Logic of CPS processes: the CPS application runs on different types of entities, which their behavior can be seen as three distinct participants. The created process model is later used to derive the code that will be executed by the CPS. For such reasons, supporting the deployment of the process requires to split the process model into a cyber, physical and control parts. These parts of the process have to be separated and handled differently. Hence, we proposed the three processes logic, that allows the designer to model the CPS behavior as a collaboration of three process participants. We also introduce a new extension that forces the modeler to specify the cyber-physical system as a single process structured in three parts.

CPS activity types: there are three types of tasks in CPS: the cyber, manual and physical task. The cyber and the physical tasks have different sub-types of tasks. The cyber task can be a web-based, cloud-based or embedded task, while the physical task can be either a sensor’s task or actuator’s task.

CPS resources: in our previous work, we proposed the device performer only as an extension, while in CPS both cyber and physical resources are equally important. Therefore, in CPS model, the performer can be Computing Performer for cyber tasks or Device Performer for physical tasks.

Real-world environment and physical entities: this extension has been proposed to support the specification of the real-world environment (RWE), as an empty pool, which is a participant containing the different physical entities that can be affected or monitored by a physical task.

4.2 Modeling Time-Related and Physical Properties

In [8], we proposed an extension of BPMN4CPS to support time-related and physical properties. First, we consider the following time-related properties:

  • Start and finish time of an activity.

  • Duration of an activity as the minimum and maximum time taken to be executed.

  • Recurrent activity or set of activities, that is restricted by a number of execution, and either an interval of time between two starts or an interval of time in which the behavior can be executed.

  • Temporal-dependency between the start/finish and start/finish of two different activities.

  • Communication time between two activities in two different processes.

  • Deadline, which is the time taken to execute one process or a set of collaborative processes.

Second, we consider the following physical properties:

  • Must happen at the start or finish time of an activity.

  • Must happen during the execution of an activity.

  • Must happen in a bound time.

  • Must happen in an infinite time.

  • Global physical properties that allow the specification of constraints on the whole collaborative behavior such as the relationship between two or more physical attributes from different activities and processes.

5 Verification of the Consistency of the CPS Processes

The verification approach we propose relies on a constraint satisfaction model. In order to achieve that, we define a set of mapping rules that transform the BPMN4CPS model into a constraint satisfaction problem (CSP) [28]. We remind you that verification of collaborative CPS processes aims to assert that the different constraints of the involved processes do not give rise to conflicts, i.e., inconsistencies, which can be an obstacle towards their collaboration. The constraint programming is a technique that takes its features from different domains such as the operational research and the artificial Intelligence. This technique helps solving real combinatorial problems. Using the constraint satisfaction problems, we can specify various parameters as variables and express the dependencies between collections of variables as a set of constraints. The goal of this technique is to define the possible values of all the decision variables, while all the specified constraints are satisfied.

Fig. 2.
figure 2

Transformation rules

Full size image

The mapping process starts first by transforming the structural, time-related and physical properties of each cyber-physical process into a set of variables and constraints. Then, we map the properties related to the communication and global behavior of the collaborative CPS processes into a set of constraints. This mapping is based on a set of transformation depicted in Fig. 2. Unfortunately, in this paper, due to space limitations, we did not introduce all the rules such as those that associate a domain for each variable and those that transform other structural dependencies between activities (e.g., the multi-choice structure).

We note that we consider some assumptions that need to be considered when modeling the systems. First, we propose to consider quantitative attributes. Qualitative physical attributes can be also supported since they can be represented as quantitative attributes based on Boolean metrics. Second, studying the recurrent behavior of a set of activities is a complicated step that requires some restrictions. To do that, we assume that first the cycle does not contain any communicating activities such as the send or receive activity. Finally, the activities in the cycle do not belong to any other cycle. This assumption ensures that the model does not contain overlapping cycles.

5.1 Transformation Rules for a Cyber-Physical Process

In our previous work [8], we proposed a set of constraints for a cyber-physical process only. However, this proposal lacks considering the cycle and the difference between multi-choice and parallel structure. Therefore, in this paper, we extend our previous work to address these issues. To do so, we present the transformation rules that must be applied to each process, in order to generate the set of needed variables and constraints. These rules are those from \(R_1\) to \(R_8\) given in the Fig. 2. In particular, the \(R_1\) and \(R_2\) allows the transformation of physical properties to a set of constraints. These constraints are related to the application domain. Therefore, we define the physical properties associated with the case study. These properties can be either specified by the designer or they can be automatically extracted from a domain model.

5.2 Transformation Rules for Collaborative CPS Processes

To verify the consistency of the communicating cyber-physical processes, in [29], we proposed a new set of constraints that allow the verification of the structural, time-related, physical and synchronization properties. However, the proposed mapping of the cycle is a very complex process that needs to transform each execution trace of the cycle to a set of variables and dependencies between these variables. In fact, this operation is very hard to achieve especially with very complex processes. In addition, the proposed constraints on the communication time do not differentiate between synchronous and asynchronous communications. Therefore, in this paper, we propose new transformation rules that are efficient to generate better and accurate results as given in Fig. 2. In particular, the rule \(R_9\) allows the specification of the synchronous communication between processes, guarantees that the communication time is satisfied, and specifies that the process remain blocked until the operation completes. Whereas, the rule \(R_{10}\) transforms the asynchronous communication that is a non-blocking communication. Finally, we solve the transformed mathematical set of combinatorial problems to check for consistency.

6 Experimentation: BPMN4CPS Tool

We implement BPMN4CPS as a plug-in for Eclipse, which is an extension of the BPMN2 Modeler. The implementation starts by extending BPMN to supports CPS aspects. Second, we extend BPMN4CPS to support time-related and physical properties. Hence, the plug-in allows designers to model the CPS processes and their collaborative behavior constrained by time-related and physical properties [30]. Third, to verify the consistency of the model, we add another feature to the BPMN4CPS plug-in that allows the automatic mapping of the processes model to a constraint satisfaction problem written in Java. To do that, we integrate the Choco solver [28] into the BPMN4CPS plug-in. In Fig. 3, we show a screen-shot of BPMN4CPS. Our tool allows the designer to model CPS processes, specify global properties and verify the model, as depicted by label ❶ in Fig. 3. We also extend the palette to include the different CPS concepts and properties, such as the cyber tasks, as shown by label ❷ in Fig. 3.

Fig. 3.
figure 3

BPMN4CPS plugin

Full size image
Fig. 4.
figure 4

Result of the consistency verification

Full size image

Based on the quality characteristics defined in ISO 9126, and the most used criteria and metrics for evaluating methods and tools inspired from [31, 32], we evaluate our approach and the developed BPMN4CPS plug-in. We prove the functionality, usability and effectiveness of our proposed approach. If we go back to the motivating example, the application of the transformation rules allows us to generate the constraint satisfaction model and automatically analyze the specified model. Based on the generated results as given in Fig. 4, we can prove that the model of the disaster recovery systems is consistent, and it ensures the satisfaction of its specified requirements.

7 Conclusion

This paper studied the verification of the consistency of inter-organizational cyber-physical processes with a focus on their time-related and physical properties. We presented BPMN4CPS, which is an extension of BPMN 2.0 to support CPS aspects and relevant properties, namely, the physical and time-related properties. Next, we described a novel verification approach that checks the consistency of the model. To accomplish the verification, we proposed a set of transformation rules that map the modeled CPS processes into a constraint satisfaction model. The resulting model can be solved in order to verify the consistency of the inter-organizational cyber-physical processes. Finally, we described the BPMN4CPS tool, and we evaluated our approach through an example of disaster recovery systems. We are currently working on BPMN4CPS plug-in and adding a number of additional features, such as support for complex physical properties. In the future, we intend to apply a dynamic (at-run-time) verification to analyze the temporal consistency.