# A Formal MDE Framework for Inter-DSL Collaboration

Salim Chehida, Akram Idani, Mario Cortes-Cornax, German Vega

## ► To cite this version:

Salim Chehida, Akram Idani, Mario Cortes-Cornax, German Vega. A Formal MDE Framework for Inter-DSL Collaboration. 25th International Conference on Coordination Models and Languages, Oct 2023, Lisbon, Portugal. pp.232-249, 10.1007/978-3-031-35361-1_13. hal-04224395

HAL Id: hal-04224395

https://hal.science/hal-04224395v1

Submitted on 2 Oct 2023

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
<figure><img src="image_3.png" /></figure>

# A Formal MDE Framework for Inter-DSL Collaboration

Salim Chehida, Akram Idani, Mario Cortes-Cornax, and German Vega

Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000, Grenoble, France
`firstname.lastname@imag.fr`

**Abstract.** In order to master the complexity of a system at the design stage, several models have to be defined and combined together. However, when heterogeneous and independent DSLs are used to define these models, there is a need to explicitly compose their semantics. While the composition of static semantics of DSLs is straightforward, the coordination of their execution semantics is still challenging. This issue is generally called inter-DSL collaboration. In this paper, we propose a formal Model Driven Engineering (MDE) framework built on the Meeduse language workbench that we extend with the Business Process Model and Notation (BPMN). Meeduse allows to instrument DSLs with formal semantics using the B method. BPMN provides an easy-to-use notation to define the coordination of execution semantics of these DSLs. A transformation of BPMN models into Communication Sequential Process (CSP) formal language enables the possibility for animation and verification. Our approach is successfully demonstrated by modeling the collaboration of two DSLs from a real case study.

**Keywords:** DSL · BPMN · Model Composition · Models Collaboration · Formal Methods · B Method · CSP · Animation · Verification.

## 1 Introduction

Domain-Specific Languages (DSLs) can be used to model different concerns of a system such as its architecture, the inherent processes, data flows or security policies. These dedicated languages permit domain experts to create models in their speciality. However, models that are built with heterogeneous DSLs must be combined together in order to favour maintenance, verification, code generation, etc. Indeed, updating a model usually leads to modifications of the other related models. Also, triggering an action in one model can induce other actions in the related models. This situation has been observed in real applications, leading to the necessity to bridge the gap between DSLs semantics and preventing inconsistencies all along a model-driven development process [12].

In this paper, we propose a novel approach, supported with a formal framework, that allows engineers to define how DSLs collaborate with each other. We use Meeduse [10], the only existing language workbench (LWB) today that enables both formal reasoning (via theorem proving) and the DSL execution
(via animation and model-checking). Meeduse uses the B method [1] for spec-
ifying the semantics of DSLs and ProB model checker [18] for animation and
verification. It has been successfully applied to several realistic case studies [11].

However, the tool did not present any feature to deal with DSL collaboration.
Hence, the goal of this work is to extend Meeduse with the capability to define,
execute and verify inter-DSL collaboration. Our approach consists of three main
steps:

1. In the first step, a composition metamodel is created in order to relate the semantic domains of independent DSLs, assuming that these semantics are themselves defined by means of metamodels;

2. In the second step, Meeduse is used to transform the various metamodels into formal B specifications taking benefit of the composition mechanism of the B method. The resulting specifications are then used to define the execution semantics of these metamodels via B operations;

3. The third step uses BPMN [20] to define the collaboration between the DSLs. In this model, tasks refer to B operations providing the execution workflow of the collaboration. By transforming the BPMN model into CSP (Communication Sequential Process [22]), we obtain a CSP||B [23] specification that is used for animating and verifying the so-called DSLs' collaboration.

To illustrate our approach, we apply it to a smart grid case study provided
by RTE, the energy transmission company in France. The case study involves
two DSLs: the first one focuses on the management of system configurations
assigning to a set of applications various infrastructures. The second is dedicated
to security risk assessment. The composition and the collaboration of these DSLs
allow to manage configurations while dealing with security concerns.

Following the introduction, we describe a motivation scenario in Section 2.
We present our model-based approach for inter-DSL collaboration in Section 3.
Then, the application of our approach to the RTE case study is discussed in Sec-
tion 4. Section 5 lists related works and finally, Section 6 draws the conclusions
and the perspectives of this paper.

## 2 Case Study and Motivation

In this work, we consider a real case study inspired from [24]. To promote renewable energies, RTE aims to make extensive use of smart grid technologies and develop efficient systems that respond to *meteorological* and *security* factors. The main challenge is to deal with overcurrent in the transmission lines due to the excess energy production in the wind farms, which can create a real danger for people and goods near the transmission lines. For this purpose, a first DSL, named *CM-DSL* (Configuration Management DSL), is used for defining the system configurations to be used for responding to the environment dynamics. A second DSL, named *SRA-DSL* (Security Risk Assessment DSL), is used for security modeling and analysis. In the following sections, more details about the aforementioned DSLs are given.
## 2.1 Configuration Management DSL (CM-DSL)

The Configuration Management DSL (CM-DSL) describes RTE configurations by assigning applications to infrastructures. In this work, we present a simplified part of CM-DSL to illustrate the problem. Figure 1 presents a model, where three applications are defined: (1) *Fast Action* uses a simple flow chart logic and leads to the massive disconnection of wind farms from the grid; (2) *Normal* refers to predictive control algorithm in order to seek the optimal use of all levers (wind farms modulation, batteries and circuit breakers); and finally, (3) *Enhanced Forecasting* uses forecasts of the next day generation and weather (wind and sunlight) for optimisation. The model also considers three infrastructures: (1) in *Centralized RTE*, algorithms can only be run on data-center resources that communicate directly with the gateways connected to sensors or actuators for generators or batteries; (2) in *Collaborative Fog*, the execution is done in sub-station calculators that communicate in a peer-to-peer scheme with the other calculators; and (3) in *Hierarchical Fog-Cloud*, all calculators are available to run the applications and both data-center to substation and substation to substation communications are allowed. Combining applications and architectures a configuration can be proposed. Figure 1 presents four different ones. A configuration is also characterized by its response time (QoS in seconds) calculated using an external simulation tool. The status is decided by the software architect, which can be valid (example of AM1-IM3) or invalid (example of AM3-IM1) depending on its QoS. In the selected *AM1-IM2* configuration (framed in dotted line), the *Fast Action* application is to be deployed on *Collaborative Fog* infrastructure. Valid configurations can be used in the real operation.

<figure><img src="image_4.png" /><figcaption>Fig. 1. A Configuration Management (CM) model showing four different configurations</figcaption></figure>

## 2.2 Security Risk Assessment DSL (SRA-DSL)

The Security Risk Assessment DSL (SRA-DSL) refers to Attack-Defense Tree [15] for security risk assessment. A tree structure is used for specifying threats,
defenses, and the combinations between them. In Figure 2, threat nodes are rep-
resented by rectangles and defense nodes by parallelograms. The combinations
between the nodes are expressed by logical operators (AND, OR, NOT) depicted
by ellipses. The SRA-DSL model of Figure 2 specifies the combination between
the 8 threats (T1, T2, ..., T8) and the 5 defenses (D1, D2, ..., D5) of the RTE
system. Each defense prevents a set of threats. For instance, *closing a specific
breach in the network* (D2) can prevent *tampering on customer network* (T5),
*denial of service* (T6), and *information disclosure* (T7). In a SRA-DSL model,
it is possible to select the possible threats (framed in bold as for instance T8)
on a part of the system or in a specific state of the system among the whole set
of system threats. It is also possible to compute the defenses subset (framed in
blue bold as for instance D4 and D5) that can counter all the selected threats.
The SRA-DSL user can also set the defense *Cost* in seconds, which is the delay
caused by its activation to protect the system (an example cost of D1 is 0.4
seconds).

<figure><img src="image_5.png" /><figcaption>Fig. 2. The SRA model</figcaption></figure>

We note that CM-DSL and SRA-DSL are independent and can be used for
other applications or case studies. For example, paper [4] shows how the SRA-
DSL is used for security risk assessment in Internet of Things (IoT) systems.

## 2.3 Collaboration and Verification Needs

CM-DSL provides the possible configurations that can meet the environmental
dynamics, but it does not consider the configurations’ security. On the other side,
the SRA-DSL is a logic-based DSL that can be used within different security
contexts. In our case study, we use SRA-DSL to identify possible threats of each
configuration and to calculate the required defenses. By doing so, the response
time and the validation state of the configuration can be updated based on the
cost of the defenses. The integration of these two DSLs infers the need to ensure
inter-DSL properties. Below, we provide some examples of properties:

- (P1) The delay caused by configuration defenses should not exceed a percentage of the configuration response time (e.g., 30%)

- (P2) At least one defense must be activated to secure a configuration.

- (P3) The response time of a configuration should not exceed a given threshold (e.g., 2 seconds).

In this work, we propose a new approach to manage and check the collaboration between two ore more DSLs (in this case, illustrated by the CM-DSL and the SRA-DSL). We aim more precisely to:

- Highlight the links between the DSLs concepts (e.g., configuration and defenses).

- Specify the collaboration process between the DSLs actions.

- Animate interactively the collaboration process while ensuring the updates at the DSL models.

- Express and check inter-DSL properties.

In the next section, we describe the Inter-DSL approach that orchestrates
the DSLs’ execution collaboration.

3 Inter-DSL Collaboration : A Model-based Architecture

An overview of our approach is given in Figure 3, divided into two main blocks: X and Y. The model-based approach is supported by the Meeduse platform for rigorous DSLs’ design (block X presented in Section 3.1). Meeduse has been extended for modeling, animation and verification of inter-DSL collaboration (block Y presented in Section 3.2). Figure 3 shows the collaboration between two DSLs, but the approach can be applied for more.

## 3.1 Formal Model Driven DSLs

As shown in Figure 3, we first specify the abstract syntax of each DSL using EMF-based modeling tool (Ecore, Xtext, Sirius, GMF, etc.). The DSL’s concepts are represented by a metamodel. The different metaclasses are characterized by a set of attributes and operations, related by a set of associations (see examples in Figure 4). The domain expert uses the DSL to create models (instances) that conform to the DSL metamodel.

We instrument our DSLs in Meeduse language workbench, which provides
a formal framework to our approach. Meeduse produces a B machine from a
given metamodel and enables the application of B method to define the exe-
cution semantics of the DSLs together with its invariant properties. The static
semantics of the DSL is represented by sets, variables and typing invariants that
<figure><img src="image_6.png" /><figcaption>**Fig. 3.** Generic architecture for modeling and verification of inter-DSL collaboration</figcaption></figure>

define the structural features of the metamodel. The execution semantics of the DSL is represented by operations that define the DSL actions and initialization. Meeduse is also equipped with a tool that allows to animate the execution of a model (instance of the metamodel) into the DSL B machine, by introducing the valuation of the B abstract sets and the initialisation of B variables.

As mentioned earlier, the Meeduse uses ProB for the animation and verification of B specifications. In this step, each DSL can be animated separately by running its actions represented by B operations. At each animation step, the animator provides the set of operations that could be executed, which are the ones that preserve the invariants. In this work, we aim to collaboratively animate a set of DSLs by triggering actions from different DSLs while respecting the collaboration process and system properties.

## 3.2 Formal Model Driven Inter-DSL Collaboration

The inter-DSL collaboration is specified by a so-called "composition metamodel" and a BPMN collaboration diagram, which will then be transformed into formal specifications to be used for animation and verification.

**Composition.** The composition metamodel links the other DSL metamodels. It is represented by a metaclass named Composition related by composition associ-
ations to the root metaclasses of each DSL to be coordinated. In this metamodel, we can also add new metaclasses with new attributes, operations (composition actions) and references to meet inter-DSL collaboration needs. Starting from this metamodel, we generate the composition B machine that includes the B specifications obtained from the different DSLs. In the dynamic part of the composition B machine, we integrate the B operations defining actions involved in the collaboration process. We can also introduce properties like those presented in the Section 2.3 as invariants of the composition B machine.

**Collaboration Model.** We express the collaboration between the DSLs actions using a process modeling language. For process modeling, there are several languages and notations, such as the Business Process Model and Notation (BPMN) and the Unified Modeling Language (UML) Activity Diagram [21]. In this work, we use BPMN 2.0, which is the standard de-facto for process modeling. BPMN, supported by the Object Management Group (OMG), is a language that proposes a graphical notation providing the description of processes elements supported by a metamodel, without specifying a fully defined execution semantics (in natural language). In our approach, we use the notion of BPMN pool, which is the graphical representation of a participant in a collaboration, to group operations of each DSL, including the composition metamodel. We represent an atomic action specifying one metamodel operation by a BPMN task and we use expanded subprocesses to represent a grouping of tasks. BPMN sequence flows are used to represent the sequence of actions in the context of a DSL (inside the Pool), while message flows are used to represent the inter-pool communication. Gateways (exclusive or parallel) model the control flow in each DSL.

**Formal Process Model.** To enable the animation and verification of inter-DSL collaboration, the graphical BPMN models are mapped to a formal specification. Several works propose this transformation to process algebras languages like CSP or Calculus of Communicating Systems (CCS) [19]. In this paper, we manually transform the BPMN diagrams into CSP models. Work in progress intends to automate and validate this transformation by exploiting works like [8]. The constructor's mapping is illustrated with our use case in Section 4.3. From this mapping, we aim to take advantage of the ProB tool (integrated into the Meeduse platform) for the animation and verification. The ProB tool takes as input the CSP process model and the composition B machine coming from the DSLs and composition metamodels respectively. The CSP||B specification, as presented in [3], is used for animating and verifying the inter-DSL collaboration processes.

# 4 Application to Smart Grid System

In our approach, the *Model-driven engineer* specifies the DSLs metamodels and the BPMN models of their collaboration. Then, the metamodels and BPMN diagrams are transformed into B and CSP respectively, while integrating the system
properties. Afterwards, the *operator* can animate the formal specifications while observing the respect of the properties.

In [5], we describe the different steps of our approach and its application to our case study. We also provide the different artifacts of this case study. The modeling part includes the CM-DSL and SRA-DSL metamodels, the metamodel of their composition, the models that define the instances of the metamodels, and the BPMN diagram that describes the collaboration between the DSLs. The formal specification part includes the B machines generated from the DSLs and their composition as well as the CSP model specified from the BPMN diagram.

## 4.1 Modeling DSLs and their Collaboration

**Metamodels.** Figure 4 shows the metamodels that we propose for our case study (one per DSL, and a third one for the composition). Part A of Figure 4 is the EMF metamodel of CM-DSL. The root class (CM) is composed of a set of applications and a set of infrastructures. Every application applies a specific optimisation algorithm that gets the production parameters and information from sensors to trigger actions such as limiting the production on wind farms or charging batteries. Infrastructures are based in RTE power stations and data-centers, connected by a private telecommunication network. A CM model is also composed of configurations, each one consists of the combination of one application and one infrastructure and it is characterized by its response time (QoS) and validation state (oisValid). The CM-DSL defines the following operations: *selectConfig* selects one configuration from the list of CM configurations, *validateConfig* validates the selected configuration, and *setQoS* introduces or modifies the QoS of the selected configuration.

In part B of Figure 4 the SRA-DSL metamodel is shown, which is composed of metaclasses for specifying the possible threats of the system and the defenses that can be deployed to protect the system. Each defense is characterised by a cost (costDef), which is the delay caused by its activation in the RTE platform. A series of metaclasses are introduced for representing the logical operators (NOT, OR, AND) combining threats and defenses. The operations of SRA-DSL are : *initSRA* selects the subset of possible threats, *selectThreat* selects a threat from the set of possible threats, *computeDefenses* calculates the subset of defenses that can block the selected threats.

Finally, part C of Figure 4 shows the composition metamodel. Metaclass COMPOSITION is composed of the root metaclasses of the previously presented DSLs (CM-DSL and SRA-DSL). The composition has its own operations that define its execution semantics. Indeed, we introduce the notion of *Secure Configuration* that associates a set of defenses to a valid configuration (using operation *affectValidDefenses*). Furthermore, operation *approveSecureConfig* allows one to validate a Secure Configuration if it ensures risk assessment and quality of service properties.

**Inter-DSL Collaboration.** In our proposal, we describe the inter-DSL collaboration using a BPMN model (Figure 5) relying on the operations of the above
<figure><img src="image_7.png" /><figcaption>Fig. 4. DSL and composition metamodels</figcaption></figure>

metamodels. We use the notion of Pool to separate the execution semantics of every DSL. The collaboration starts in pool *DSLs_COMPOSITION*, where it triggers via a message (named *ConfigurationRequest*) the selection and validation of a configuration at the CM-DSL level. Note that this corresponds to a functional validation, not considering yet the security aspects. Afterwards, in the composition pool, a new secure configuration is created and associated to the validated configuration. This task is triggered by the reception of message *ValidConfig*. The new secure configuration is then sent to the SRA-DSL pool in order to select possible threats of this configuration and compute the defenses that can prevent them. When receiving the defenses (message *ValidDefenses*), it is possible to approve the secure configuration after checking the global QoS and the other risk assessment properties.
<figure><img src="image_8.png" /><figcaption>Fig. 5. BPMN collaboration model of SRA-DSL and CM-DSL</figcaption></figure>

## 4.2 Formalization of Metamodels

While metamodels describe static semantics of DSLs, the BPMN model and the associated operations represent their execution semantics. We need on the one hand a tool to define and animate these semantics and on the other hand a way to guarantee that the security properties are preserved by the underlying behaviour. To this purpose the Meeduse framework has been extended. The tool applies the B method to formally define execution semantics of DSLs using B operations, which allows us to introduce the security properties using B invariants. From this formal specification the AtelierB prover is applied in order to guarantee the correctness of the model. In this section, we start by presenting an excerpt of the resulting B specifications, and then we discuss the CSP model that is built from our BPMN diagram.

Given a metamodel, Meeduse generates a formal B specification in which classes are defined using sets. Attributes and associations are defined using functional relations. Not all of our specifications are presented but only an exam-
ple, as we rather focus on the composition metamodel. The header part of the
corresponding specification is given below. This B machine includes machines
`CM_DSL` and `SRA_DSL` issued from our DSLs and where operations `select-Config`, `validateConfig`, `setQoS`, `selectThreat`, `computeDefenses` and `initSRA` are
defined.

```
MACHINE DSL_Composition
    INCLUDES CM_DSL, SRA_DSL
    PROMOTES
        selectConfig, validateConfig, setQoS, /* from CM DSL */
        selectThreat, computeDefenses, initSRA /* from SRA DSL */
```

Figure 6 gives the B data structures and their typing invariants that are produced by Meeduse from the composition metamodel. Specializations of functional relations depend on the character of attributes and associations: single/multiple valued and mandatory/optional. Class `SecureConfiguration` is transformed into an abstract set named `SECURECONFIGURATION` that represents the set of possible instances of the class. Variable `SecureConfiguration` defines the effective instances of this class. We introduced in this machine the variable `theSecConf` in order to represent the current secure configuration that is managed by a given process.

```
SETS
    COMPOSITION; SECURECONFIGURATION
VARIABLES
    SecureConfiguration, sra, cm, validConfig, validDefenses, secureConfigs,
    isValidSecConf, maxQoS, relativeCost, theSecConf
INVARIANT
    /* Object Definition */
    SecureConfigurationsubseteqSECURECONFIGURATION
    /* Associations */
    srainCOMPOSITION→SRA
    cmCOMPOSITION→CM
    validConfiginSecureConfiguration→Configuration
    validDefensesinSecureConfiguration↔Defense
    secureConfigsinSecureConfiguration→COMPOSITION
    /* Attributes */
    validSecConfinSecureConfiguration→BOOL
    maxQoSinSecureConfiguration→REAL
    relativeCostinSecureConfiguration→REAL
    /* added variable */
    theSecConfinSECURECONFIGURATION
```

<caption>Fig. 6. B data of the composition machine</caption>

Regarding the inter-DSL properties P1, P2 and P3 introduced in Section
2, they are formally defined as follows. This invariant means that if a secure
configuration is created (i.e. becomes an existing instance) and validated, then P1, P2 and P3 hold.

## DEFINITIONS

$$ \mathit{sumDefCost}(sc) == \sum \mathit{def}. (\mathit{def} \in \mathit{validDefenses}[\{sc\}] | \mathit{costDef}(\mathit{def})) $$

$$ \mathit{approve}(sc) == $$

$$ \mathit{sumDefCost}(sc) + \mathit{QoS}(\mathit{validConfig}(sc)) \leq \mathit{maxQoS}(sc) $$

$$ \land \mathit{sumDefCost}(sc) \leq \mathit{relativeCost}(sc) \times \mathit{QoS}(\mathit{validConfig}(sc)) $$

$$ \land \mathit{validDefenses}[\{sc\}] \neq \emptyset $$

## INVARIANT

$$ \mathit{theSecConf} \in \mathit{SecureConfiguration} \land \mathit{isValidSecConf}(\mathit{theSecConf}) = \mathbf{TRUE} $$

$$ \Rightarrow \mathit{approve}(\mathit{theSecConf}) $$

The dynamic parts of the various B machines contain B operations that specify the execution semantics of our DSLs. We provide for example the specification of operation `approveSecureConfig` that is defined in the *DSL Composition* machine:

## OPERATIONS

$$ \mathit{approveSecureConfig} = $$

PRE

$$ \mathit{theSecConf} \in \mathit{SecureConfiguration} $$

$$ \land \mathit{isValidSecConf}(\mathit{theSecConf}) = \mathbf{FALSE} $$

$$ \land \mathit{approve}(\mathit{theSecConf}) $$

THEN

$$ \mathit{isValidSecConf}(\mathit{theSecConf}) := \mathbf{TRUE} $$

END

All our specifications have been proved correct via the AtelierB prover [6]. The latter produces Proof Obligations (POs), which correspond to theorems that require proof in order to verify the correctness and consistency of a B machine. AtelierB offers an automatic prover able to prove the majority of POs automatically, without any user interaction. This makes it easy to quickly verify large parts of the system specification, and reduces the burden on the user to manually prove each individual PO. The prover also provides interactive prover designed for handling and finalizing complex proofs, also for detecting errors in the specifications.

With AtelierB, we generated 299 POs. Most of them have been proved automatically; only 10 POs have been discharged manually using the interactive prover. The latter ones required additional information to be completed and corrected. The proof using AtelierB provides the guarantee that all the invariants of our DSLs are preserved by the formal specifications of their execution semantics and that the composition is correct with regards to these invariants and the security properties.

## 4.3 BPMN Formalization with a CSP Transformation

Having the B specifications, the formalization of the coordination model can be treated. Our objective is to apply the workflow of the BPMN model to the
<figure><img src="image_9.png" /><figcaption>Fig. 7. Transformation of pools into CSP</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 8. Parallel synchronisation of pools</figcaption></figure>

## 4.4 Discussion

The CSP model and the B specifications that describe the semantics of DSLs provide a formal framework that is managed by ProB and Meeduse in order to ensure the animation as well as the verification. First, Meeduse evaluates the formal B specifications from the models of Figures 1 and 2. The resulting valuations are then delivered to ProB, which allows a step-by-step animation of B operations. The execution of DSLs in Meeduse using ProB is well mastered today and has been discussed in [10]. However, the shortcoming of this approach is the absence of guidance during animation, which makes it inconvenient for DSL collaboration. In order to address this limitation, we suggest to apply the CSP||B approach. The idea is to marry CSP and B such that the execution of a B operation corresponds to an event that can be enabled in CSP, which provides
a guidance all along the animation process. Roughly speaking, the B machine
and the CSP process must synchronise on common events, that is, an operation
can only happen in the combined system when it is allowed both by the B and
the CSP. For more details about this technique we refer the reader to [3].

We have tested several executions of our coordination model based on our
case study, leading to the creation of several secure configurations with various
threats and defenses. Figure 9 shows the animation of the composition B ma-
chine presented in Section 4.2 guided by the CSP model of Figures 7 and 8,
using the ProB tool. In the *History* window, an example of execution scenario
that creates a new secure configuration is shown. The *Enabled Operations* win-
dow lists operations that can be called at this stage and whose execution will
satisfy their precondition, and therefore preserve the state invariant. The *State
Properties* window provides the current value of each state variable of the com-
position machine. At the animation step, we can observe the insurance of system
properties P1, P2 and P3 introduced in Section 2.3 and specified as invariants
in the composition B machine in Section 4.2.

<figure><img src="image_11.png" /><figcaption>Fig. 9. ProB screenshot showing animation and verification of inter-DSL collaboration</figcaption></figure>

Regarding verification, one of the advantages of B is the availability of the-
orem provers and model-checkers. We did not discuss in details this activity
but note that all our formal specifications have been proved, which guarantees
the correctness of the B models on which we built the coordination process. In-
deed, our approach ensures the correctness and reliability of the resulting RTE
system, which can help preventing dangerous situations that can be caused by
overcurrent in the transmission lines.

# 5 Related Work

The problem of managing the interactions between models is not new and it has been addressed in various fields including Artificial Intelligence, Robotics, and Control Systems. In the context of Model Driven Engineering (MDE), the proposed solutions are categorized into two classes: composition and coordination approaches [16]. The composition approaches build a model specifying the structural relationships between model elements. The composition model is specified using matching operators that define the syntactic similarities between model elements and merging operators that implement rules to specify how the matched elements must be composed. The operators are provided by dedicated languages such as Epsilon [14]. The composition model can also be defined by composing the syntax of different model languages into a new language syntax expressed by a metamodel [7]. As part of the composition approaches, F. Jouault et al. [12] combine megamodeling and model weaving techniques to build an environment that ensures traceability and navigation between the DSLs models. The environment represents links between different DSL models, which provides an intuitive way to understand relationships between them. However, these composition approaches consider only the language's static syntax; they focus on traceability without taking into account execution semantics.

In coordination approaches, a new model is often built to define how the models behave and interact with each other. Dedicated languages (e.g. Linda [9]) have been proposed for this purpose. There also exist some coordination frameworks, such as ModHel'X [2], to automate and support the coordination process. However, the coordination is encoded using a general-purpose programming language (Java), which is not suitable for performing verification and validation. As part of the GEMOC project<fnref n="2" />, Larsen et al. [17] propose the B-COOl language that allows specifying a coordination pattern between DSLs. The language offers concurrency and communication models representing the control-flow aspects, including the synchronisation and the causality relationships between execution functions. This is close to some CSP operators, but the missing piece is the usage of provers and model-checkers for automatic verification activities. In our work we apply well-known formal languages (B and CSP) and an established semi-formal notation (BPMN), which enables the application of widely used tools for modeling and verification.

Our approach combines the composition and coordination techniques. We build a composition metamodel that refers to the coordinated DSLs metamodels without altering their semantics and behaviors. BPMN diagram is used for expressing the coordination process between the DSLs. The DSLs metamodels and the BPMN coordination model are then transformed into a formal specification to be used for checking and validating the DSLs models coordination.

<footnote n="2">² https://gemoc.org/</footnote>
# 6 Conclusion

This paper presented a tool-supported approach for the formal modeling and verification of inter-DSL collaboration. The approach extends the Meeduse framework by integrating a composition metamodel and BPMN model to explicitly specify inter-DSL collaboration. The formal specification generated from the models and metamodels is then used to verify the DSLs models coordination. The proposed approach was demonstrated to be effective through its successful application in a real case study.

Going forwards, the next steps include implementing and validating the transformation rules from BPMN to CSP, as well as expressing and checking properties at the workflow level. These developments will further enhance the automation and reliability of the proposed approach.

# Data Availability Statement

The artifact is available in the Software Heritage repository:

swh:1:dir:c38d7336f13f438eab7212227f10fb0dbf0350c1

# References

1. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996). https://doi.org/10.1017/CBO9780511624162

2. Boulanger, F., Hardebolle, C.: Simulation of multi-formalism models with model'x. In: 2008 1st International Conference on Software Testing, Verification, and Validation. pp. 318 – 327 (05 2008). https://doi.org/10.1109/ICST.2008.15

3. Butler, M., Leuschel, M.: Combining CSP and B for Specification and Property Verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods. pp. 221–236. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)

4. Chehida, S., Baouya, A., Bozga, M., Bensalem, S.: Exploration of Impactful Countermeasures on IoT Attacks. In: 9th Mediterranean Conference on Embedded Computing, MECO 2020, Budva, Montenegro, June 8-11, 2020. pp. 1–4. IEEE (2020), https://doi.org/10.1109/MECO49872.2020.9134200

5. Chehida, S., Idani, A., Cortes-Cornax, M., Vega, G.: GitHub Artifacts, https://github.com/SalimChehida/Inter-DSL-Collaboration

6. Clearsy: Atelier B, https://www.atelierb.eu/en/

7. Emerson, M., Sztipanovits, J.: Techniques for metamodel composition. OOPSLA - 6th Workshop on Domain Specific Modeling (01 2006)

8. Flavio, C., Alberto, P., Barbara, R., Damiano, F.: An ECLIPSE Plug-In for Formal Verification of BPMN Processes. In: 2010 Third International Conference on Communication Theory, Reliability, and Quality of Service. pp. 144–149 (2010). https://doi.org/10.1109/CTRQ.2010.32

9. Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM 35(2) (1992)

10. Idani, A.: Meeduse: A Tool to Build and Run Proved DSLs. In: Integrated Formal Methods: 16th International Conference, IFM 2020, Lugano, Switzerland, November 16–20, 2020, Proceedings. Springer-Verlag, Berlin, Heidelberg (2020)
11. Idani, A., Ledru, Y., Ait Wakrime, A., Ben Ayed, R., Bon, P.: Towards a Tool-Based Domain Specific Approach for Railway Systems Modeling and Validation. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Springer International Publishing (2019)

12. Jouault, F., Vanhooff, B., Bruneliere, H., Doux, G., Berbers, Y., Bezivin, J.: Inter-DSL Coordination Support by Combining Megamodeling and Model Weaving. In: Proceedings of the 2010 ACM Symposium on Applied Computing. p. 2011–2018. SAC ’10, Association for Computing Machinery, New York, NY, USA (2010)

13. Kleine, M.: CSP as a Coordination Language. In: De Meuter, W., Roman, G.C. (eds.) Coordination Models and Languages. pp. 65–79. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)

14. Kolovos, D.S., Paige, R.F., Polack, F.A.C.: Merging Models with the Epsilon Merging Language (EML). In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) Model Driven Engineering Languages and Systems. Springer Berlin Heidelberg (2006)

15. Kordy, B., Mauw, S., Radomirović, S., Schweitzer, P.: Foundations of Attack-Defense Trees. In: Degano, P., Etalle, S., Guttman, J. (eds.) Formal Aspects of Security and Trust, vol. 6561, pp. 80–95. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)

16. Larsen, M.E.V.: BCOol : the Behavioral Coordination Operator Language. Ph.D. thesis, University of Nice Sophia Antipolis, France (2016)

17. Larsen, M.E.V., DeAntoni, J., Combemale, B., Mallet, F.: A Behavioral Coordination Operator Language (BCOoL). In: Proceedings of the 18th International Conference on Model Driven Engineering Languages and Systems. MODELS ’15, IEEE Press (2015)

18. Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. International Journal on Software Tools for Technology Transfer **10**, 185–203 (2008)

19. Milner, R.: A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg (1982)

20. OMG: Business Process Model and Notation (BPMN), Version 2.0 (January 2011), http://www.omg.org/spec/BPMN/2.0

21. OMG: Unified modeling language™ (uml®) (2011), http://www.omg.org/spec/UML/index.htm

22. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, USA (1997)

23. Schneider, S., Treharne, H.: CSP Theorems for Communicating B Machines. Form. Asp. Comput. **17**(4), 390–422 (dec 2005), https://doi.org/10.1007/s00165-005-0076-7

24. Tourchi Moghaddam, M., Rutten, E., Giraud, G.: Hierarchical Control for Self-adaptive IoT Systems : A Constraint Programming-Based Adaptation Approach. In: HICSS 2022 - Hawaii International Conference on System Sciences. pp. 1–10. Hawaii, United States (Dec 2022), https://hal.inria.fr/hal-03461137