2. Second iteration: we partition state $val_{m-2}$ into two sub-states:

$$val_{m-3} \hat{=} val_{m-2} \wedge \neg Pre(op_{m-1})$$

$$val_{m-2} \hat{=} val_{m-2} \wedge Pre(op_{m-1})$$

* **case 1:** we choose $op_{m-1} = meetingNew(m_1, John)$, and then we have:
  $Pre(meetingNew(m_1, John)) \hat{=} m_1 \notin meeting \wedge John \in person$, and
  $val_0 \nrightarrow val_{m-2}$ because $John \notin person$

In this case, the algorithm does not find an operation permitted to John leading to a state where operation *meetingNew* becomes enabled. Indeed, no operation satisfies PO (6). In the other side, PO (5) succeeds for all operations. Our algorithm concludes that there does not exist an attack scenario invoking *meetingNew* in step $m-1$ (Figure 3.8).

<figure><img src="image_48.png" /><figcaption>Figure 3.8: No state enabling operation *meetingNew* is found</figcaption></figure>

* **case 2:** we choose $op_{m-1} = personAddMeetingOwner(John, m_1)$. We have:
  $Pre(personAddMeetingOwner(John, m_1)) =$
  $m_1 \in meeting \wedge John \in person \wedge (John, m_1) \notin MeetingOwner$

$$\begin{align*} val_{m-2} \hat{=} & \neg(m_1 \in meeting \wedge meetingOwner\{(m_1)\} = John) \wedge \\ & m_1 \in meeting \wedge John \in person \wedge (John, m_1) \notin MeetingOwner \\ & \hat{=} m_1 \in meeting \wedge John \in person \wedge (John, m_1) \notin MeetingOwner \end{align*}$$

$$\begin{align*} val_{m-3} \hat{=} & \neg(m_1 \in meeting \wedge meetingOwner\{(m_1)\} = John) \wedge \\ & \neg(m_1 \in meeting \wedge John \in person \wedge (John, m_1) \notin MeetingOwner) \\ & \hat{=} m_1 \notin meeting \vee (meetingOwner\{(m_1)\} \neq John \wedge John \notin person) \end{align*}$$

$$val_0 \nrightarrow val_{m-2} \text{ because } John \notin person$$

In this case, PO (6) succeeds for operation *personNew*, which means that if this operation is executed, it may lead to a state where operation *meetingNew* can be enabled. Operation *personNew* may be executed by *John* as system administrator.
3. Third iteration: we partition state $val_{m-3}$ into two sub-states:

$$ 
\begin{aligned}
val_{m-3} &\hat{=} val_{m-3} \wedge Pre(personNew(John)) \\
&\hat{=} John \notin person \wedge (m_1 \notin meeting \vee meetingOwner\{(m_1)\} \neq John)
\end{aligned}
 $$

This stops normally the algorithm because in this case $val_0 \Rightarrow val_{m-3}$. Figure 3.9 presents the full symbolic scenario that allows John to modify Alice's meeting.

<figure><img src="image_49.png" /><figcaption>Figure 3.9: Symbolic malicious scenario for user John.</figcaption></figure>

### 3.3.5 Discussion

Technically, our approach applies the GeneSys tool in order to produce proof obligations and then asks the AtelierB prover to discharge them automatically. As the resulting scenarios are symbolic and based on "possibly reached proofs", the analyst can conclude that attacks may exist but he can not guarantee their existence for the concrete system. An interesting contribution of our proof-based symbolic sequences, besides the fact that they draw the analyst's attention to potential flaws, is that they give useful inputs to the model-checker. Indeed, a model-checking tool can be used to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. For example, based on the symbolic sequence of Figure 3.9, ProB was able to extract the malicious concrete scenario represented in Figure 3.10. In order to reduce significantly the state space, we can ask ProB to explore only operations found in the symbolic malicious scenarios. For our example, when trying only operations personNew, personAddMeetingOwner and meetingSetStart, ProB exhibits a concrete attack scenario after visiting a dozen of states which shows a significant speed up with respect to our initial ProB attempts (involving more than 1000 states).

Our technique was able to extract another scenario (Figure 3.11) which can be executed by user Bob holding the supervisor role from the same initial state, in order to steal the ownership of $m_1$. In this scenario, Bob first cancels the meeting and then he recreates it before applying the critical operation. The first scenario, done by user John, is made possible by the full access permission to class Person, associated to role SystemAdministrator, which includes the right to modify association ends. This attack affects meeting integrity. One solution can be to add an SSD (Static Separation of Duties) constraint between roles SystemAdministrator and SystemUser.
John will then still be able to become owner of the meeting, but will not be able to log in as SystemUser in order to modify it.

The second scenario done by Bob was possible due to role Supervisor which gives him the right to cancel a meeting, and then, as a SystemUser he can recreate it in order to become its owner. This scenario does not point out a flaw since whenever a meeting is cancelled it should be legitimate that a user can start a new meeting with the same identifier as the cancelled one.

Our algorithm was able to extract all possible sequences leading to the state that enables the critical operation. The security breaches that our technique is looking for, are issued from flaws in the conceptual logic of the security policy. Then, the produced sequences don't violate the access control policy, but they must be checked carefully by the security analyst in order to decide whether it is an attack scenario (e.g attack 3.10 done by John) or a legitimate access (e.g scenario 3.11 performed by Bob).

<figure><img src="image_50.png" /><figcaption>Figure 3.10: John’s scenario.</figcaption></figure>

<figure><img src="image_51.png" /><figcaption>Figure 3.11: Bob’s scenario.</figcaption></figure>

## 3.4 Related Work

Several research works have been devoted to the validation of access control policies. They are mainly focused on detecting external intrusion. Recently, the interest to insider attacks grew leading to two categories of validation: stateless and dynamic access control validation.

Stateless access control validation is dedicated to validate security policies in a given state without taking into account the dynamic evolution of the IS states. Among these works we can
cite the SecureMova tool (Basin et al., 2009) which models security policies using SecureUML and OCL expressions. In the same context, Kuhlmann et al. (2013) took advantage on the USE tool to model RBAC policies in OCL in order to express authorization constraints and to query about access control rules. Far from UML modeling, Fisler et al. (2005) developed the Margrave tool to answer the same kind of stateless queries by analysing RBAC models written in XACML and translated into a form of decision-diagram. Also, some interesting works (Toahchoodee et al., 2009b, Zao et al., 2003) using Alloy language have been defined to analyse access control policies. Even though authors have not sought to study the dynamic evolution of functional states and their effect on the authorization constraints, we believe that a tool like Alloy could support such analysis. Note that such stateless queries can be performed easily based on the formal B specifications produced by the B4MSecure platform. The main limitation of a stateless access control validation is that it does not indicate whether the given state is reachable, or not, and then it may lead to incomplete conclusions.

Dynamic access control validation attempts to identify strategies followed by malicious users to counter some security rules by taking advantage of the IS states evolution. In (Qamar et al., 2011b), we proposed interactive dynamic analysis with the help of a Z animator, but this approach requires user insight and may miss some possible flaws. Zhang et al. (2005, 2008) proposed a backward algorithm to find a strategy allowing the attacker to reach a target state. A plain model-checking approach is proposed in order to check specifications written in the RW (Read-Write) language. On the one hand, the proposed algorithm suffers from scalability for the verification of complex specifications because of combinatorial explosion of the state space; and on the other hand, the RW language is poor compared to B because it doesn't express complex functional behaviours. The authors propose a contribution towards identifying strategies involving multiple users in coalition. This aspect is not covered in this paper and is planned for further work. A similar approach is proposed in (Koleini and Ryan, 2011) in order to validate access control policies of web-based collaborative systems. Even though their experiments show that they achieve better results compared to the approach in (Zhang et al., 2005, 2008), it is still a model-checker solution that can not deal with policies of huge size.

Becker and Nanz (2010) approach is the most similar approach to ours. Indeed, they proposed a Hoare-style proof system based on a Logic for State-Modifying (SMP) in which they express reachability properties in terms of pre and post-conditions. They reason about an abstract set of target states that satisfy some constraint. They also implemented a backward algorithm that extracts the sequence of operations leading to the goal state. Their algorithm is also able to compute the minimal sequence. However, the use of a logic-based language like SMP is not adequate for the context of Information Systems with a need to express complex functional behaviours. Moreover, the use of a proof system on a symbolic model may produce a sequence which cannot be reproduced in the concrete model. To circumvent this shortcoming we proposed in our approach to combine both proofs and model-checking techniques.

Our proof based symbolic search is achieved by assessing reachability properties (Bert et al., 2005) of functional operations. Other works proposed to explore this kind of properties in
order to reason on sequences of B operations. In (Mammar and Frappier, 2015), the authors proposed two approaches to prove reachability properties in a B formal information system modelling. In the first one, they used substitution refinement techniques based on Morgan's specification statement, and in the second one, they proposed an algorithm that produces a proof obligation to be discharged automatically by AtelierB in order to prove whether a given sequence of operations reaches (or not) a defined state. The proposed techniques may help for our work since it is a proposal to simplify proofs and make them easier for AtelierB. However, unlike our approach, they don't search sequences leading to a goal state from an initial one. Their approach starts from a given sequence of operations, and tries to prove its reachability.

## 3.5 Conclusion

This chapter described a symbolic search approach that can extract insider malicious behaviours from a formal Information System modelling. The meeting scheduler example was discussed in several articles (Basin et al., 2006, 2009). However, they do not report the attack scenarios presented in this paper. This is due to the fact that dynamic evolution of the functional state is not taken into account. We showed how dynamic analysis, assisted by proofs and model-checking, is useful to find out potential threats. In addition, thanks to our algorithm, proofs and model checking tools, our method can be automated in order to extract attack scenarios breaking some authorization constraint. We also applied our approach on several case studies and we were able to find, automatically, the discussed threats.

Our approach is automated thanks to B4MSecure<fnref n="1" />, GeneSyst<fnref n="2" />, AtelierB<fnref n="3" /> and ProB<fnref n="4" />. First, B4MSecure translates functional and security graphical models into B specification, from which we automatically produce proof obligations of enabledness and reachability properties using GeneSyst. Then, these proof obligations are discharged automatically using the AtelierB prover. When a symbolic scenario is found, ProB is used to explore the concrete state space focusing on operations issued from the symbolic scenario. We developed GenISIS, a new tool that implements our algorithm and integrates all the tools mentioned above in order to have a complete automated solution. The main limitation of our work is that sometimes, when proof obligations are complex, AtelierB fails to prove them automatically. Interactive proofs are then required, but they may be pretty difficult for the analyst. One naive solution is to keep operations for which proofs don't succeed automatically in order to be exploited further using the model-checker. A more interesting solution is to focus on other kinds of proof obligations. For example, one can try to prove that an operation *op* is never enabled from a state *E* and/or *op* never reaches a state *F*. Applying these proofs to the meeting scheduler example we were able to eliminate half of the operations after proving automatically that they cannot be involved in the attack scenario.

<footnote n="1">¹ http://b4msecure.forge.imag.fr</footnote>

<footnote n="2">² http://perso.citi.insa-lyon.fr/nstouls/?ZoomSur=GeneSyst</footnote>

<footnote n="3">³ http://www.atelierb.eu/</footnote>

<footnote n="4">⁴ http://www.stups.uni-duesseldorf.de/ProB</footnote>
2nd part

# Building correct DSLs
<figure><img src="image_52.png" /></figure>
# Chapter 4

## Formal Model-Driven Executable DSLs

### Contents

<table><tr><td>4.1</td><td>DS(M)L's semantics</td><td>97</td></tr><tr><td>4.2</td><td>Preliminary study and critical review</td><td>101</td></tr><tr><td>4.3</td><td>A Formal Model-Driven Petri-net DSL</td><td>107</td></tr><tr><td>4.4</td><td>Debugging with PNet<sub>Reference</sub></td><td>114</td></tr><tr><td>4.5</td><td>Conclusion</td><td>117</td></tr></table>

This chapter is an excerpt issued from these two papers:

Akram Idani. Formal model-driven executable DSLs: Application to Petri-nets. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 18(4), 2022. URL https://doi.org/10.1007/s11334-021-00408-4.

Akram Idani, Yves Ledru, and German Vega. Alliance of Model Driven Engineering with a Proof-based Formal Approach. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 16(3):289-307, 2020. URL https://doi.org/10.1007/s11334-020-00366-3.

Model Driven Engineering (MDE) is an interesting paradigm in software systems development because it provides solutions to the software complexity on the one hand, and it shows how to bridge the gap between conceptual models and coding
activities, on the other hand. The definition and the use of domain specific models through-
out the engineering life-cycle makes MDE a powerful asset. Furthermore, MDE is assisted
by numerous tools (EMF<fnref n="1" />, XText<fnref n="2" />, ATL<fnref n="3" />, etc) dedicated to put into practice a clear separation
of concerns ranging from requirements to target platforms, and going through several design
stages. Interoperability between these tools is favored by the use of standardized meta-modeling
formalisms which increases automation especially for developing domain specific modeling
languages (called DSMLs). These advantages reduce the risk that human errors such as mis-
interpretation of the requirements and specification documents lead to erroneously validate the
specification, and hence to produce the wrong system. Still, while model-driven DSLs provide
solutions to the validation problem (“do the right system”), the verification problem (“do the
system right”) remains a major challenge due to the lack of formal reasoning tools in MDE
platforms.

Contribution

This chapter shows how we define mappings between DS(M)Ls as they are defined in MDE
techniques and the rigorous world of formal methods. Our approach is assisted by Meeduse
(Idani, A., 2020b), a tool that we developed in order to translate a DS(M)L meta-model into an
equivalent formal B specification that represents its semantic domain, using the set theory and
the first order predicate logic. In MDE, the design of a DS(M)L addresses two main layers:
meta-modeling and modeling. Meta-modeling refers to the definition of the language abstract
syntax where domain concepts and their relationships are defined independently from their
concrete representation. The modeling layer allows one to create instances of these domain
concepts by applying a predefined concrete syntax (graphical or textual). Our approach applies
the formal B language to both layers. At the modeling layer, the abstract data-types generated
from the meta-model layer, become valuated data types, which allows animation. Regarding
the DSL behavioral semantics, they follow the same principles. Indeed, they are defined over
the meta-modeling layer using high-level B operations, which are then animated by Meeduse
on the modeling layer.

This alliance between MDE and a formal method, assisted by Meeduse, makes domain spe-
cific models provable and also executable thanks to the animation of their expected behaviour
directly in a dedicated DS(M)L tool. The interest of Meeduse is that it integrates the ProB
JAVA API (Körner et al., 2020). Given a model designed in the DS(M)L tool, Meeduse injects
it as valuations in the generated B specification and calls ProB in order to compute the list of
operations that may be animated from these valuations. When an operation is animated the tool
computes the new variable valuations and then it translates back these valuations to the initial
model which results in an automatic animation of domain models. This technique allows one to

<footnote n="1">¹ EMF: https://www.eclipse.org/modeling/emf/</footnote>

<footnote n="2">² Xtext: https://www.eclipse.org/Xtext/</footnote>

<footnote n="3">³ ATL: http://www.eclipse.org/atl/</footnote>
take benefit of formal reasoning tools such as provers and model-checkers throughout the MDE
process. The proposed method uses the AtelierB prover to guarantee the correctness of the
model's behavior with respect to its invariant properties, and the ProB model-checker in order
to animate underlying execution scenarios. Besides the use of these automatic reasoning tools
in MDE, proved B refinements have been investigated in order to gradually translate abstract
models to concrete ones that can then be automatically compiled into a programming language.

Structure

This chapter is structured as follows:

* Section 4.1 discusses the meaning of DS(M)Ls semantics and presents an overview of our approach to formally define these semantics.

* Section 4.2 summarizes an experimental study that we have done with several tools dedicated to executable DSLs, and gives our observations and lessons learned.

* Section 4.3 shows how the semantics of a DSL can be formally defined using the B method and CSP.

* Section 4.4 illustrates some debugging activities that can be done using the Meeduse tool.

* Section 4.5 draws the conclusion of this chapter.

4.1 DS(M)L's semantics

Execution of Domain Specific (Modeling) Languages (DS(M)Ls) is an active research area in
Model Driven Engineering (MDE). The intention is to be able to perform early analysis of a
system's behavior before its implementation. Indeed, execution a DS(M)L tends to reduce the
gap between the model and the system, since DS(M)Ls would not only represent the expected
system's structure and behaviour but they can themselves behave as the system should run. In
this work we apply a formal approach in order to define, prove, and execute the underlying
semantics of a DS(M)L. This section presents an overview about DS(M)L semantics as they are
defined in the state of the art and explains the main principles of our approach.

**4.1.1 Abstract syntax and semantic domains**

Bryant et al. (2011) discuss challenges and directions about DSLs semantics and point out that their formal definition is the foundation for several benefits: automatic generation of some DSL tooling, formal analysis of a model’s behavior, and/or composition of concerns issued from different languages. The authors define the semantics of a DSL as a mapping from its abstract syntax to some semantic domain. The abstract syntax defines the modeling concepts, their
relationships and attributes; and the semantic domain is some mathematical framework whose meaning is well-defined. In the same direction, Harel and Rumpe (2004) state that a semantic domain is a well-defined and well-understood agreement on a language's meaning.

In MDE, the notion of abstract syntax is well mastered today thanks to the concept of meta-model (which is standardized by the Meta-Object Facility (MOF) document (Object Management Group, 2015)). However, the notion of semantic domain remains unclear because, on the one hand, the MOF is informally defined, and on the other hand, a common misconception in modeling languages is to confuse semantics with behaviours as stated in (Harel and Rumpe, 2004). In fact, the description of a behaviour is itself a DSL with its own abstract syntax and semantic domain. For example, several MDE tools define the simple Petri-net DSL using a common meta-model, but they apply various languages (Kermeta, xMof, fUML, java) to define the expected behaviour when firing a petri-net transition. These languages are additional DSLs with different semantic domains that lead to different behaviours when executing the same Petri-net model with different tools.

Meta-models are therefore not sufficient to describe the behaviour of a DSL, that's why some attempts exist in order to enhance meta-models by action languages, e.g. Kermeta (Bousse et al., 2018); or to translate meta-models into a target language that offers behavioural facilities, e.g. Java (Hartmann and Sadilek, 2008). In our approach we apply this second strategy, called translational in (Bryant et al., 2011), but we use the formal B language (Abrial, 1996), which offers a way to mathematically define the semantic domain of a DSL. In our approach we adopt a deep embedding approach when translating a DSL meta-model into the B language. The formal semantic domain of a DSL will represent data typing with the corresponding structural constraints defined in set theory and first order logic. Regarding the DSL behaviour, it is defined using B operations that can be manually written, like presented in this chapter or generated from additional DSLs that can describe behaviours. In (Idani, A., 2020b) we proposed to produce the B operations from a coloured Petri-nets DSL.

### 4.1.2 Dynamic semantics vs Behavioural semantics

Several research works have been devoted in order to provide solutions with tools that make DSLs executable. In Model-Driven Engineering, DSL execution mainly refers to the definition of semantics, which are roughly called by means of several terms like dynamic, operational, executable and/or behavioural. Jézéquel et al. (2013) refer to behavioral semantics of a DSL, as the semantics that allow to run a program. They identify two kinds of behavioral semantics: translational semantics and operational semantics: a translational semantics would result in a compiler while an operational semantics would result in an interpreter. In (Muller et al., 2005), a different definition is provided without a distinction between operational semantics and behavioral semantics. The authors refer to a high level execution defined over meta-models and which uses actions (also called operations) to define model's behaviour. Similarly to programs which are made of data structures and algorithms, in (Muller et al., 2005) an executable DSL is made of meta-data and actions. The various definitions that we found mix low-level notions
(compilers, programs, etc), and high level notions (meta-models, etc). This is less the case for
programming languages where the terms dynamic semantics and execution semantics are used
to describe the runtime behavior of programs (Vergu et al., 2015). The so-called dynamic (or
execution) semantics in programming languages, "defines how and when the various constructs
of the language produce artifacts (e.g. bytecode) that can be executed in a given target platform
(Floyd, 1993) (e.g. virtual machine)".

For clarity we use terms dynamic and execution semantics of a DSL as soon as a run-
time environment is concerned which is close to programming languages (Vergu et al., 2015,
Floyd, 1993). Terms operational and behavioral semantics for us are inspired by (Muller et al.,
2005) and they are limited to high level actions that describe how models behave. The gap
between both semantics, does not make them conflicting because at a high level one can de-
fine behaviours of models and at a low level this behaviour can be translated into a runtime
environment. The challenge is how to guarantee the compatibility between the resulting exe-
cutions: that of a model given its operational semantics, and that of the runtime program given
its dynamic semantics. Works of U. Tikhonova (Tikhonova et al., 2013, Tikhonova, 2017a,b)
bridge this gap between operational and dynamic semantics, by providing reusable specification
templates which are templates that allow to explicitly define the dynamic semantics of a DSL
over its operational semantics. These templates are presented in the form of a library of spec-
ifications, each of which formalizes a separate software solution. The operational semantics
of a DSL are then expressed as a composition of these specification templates, which favours
some kind of generic programming of the DSL dynamic semantics. However, the use of a spec-
ification templates library makes several restrictions to the definition of semantics because it
is not obvious to cover all possible behavioural needs with various abstraction levels. In our
proposal, we address the semantic gap between operational and dynamic semantics of a DSL
thanks to the refinement paradigm of the B method which allows to produce step-by-step a low
level implementation of a DSL from its high level description.

4.1.3 Executable DS(M)Ls in Meeduse

Figure 4.1 summarizes how we put into practice the alliance of MDE with a proof-based formal approach in order to define DS(M)Ls with formal semantics and favour their execution. Our tool support named Meeduse<fnref n="4" /> links three technological spaces: EMF (Steinberg et al., 2009) for model driven engineering, B Method (Abrial, 1996) for proofs and refinements, and finally the execution of the target system. The top hand side of figure 4.1 represents the abstract syntax of a DSL by means of an ECore meta-model, its mapping to the corresponding formal semantics domain (box B Machine), and its operational semantics which starts from the description of an abstract behavior and applies refinements until the specification of its concrete behavior (boxes abstract behavior, refined behavior and concrete behavior). The bottom hand side of figure 4.1 defines the dynamic semantics of the DSL since it is an extraction of an executable language

<footnote n="4">⁴ Meeduse: Modeling Efficiently EnD USEr needs (http://vasco.imag.fr/tools/meeduse/).</footnote>
from the high level DSL artifacts. We build our approach on several components: Translator, Injector, Animator and Trace runner.

<figure><img src="image_53.png" /><figcaption>Figure 4.1: Meeduse overview</figcaption></figure>

(1) **Translator**: this component translates an Ecore (Steinberg et al., 2009) meta-model into an equivalent B specification gathering the structure of the meta-model as well as basic operations like constructors, destructors, getters and setters. The resulting B specification can be enhanced manually by additional invariants and its proof of correctness with respect to these invariants can be done using AtelierB prover. Technically, the tool translates an ECore model into an UML model and then applies B4MSecure to produce a formal B machine representing the functional aspects of the DSL.

(2) **Injector**: injects instances of a meta-model, which can be designed using EMF-based modeling tools (like Sirius, GMF, XText, etc) into the B specification produced from the meta-model. This component introduces enumerations into abstract data structures like abstract sets, and hence allows valuations of the B machine variables.

(3) ** Animator**: animation of B specifications is done using the ProB JAVA API (Körner et al., 2020). The Animator component asks ProB to animate B operations and gets the reached state by means of B variables valuations. Then, Meeduse computes the equivalence between these valuations and the initial EMF model and applies the necessary modifications to the model in order to keep this equivalence all along the animation process.
(4) Trace runner: this component plays a sequence of operations issued from an execution trace by animating the corresponding B operations, which leads to automatic modifications of the model. Thanks to this component, animation can be done from outside EMF by an external program which is running in the target platform. Note that the target platform source code can be produced by applying MDE transformations or by using the code generator of AtelierB after successive refinements. In both cases, the trace runner is useful on the one hand, for conformance validation between the model and the execution, and on the other hand for some kind of runtime verification. In (Idani, A. et al., 2020), we presented the first strategy where an implementation in the C language is generated by AtelierB from the most concrete B machine.

## 4.2 Preliminary study and critical review

In (Idani, A., 2022, 2020a) we experimented several existing MDE implementations of Petri-nets applying Java, QVT, Kermeta and fUML. We tried them to debug a safety-critical system in order to check their ability to address properties such as: correctness, deadlock freedom, mutual exclusion and fairness. This section gives the lessons learned from this study and discusses why formal alternatives are required to ensure the correctness of DSLs.

### 4.2.1 A simplified Petri-net DSL

Petri-net (Petri and Reisig, 2008) is a visual language used for modelling concurrent systems. Its mathematical foundations inspired by the graph theory allow formal calculus about safety properties. The choice of this DSL is motivated by the fact that it is often used as an illustrative case by the research works and tools interested in modeling and debugging techniques, and also because it has had a wide range of applications in safety critical systems. This section builds on a simplified version of this DSL and defines a Petri-net based safety-critical example.

#### 4.2.1.1 Structural and contextual semantics

Figure 4.2 shows the simplified Petri-net meta-model as considered by (Bousse et al., 2018, Deantoni, 2016). It is composed of three meta-classes: Net (the root class), Place and Transition. These classes are linked by four relationships: places, transitions, input and output. This meta-model defines structural features of a given Petri-net. For instance, a transition must be linked to at least one input place and one output place. Attribute tokens represents the number of tokens in a place: it is single-valuated, optional and without a default initial value. The various references of this meta-model don't admit repetitions. Note that the meta-model is taken from (Bousse et al., 2018)<fnref n="5" /> and it is presented without any modification. There exist some variations of this meta-model where transitions admit both 0 inputs and 0 outputs. Furthermore, the Petri-net DSL must comply with the following contextual invariant written in OCL:

<footnote n="5">⁵ The corresponding ECore file can be found at (Petri-net ecore file, 2020).</footnote>
context Place
inv Token_Is_Natural: self_tokens ≥ 0

<figure><img src="image_54.png" /><figcaption>Figure 4.2: Petri-nets meta-model.</figcaption></figure>

For illustration we use the Petri-net of figure 4.3 that controls traffic lights in a crossroad. In some sense, this model deals with a safety-critical system since failures may lead to loss of life due to accidents that it may cause. This model represents two traffic lights (Light 1 and Light 2) that are to be placed in two roads that intersect. These traffic lights are respectively controlled by the left side and the right side of this figure. Every traffic light sequentially switches from Green to Orange and then to Red, in an infinite loop. This Petri-net model shows concurrent evolutions of traffic lights without any synchronisation between them. Finally, the current state of this model assigns red to Light 1 and green to Light 2.

<figure><img src="image_55.png" /><figcaption>Figure 4.3: Traffic light controller in petri-nets (V1)</figcaption></figure>

In our study we supposed that by using a Petri-net debugger, a domain expert would like to verify some safety properties such as:
* correctness: asserts that the system does not exhibit bad behaviors, where invariants (structural or contextual) are violated.

* deadlock-freedom: states that the traffic lights can't be blocked in a state in which no progress is possible

* mutual exclusion: states that lights in a road intersection cannot enter simultaneously their critical sections (critical sections are states green and orange in our example).

* fairness: requires that the system gives fair turns to its components (in our example both lights must be able to function).

### 4.2.1.2 Execution semantics

Basic execution semantics of the Petri-net DSL are defined by means of transition firing which holds when a transition satisfies an enabledness property. To check this property, we require to call a query defined as:

```
query isEnabled(t : Transition) : Boolean =
    t.input->forAll(p : Place | peditkens > 0)
```

This query returns true if attribute tokens is greater than 0 for each input place of transition *t*, false otherwise. Algorithm of figure 4.4, taken from (Bousse et al., 2018), describes how a Petri-net runs.

<figure><img src="image_56.png" /><figcaption>Figure 4.4: Running a Petri-net.</figcaption></figure>

This algorithm chooses non-deterministically (operator $\notin$) a transition *t* (called $t_{enabled}$) from the set of transitions that satisfy the enabledness property and then calls operation *fire*(*t*).
As a result the number of tokens in the input places of *t* is decreased (operation *removeToken*) and the number of tokens in the output places is increased (operation *addToken*). Modifications of tokens, done at every call to operation fire, modify the set of enabled transitions. The algorithm may loop or stop when this set becomes empty.

### 4.2.1.3 Benchmark

In order to debug the aforementioned safety properties using various MDE approaches and observe their strengths and limitations, our experimental study was built on approaches that are widely accepted in the MDE literature: Java, QVT, Kermeta and fUML. In the remainder, we refer to them respectively as: PNet<sub>Java</sub>, PNet<sub>QVT</sub>, PNet<sub>Kermeta</sub> and PNet<sub>fUML</sub>. Our choice was also motivated by the fact that these approaches are the only ones that we found, where the Petri-net DSL was already implemented, in addition to the availability of the underlying artifacts (source code, publications, tutorials). Furthermore, tools assisting these approaches use the Eclipse Modeling Framework (EMF), which makes easy their integration and the analysis of the Petri-net DSL within a unified MDE framework.

**PNet<sub>Java</sub>** (Hartmann and Sadilek, 2008). Java-based semantics of the petri-net DSL are proposed in (Hartmann and Sadilek, 2008) and supported by a tool named EProvide (2020). This java implementation is easily reproducible in the Eclipse Modeling Framework. The approach is combined with graphical editor creation in order to support rapid prototyping of animated visual interpreters and debuggers.

**PNet<sub>QVT</sub>** (Wachsmuth, 2008). QVT (Query/View/Transformation) is an OMG standard for model transformations. QVT defines: QVT-Relations and QVT-Core which are declarative languages but at two different levels of abstraction, and QVT-Operational which is an imperative language. Wachsmuth (2008) used QVT-Relations which is the high-level language of QVT extending OCL and its semantics with imperative features.

**PNet<sub>Kermeta</sub>** (Deantoni, 2016, Bousse et al., 2018). Kermeta (Jézéquel et al., 2013) is a language workbench that involves different meta-languages for abstract syntax (aligned with EMOF (Object Management Group, 2015)), static semantics (aligned with OCL) and behavioural semantics. In (Deantoni, 2016, Bousse et al., 2018), the Gemoc studio was applied together with the Kermeta/XTend language to define the petri-net DSL and debug its execution using an animation technique.

**PNet<sub>fUML</sub>** (Langer et al., 2014, Mayerhofer et al., 2013). fUML (Object Management Group, 2011) is an OMG standard that defines the execution semantics of a subset of UML 2.3. The standard applies, in the form of pseudo Java-code, a basic virtual machine enabling UML models using elements comprised in the fUML subset to be executed. Mayerhofer et al. (2013)
proposes the xMOF tool which integrates fUML with MOF to enable the specification of the
behavioural semantics of DSLs in terms of fUML activities.

## 4.2.2 Ascertainment and discussion

### 4.2.2.1 Challenges

There exist several well established tools (Thong and Ameedeen, 2015) that implement the Petri-net theory for verification purposes and apply various programming languages. However, even if most of them are open-source, it remains difficult to update their code in order to experiment various semantics. Not only the developer must have high programming skills, but he/she must also understand the tool logic, which is a very challenging task especially for tools dedicated to formal languages. To this purpose, a MDE solution is much more suitable, because it allows one to reason on the DSL itself, rather than on how the DSL is encoded in a given programming language. Our works focus on MDE tools dedicated to DSL execution and debugging, and apply them to the Petri-net DSL, together with a formal approach. The objective is to benefit from the rich catalog of MDE tools without losing sight of correctness and rigorous development. Indeed several MDE tools exist: model-to-model transformation, model-to-code generation, constraint-checkers, graphical concrete syntax representation, bi-directional mappings, etc. The approach of PNet<sub>Java</sub> proposes to support stepping back in the execution history of a DSL. PNet<sub>QVT</sub> investigated model-to-model transformations as a way to define execution semantics of a DSL. PNet<sub>Kermeta</sub> relies on generic trace management to provide an omniscient debugger thereby allowing developers to “go back in time” (Lienhard et al., 2008). Finally, PNet<sub>fUML</sub> proposed a new meta-modeling language (xMOF) for specifying the abstract syntax and behavioral semantics of DSLs based exclusively on standardized modeling languages (fUML and MOF). We experimented these tools being guided by two point of views:

* The end-user point of view: the end-user of a Petri-net is often either a Petri-net expert who is interested by verification features (such as model-checking), or a domain expert who is interested by interactive animation and/or simulation. Note that the experimented approaches were not interested by verification, but rather by validation; and hence we focused on debugging rather than on proofs and model-checking.

* The developer point of view: we assume that the developer of a Petri-net DSL has a good knowledge of the Petri-net theory and his/her intention is to provide a bug-free tool. Thus, we look at how existing tools encoded the semantics of the Petri-net DSL in order to locate the critical parts and find the origin of failures when they happen.

### 4.2.2.2 Observations

Unfortunately, even if our benchmark tools address several interesting features and challenging directions for DSL development, their application to the Petri-net DSL is limited to the
simplified semantics. As they didn't go further towards the realistic Petri-net DSL, it is diffi-
cult to objectively evaluate the usefulness of the resulting models for verification. Hence, our
objective was not to check the correctness of their Petri-net case study — since their underly-
ing approaches didn't deal with correctness — but rather to build a formal MDE Petri-net and
illustrate its contributions based on existing simplified implementations from which unsafe be-
haviours were exhibited. Indeed, our main observation is that even if it seems easy to use MDE
tools to develop the semantics of a language, the developer can miss obvious details without a
good support for verification. Furthermore, this may weaken the general approach of executable
DSLs when applied for debugging complex and safety-critical systems.

The analysis of our benchmark for simplified Petri-nets showed that failures or unsafe be-
haviours may originate from several artifacts:

* The meta-model and its underlying modeling operations, because often execution semantics apply the modeling operations to update the input model. In order to safely update the model, our approach generates a set of pre-established modeling operations that are correct by construction, meaning that they will never violate the structural features of the meta-model.

* The model itself, because incorrect behaviours may not be exhibited from models, especially when the DSL builder applies internal choices that are not conformant to the standard semantics. To cope with this issue we have done a systematic analysis of the MOF semantics for all the constructs that are covered by our approach and provided a suitable transformation from ECore to B.

* The implementation of the operational semantics that may be distant or not conformant to the DSL's specification. This is a validation problem that requires the involvement of a domain expert. In the context of the Petri-net DSL the semantics are mathematically defined, which is compatible with the usage of a formal method such as B.

* The execution engine of the meta-language. For example, EMF/OCL based engines wrongly support non-determinism as discussed in (Baar, 2005, Vallecillo and Gogolla, 2017). In our case, the execution engine is the ProB animator and model-checker (Leuschel and Butler, 2008). This powerful tool has had several successful industrial applications that address safety-critical systems.

The four implementations of our benchmark tools are highly simplified and used for illustra-
tion only. The underlying approaches are accepted by the MDE community and have the ability
to design and correctly instrument DSLs. From our experiments PNetJava gave the better exe-
cution outputs however it suffers from its poor abstraction. PNetQVT gave the better abstraction
level however it suffers from limitations of the misuse of non-determinism. Finally, PNetKermeta
and PNetUML proposed a controllable deterministic behaviour by enabling the first transition
satisfying the enabledness property.
### 4.2.2.3 Added-value and limitations

To cope with the aforementioned limitations, we proposed an alternative solution, to the Petri-net DSL. The correctness of our solution is attested by theorem proving and its execution is managed by an animator. Section 4.3 presents our solution and Section 4.4 shows how the B method can help during the verification and validation activities. The challenge is therefore to show by practice how and why a formal model-driven executable DSL is developed and executed. The Petri-net DSL is widely applied in safety-critical systems for verification and simulation (Thong and Ameedeen, 2015), and hence we believe that the application of a formal method to this DSL is a strong requirement. Moreover, in order to go beyond the simplified illustrative case we applied our solution to PNML (Petri-Net Markup Language), the international standard ISO/IEC 15909 for Petri-nets, providing formal and realistic basis that may be useful for possible improvements of other MDE tools. This application is presented in the next chapter.

A major limitation of our FMDE approach is that the integration of a formal method within MDE tools is not an easy task. Indeed, a major difficulty is that usually a MDE expert does not have knowledge of formal methods; and often, proofs and model-checking is not widespread because it seems to create an overhead for the developer. In (Andova et al., 2012), the authors state that: "[...] the learning curve of formal methods is steep, whereas the learning curve for drawing diagrams on the black board is very low.". This observation is true due to the complexity of the mathematical notations that support formal methods.

Nonetheless, when language analysers, such as compilers, are used for safety-critical or high-assurance software, Leroy (2009) attests that "validation by testing reaches its limits and needs to be complemented or even replaced by the use of formal methods such as model checking, static analysis, and program proof". In our proposal we advocate for collaborations between the formal methods community and the MDE community in order to take benefits of their respective tooling. Our approach (Idani, A. et al., 2020), and its tool support Meeduse (Meeduse, 2020, Idani, A., 2020b), favor this collaboration since it makes possible the use of DSL builders and formal methods tools together in one unified framework (i.e. EMF). The DSL tool development is the task of MDE experts who have the skills to define meta-models with associated static constraints, and the formal semantics specification is the task of the formal methods experts who are experienced in provers and model checkers.

## 4.3 A Formal Model-Driven Petri-net DSL

The disparity between DSL execution tools leads to behaviours that are conformant to the semantics specified by their execution models but which may be far from the expected behaviour in accordance with the domain expertise. This is an important problem since the same model may not be executed in the same way on different tools even for deterministic structures. In fact, when designing a model via a given DSL tool, the domain expert focuses on debugging his/her model rather than debugging the DSL semantics provided by the MDE expert.
In (Idani, A., 2022), we proposed an alternative definition of the Petri-net semantics (that we call PNet<sub>Reference</sub>) using Meeduse. The use of a well-established formal approach assisted by provers and model-checkers, would at least guarantee the consistency of the Petri-net DSL and its conformance to the expected semantics. The proposed formal model-driven Petri-net DSL builds on the B method (Abrial, 1996) and the CSP (Hoare, 1985) process algebra (Communicating Sequential Processes).

### 4.3.1 Static semantics

In order to get a formal B specification of the static semantics of a DSL, Meeduse translates its meta-model into a correct-by-design B specification. This translation extracts a UML model from the ECore file of the meta-model, and then applies B4MSecure. Figure 4.5 gives the structural part of the generated B machine.

<figure><img src="image_57.png" /><figcaption>Figure 4.5: Structural part of the Petri-nets machine</figcaption></figure>

The invariant covers structural properties defined by multiplicities and the optional/mandatory character of attributes, as well as contextual constraints like the `Token_Is_Natural` invariant. For example, predicates from line (18.) to line (23.) translate multiplicities `1..*` associated to references input and output. Attribute tokens which is single-valued, optional and defined over the set of natural numbers, is translated into a partial function from set `Place` to the B type `NAT` (see line (17.)). Note that in EMF this type does not exist, which then requires the additional OCL constraint in the EMF-based tools. In Meeduse it is possible to mix predefined EMF/UML basic types with those defined in the B language.

### 4.3.2 Modeling operations

Our objective is to use Meeduse in order to reproduce the EMF process for editing models, but in the rigorous world of a formal method. Indeed, EMF generates a Java implementation from
a meta-model gathering all basic operations (setters, getters, etc) and Meeduse generates a B machine gathering similar basic operations but which are written in a theory (set theory, first order predicate logic and generalized substitutions) allowing to carry out proof of correctness. Figure 4.6 shows the basic setter of attribute `tokens` produced by Meeduse. By default, this setter preserves invariant properties since it affects a natural number to attribute `tokens` thanks to precondition: `val ∈ NAT`.

<figure><img src="image_58.png" /><figcaption>Figure 4.6: Basic setter of attribute tokens</figcaption></figure>

Figure 4.7 gives two cases of the place creation operation that depend on the optional/mandatory character of attribute tokens. An attribute without an initial value in the meta-model leads to two possibilities: (1) if the attribute is mandatory then the B constructor requires a parameter to assign an initial value to the attribute and (2) if it is optional then the constructor creates a place with an undefined attribute value.

<figure><img src="image_59.png" /><figcaption>Figure 4.7: Constructors of class Place</figcaption></figure>

The B operations generated by Meeduse are conceptually more accurate than the unique java translation used in EMF-based DSL tools because they guarantee the preservation of the structural features of the meta-model. From this specification, AtelierB generated 74 proof obligations (POs) for which it was able to automatically prove 62. The 12 other POs were proved interactively without any improvement of the B specifications.
### 4.3.3 Operational semantics

Tools of our benchmark used (meta-)programming languages with algorithmic facilities in order to define the operational semantics of Petri-nets. In our approach we use additional B operations to those generated automatically and we propose to coordinate them using CSP process algebra. Besides theorem proving, this formal background, allows one to apply associated animation and model-checking tools in order to rigorously debug and verify the various models.

Operational semantics often introduce complex modifications to the domain-specific model: they may create or destroy objects, modify relationships between these objects and also update several class attributes at the same time. We are then afraid that the difficulty in applying executable DSLs in safety-critical systems goes beyond the failures we were able to exhibit from our benchmark tools, i.e. overflow typing or implicit assignment of default values, or even non-determinism. In our opinion, this issue needs a methodological background and a clear separation of concerns regarding the properties to verify:

1. those of the meta-model with associated modeling operations (e.g. setToken, ...),

2. those of the user-defined operations (e.g. addToken, removeToken, ...),

3. those of the coordination mechanism (e.g. operations fire and run of figure 4.4).

The first kind of properties is covered by the functional model (machine nets of figure 4.5) extracted automatically from the meta-model. The resulting B specification gathers modeling operations and can be enhanced by additional invariants in order to take into account contextual properties and prove its correctness. The two other kinds of properties would be introduced by an expert in formal methods based on this functional model. This is a similar approach to a classical MDE technique where first EMF generates a Java API from a meta-model and then frameworks for executable semantics suggest the use of specific languages (like QVT, Kermeta, etc). In our approach this specific language is that of the B method.

We define operational semantics using B operations in an additional machine that we call semantics in the following. This machine includes the functional machine nets in order to be able to explicitly call its operations. Contrary to the java protected field produced by EMF from attribute tokens, in B the only way to modify a variable outside the machine in which it is defined, is to use operations provided by the latter. The Petri-net implementations of our benchmark are simple cases because they should address mainly two basic properties: the first one about attribute tokens that belongs to natural numbers was discussed in the previous section, and the second one is about transition enabledness. This property should not only take into account the positive value of tokens (relation Place_tokens) for all input places (input⁻¹[{tt}]) of a transition tt but must also take into account the upper limit of this attribute for all output places (output⁻¹[{tt}]). Operation getEnabled (figure 4.8) is a formalisation of query isEnabled presented in section 4.2.1.2. Substitution ANY ... WHERE ... END gets any transition tt satisfying preconditions:
$$ (P1) \text{ Place\_Tokens}[\text{input}^{-1}[\{\text{tt}\}]] \cap \{0\} = \emptyset $$

$$ (P2) \text{ Place\_Tokens}[\text{output}^{-1}[\{t\}]] \cap \{\text{MAXINT}\} = \emptyset $$

```pascal
tEnabled ← getEnabled =
    ANY tt WHERE
        tt ∈ Transition ∧
        {0} ∩ Place_tokens(input⁻¹[{tt}]] = ∅ ∧
        {MAXINT} ∩ Place_tokens(output⁻¹[{tt}]] = ∅
    THEN
        tEnabled := tt
    END;
```

<caption>Figure 4.8: Operation getEnabled</caption>

Since relation Place_tokens is defined over natural numbers, it is not necessary to use the `forAll` primitive inside the precondition like in the OCL query. The precondition of operation `getEnabled` simply verifies if values `0` and `MAXINT` belong to the sets of tokens issued from the input and output places of `tt`. Precondition (P1) is not sufficient because we would like to safely increase the number of tokens in the output places. Without precondition (P2), the Petri-net controller may then reach a state in which a transition is enabled, and the tokens in its input places are consumed without producing tokens in the output places. This would lead to an inconsistent Petri-net because consumption and production of tokens should not be dissociated. Both preconditions are then required in order to be able to call both `addToken` and `removeToken` when a transition is enabled. Figure 4.9 gives the B specification of operations `addToken` and `removeToken`.

```pascal
removeToken(pp) =
    PRE
        pp ∈ Place ∧ pp ∈ dom(Place_tokens) ∧
        Place_tokens(pp) > 0
    THEN
        Place_SetTokens(pp, Place_tokens(pp) - 1)
    END;

addToken(pp) =
    PRE
        pp ∈ Place ∧ pp ∈ dom(Place_tokens) ∧
        Place_tokens(pp) < MAXINT
    THEN
        Place_SetTokens(pp, Place_tokens(pp) + 1)
    END;
```

<caption>Figure 4.9: Operations addToken and RemoveToken</caption>
Every operation has three preconditions allowing the success of the POs computed by the
AtelierB prover:

* the parameter typing predicate $pp \in Place$,

* the definition domain of the **tokens** number (greater than zero or less than maxint), and

* predicate $pp \in dom(Place_Tokens)$ which asserts that attribute **tokens** is assigned to a value for place $pp$. This predicate guarantees the well-definedness PO of application $Place_Tokens(pp)$. Indeed, in order to be able to read the value of attribute **tokens** from a given place, the program must verify that the value is not undefined for that place.

Both operations **addToken** and **removeToken** call the basic setter **Place_SetTokens** (figure 4.6) of the functional model, and hence they preserve the meta-model invariant properties. As the Petri-net running algorithm iterates over input and output places of a transition, we enhance machine **semantics** by an additional getter (figure 4.10) which returns these sets given a transition *tt*. Finally, AtelierB discharged four proof obligations from this machine (two POs for the setter call, and two additional POs for the well-definedness of *Place_Tokens(pp)*) and it was able to prove them automatically.

```
src, trg ← getPlaces.tt() =
```

PRE

$tt \in Transition$

THEN

```
src := input⁻¹ [{tt}]
```

```
|| trg := output⁻¹ [{tt}]
```

END;

<caption>Figure 4.10: Operation getPlaces</caption>

### 4.3.4 Semantics coordination

Machine **semantics** provides B operations that are proved correct. It guarantees that any running algorithm based on these operations will not lead to violations of the model's properties. The notion of algorithm in the oxford dictionary (Oxford, 2020), is defined as: "an algorithm is a process or set of rules to be followed in calculations or other problem-solving operations". In order to keep reasoning at a high abstraction level, and be faithful to this definition, operations **run** and **fire** presented as algorithms in figure 4.4, will be defined as CSP<fnref n="6" /> processes that coordinate operations of machine **semantics**. The process algebra CSP is an event-based formalism that enables description of patterns of system behaviour. Butler and Leuschel (2005)

<footnote n="6">⁶ CSP: Communicating Sequential Processes Hoare (1985).</footnote>
propose a combination of CSP and the B method and its integration within ProB. This formalism is then useful for executable DSLs due to its abstraction capabilities and also thanks to its integration within ProB. Figure 4.11 provides the main CSP constructs. In this section we apply the following ones:

* simple action prefix $a \to P$ where $a$ is a B operation name (called channel in CSP) possibly followed by a sequence of outputs ($!v$) and inputs ($?var$) such that $v$ is a value expression and $var$ is a variable identifier.

* sequential composition ($P ; Q$) meaning that the execution of process $Q$ follows that of process $P$.

* process interleaving ($P ||| Q$) where the resulting execution traces are the arbitrary interleaving of traces issued from each process.

* guarded process ($g : P$) which is the execution of process $P$ under a condition defined by guard $g$.

<table><caption>Figure 4.11: Some commonly used CSP operators</caption><thead><tr><td>Operator</td><td>Syntax</td></tr></thead><tbody><tr><td>stop</td><td>STOP</td></tr><tr><td>skip</td><td>SKIP</td></tr><tr><td>prefix</td><td>$a \to Q$</td></tr><tr><td>conditional prefix</td><td>$a?x : C \to P$</td></tr><tr><td>external choice</td><td>$P \sqcap Q$</td></tr><tr><td>internal choice</td><td>$P \sqcap Q$</td></tr><tr><td>interleaving</td><td>$P ||| Q$</td></tr><tr><td>parallel composition</td><td>$P \llbracket A \rrbracket Q$</td></tr><tr><td>sequential composition</td><td>$P ; Q$</td></tr></tbody></table>

Figure 4.12 shows the CSP specification of the petri-net running algorithm. This algorithm is composed of four processes: RUN, FIRE, CONSUME and PRODUCE. Process RUN (line 2.) is a recursion defined by a sequential composition with the prefixed process FIRE. In this sequence channel getEnabled?trans is a call to the B operation getEnabled whose output value is registered in variable trans which is then transmitted to process FIRE. Concretely, variable trans represents an enabled transition provided non-deterministically by operation getEnabled. The simulation of process RUN continues indefinitely or stops when the system reaches a deadlock. Process FIRE, applied to a transition trans, is a sequencing of processes CONSUME and PRODUCE preceded by the simple action prefix: getPlaces!trans?input?output. This action is a call to the B operation getPlaces on transition trans in order to get its input and output places which are further transmitted to processes CONSUME and PRODUCE. These two processes apply respectively operations removeToken and addToken to all elements of sets input and output. Notation $|||_{[x \in S]}$ Op!x represents a replicated interleaving which applies all possible combinations of Op having the various valuations of parameter $x$ taken from set $S$.
1. MAIN = RUN

2. RUN = getEnabled?trans → FIRE(trans) ; RUN

3. FIRE(trans) =

4. getPlaces!trans?input?output → (

5. CONSUME(input) ; PRODUCE(output)

6. )

7. CONSUME(input) = |||[x∈input]removeToken!x → SKIP

8. PRODUCE(output) = |||[x∈output]addToken!x → SKIP

<caption>Figure 4.12: CSP formalisation of run and fire</caption>

## 4.4 Debugging with PNet<sub>Reference</sub>

In Meeduse, ProB and EMF are applied together in order to take benefit of the visualisation capabilities of tools like Sirius and GMF, and the animation and model-checking functions of ProB. In this preliminary study we used the first version of Meeduse (Figure 4.13); it was just a prototype that is used as a proof of concepts.

<figure><img src="image_60.png" /><figcaption>Figure 4.13: Integration of ProB within EMF</figcaption></figure>

EMF and ProB were synchronized at every animation step using a notification mechanism, which allowed us to debug the traffic light via PNet<sub>Reference</sub>. We have two possibilities to apply the ProB tool:
1. interactive animation, which is useful for domain experts,

2. model-checking, which allows sophisticated analysis of reachability properties.

First, Meeduse interprets an input EMF model, such as the traffic light model of figure 4.2 and injects its elements as valuations in the formal specification of the meta-model. These valuations (bottom part of figure 4.13) allow ProB to initialize the B machine and start animation. The right side of figure 4.13 provides the ProB view and the left side shows our Sirius modeler that we developed for the simplified Petri-net case study. The ProB view shows CSP guided animation of machine semantics. In the current state of the model two operations are enabled: start1 and t2. In interactive animation, depending on the choice done by the user, the tool fires the selected transition and then changes the model according to the formal B specification. For every animation step, Meeduse gets the B machine state from ProB and translates it back to the EMF model in order to update the graphical view. As presented in figure 4.13, ProB offers model-checking functions allowing to find deadlocks, invariant violations and reachability of CSP goals.

### 4.4.1 Mutual exclusion

The mutual exclusion property can be expressed by the following invariant which excludes a state where traffic lights are simultaneously in their critical sections. A traffic light enters its critical section after enabling transition start and it leaves it by transition end meaning that the critical section includes states Green and Orange:

$$ 
\begin{aligned}
& 1 \in Place_tokens[\{green1, orange1\}] \\
& \Rightarrow Place_tokens[\{green2, orange2\}] = \{0\} \\
\wedge \quad & 1 \in Place_tokens[\{green2, orange2\}] \\
& \Rightarrow Place_tokens[\{green1, orange1\}] = \{0\}
\end{aligned}
$$

In order to check whether this mutual exclusion property holds or not for our Petri-net model, we add this invariant to machine semantics and we ask ProB to find invariant violations starting from several possible initial states. ProB successfully found all the expected invariant violations and also produced the corresponding transition sequences (called counter-examples). ProB provides several interesting facilities to debug a formal specification in order to improve it. Figure 4.14 shows the improved petri-net model where place sync is added between transitions start and end. Note that currently Meeduse does not provide means to apply the feedback produced by ProB (such as trace analysis, invariant decomposition, etc) to the input EMF model. The introduction of place sync is hence done after checking the trace produced by ProB when it found the invariant violation. From the initial state of Figure 4.13 both start1 and start2 can be enabled because their input places have the required number of tokens. If start1 (respectively start2) is fired then the token of place sync will be consumed which
forbids Light 2 (respectively Light 1) to enter its critical section. This token will be restored after firing transition *end1* (respectively *end2*). From this Petri-net model ProB didn't find any invariant violation after visiting all possible nodes of the state space. This proof guarantees the mutual exclusion property of the improved traffic-light.

<figure><img src="image_61.png" /><figcaption>Figure 4.14: Improved petri-net for mutual exclusion (V2)</figcaption></figure>

## 4.4.2 Fairness

In order to check this property we apply a parallel composition of process RUN with process FAIRNESS defined in figure 4.15, line (12.). This process leads to two possible traces:

* (*step1* ; *step2* ; *goal*), and

* (*step2* ; *step1* ; *goal*)

Channel *step1* (respectively *step2*) is produced from process FIRE when guard *trans* = *end1* (respectively *trans* = *end2*) holds. The objective of this specification is to stop the running algorithm when goal STOP is reached, which means that the system produced a trace where both transitions *end1* and *end2* are fired by the RUN process. For the example of Figure 4.14 ProB successfully produced the expected sequences leading to the CSP goal process and showing that the system gives fair turns to lights 1 and 2. However, given that the running algorithm is non-deterministic, it would be interesting to seek for the existence of loops where only one light runs. For this purpose, we can override the getEnabled operation in process RUN as follows:

$$RUN = FIRE(start1) ; FIRE(t1) ; FIRE(end1) ; RUN$$

From this CSP rule, ProB covered the whole state space and didn't find a deadlock showing that the system may stay running without evolutions of Light 2. This proof exhibits a weak fairness from the model. To improve the traffic light Petri-net the domain expert can introduce
1. MAIN = RUN |[{step1, step2}]| FAIRNESS

2. RUN = getEnabled?trans → FIRE(trans) ; RUN

3. FIRE(trans) =

4. getPlaces!trans?input?output → (

5. CONSUME(input) ; PRODUCE(output)

6. ) ;

7. ( (trans = end1) : step1 → SKIP

8. [] (trans = end2) : step2 → SKIP

9. [] (trans ∉ {end1, end2}) : SKIP )

10. CONSUME(input) = |||[x∈input]removeToken!x → SKIP

11. PRODUCE(output) = |||[x∈output]addToken!x → SKIP

12. FAIRNESS = (step1 → SKIP ||| step2 → SKIP) ; goal → STOP

<caption>Figure 4.15: Fairness checking with CSP</caption>

a sequencing mechanism (figure 4.16) and replay the fairness checking, first with the CSP specification of figure 4.15 for non-regression and next with the overriding of rule RUN as mentioned above. The latter ends with a deadlock because after FIRE(end1) it is not possible to go back and run again FIRE(start1). The fairness checking with the CSP specification of figure 4.15 provides the same result as previously meaning that this petri-net controller gives fair turns to lights 1 and 2 without any loop where only one light runs.

<figure><img src="image_62.png" /><figcaption>Figure 4.16: Final traffic lights petri-net (V3)</figcaption></figure>

Note that by deleting place sync from figure 4.16 the resulting execution traces, with regard to the elements issued from the initial model, are included in the ones issued from figure 4.14. We can therefore assume that the fairness property is a refinement of the mutual exclusion property, and hence reduce the Petri-net model of figure 4.16 by deleting place sync.
## 4.5 Conclusion

Few proposals exist for bridging the gap between DSLs with their supporting tools and a proof based formal approach dedicated to execution semantics. The closest ones in comparison with the Meeduse approach in general are (Rivera et al., 2009) and (Gargantini et al., 2010a), where respectively MAUD and Abstract State Machines (ASM) are used. Unfortunately these works do not address the joint execution of the formal model and the DSL, which is a major contribution of Meeduse. One interesting perspective is to integrate several target formalisms within Meeduse being inspired by these works. In this chapter we applied our tool to the simplified Petri-net DSL. In the next chapter we propose several other applications, including PNML, the international standard ISO/IEC 15909 for Petri-nets. Before coming to this realistic application we tried several simplified implementations of this DSL applying MDE tools for DSL execution. The study allowed us to illustrate via several obvious details, how useful is a formal approach especially when addressing a DSL that is dedicated to safety-critical systems.

The major observation is that during the verification activities several concerns must be dissociated: properties of the meta-model, those of the execution semantics and finally those of the coordination algorithm. When an executable DSL is not carefully defined, it may lead to a succession of conceptual failures: failures of modeling operations (e.g. setTokens) may result in failures of execution operations (e.g. addToken), which in turn may result in failures of the coordination operations (e.g. fire/run). The major risk is that when debugging a model, the domain expert does not worry about the correctness of the DSL tool because it is basically the task of the MDE expert. In language programming the developer debugs his/her source-code (in MDE this is seen as a model) using existing IDEs without paying attention to how the language semantics are encoded since in the language theory these semantics are formally defined and compilers are well established techniques. Observations made by this work show that it is difficult to transpose debugging as used in language programming and compilers into executable DSLs especially for safety-critical systems.

Finally, we think that the application of executable DSLs in safety-critical systems require the collaboration of experts from both MDE and formal methods communities. The first actor defines the DSL with associated modeling tools and the second one defines the execution semantics with associated verification activities.
# Chapter 5

## Applications and case studies

### Contents

<table><tr><td>5.1 Application 1: Petri-net Markup Language</td><td>121</td></tr><tr><td>5.2 Application 2: Railway systems</td><td>129</td></tr><tr><td>5.3 Application 3: Model transformation</td><td>140</td></tr></table>

The systematic mapping study of Iung et al. (2020) shows that among the 59 existing language workbenches (LWBs) only 9 provide supports for verification, which is only done via testing (the formal dimension is completely absent). This is an important shortcoming because the absence of a good support for verification weakens the applicability of DSLs, especially for safety-critical systems. Indeed, in these systems correctness is a strong requirement and it is often addressed by the application of formal methods. During the last three/four years we investigated and developed a solution to this problem by proposing a Formal Model-Driven Engineering (FMDE) approach to create zero-fault DSLs, which are DSLs whose semantics are mathematically proved correct with regards to their structural and logical properties.

We developed the Meeduse tool to make the bridge between MDE and the formal B method. Technically the tool is built on EMF (Steinberg et al., 2009) (The Eclipse Modeling Framework) and ProB (Leuschel and Butler, 2008), an animator and model-checker of the B method that is certified T2 SIL4 (Safety Integrity Level), which is the highest safety level according to the Cenelec EN 50128 standard. ProB is also used by companies such as Alstom, Thales, Siemens, General Electric, ClearSy and Systerel. In addition to the formal reasoning about the semantics of DSLs, Meeduse offers execution and debugging facilities, which is a major contribution in comparison with other works built on DSLs and formal methods. The overall idea is that animation done in ProB is equivalently applied to the input EMF model leading to a correct model execution.
This chapter reviews progress made and three major realistic applications of Meeduse, which attests the interest and power of our FMDE approach to build executable DSLs (called in the remainder xDSLs).

Publications related to the applications of Meeduse

Akram Idani. The B Method Meets Petri-Nets: Shallow and Deep Embedding. LNCS
*Transactions on Petri-nets and Other Models of Concurrency*, 2022a. Submitted re-
vised version.

Akram Idani. The B Method meets MDE: Survey, progress and future. In *16th International Conference on Research Challenges in Information Science (RCIS)*, volume 446 of *LNBIP*. Springer, 2022b. URL https://doi.org/10.1007/978-3-031-05760-1_29.

Akram Idani. A Lightweight Development of Outbreak Prevention Strategies Built on Formal Methods and xDSLs. In *ACM European Symposium on Software Engineering (ESSE)*. ACM, 2021. URL https://doi.org/10.1145/3501774.3501787.

Akram Idani. Formal model-driven executable DSLs: Application to Petri-nets. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 18(4), 2022c. URL https://doi.org/10.1007/s11334-021-00408-4.

Akram Idani, Germán Vega, and Michael Leuschel. Applying Formal Reasoning to Model Transformation: The Meeduse solution. In *Proceedings of the 12th Transformation Tool Contest, co-located with STAF'2019*, volume 2550 of *CEUR Workshop Proceedings*, pages 33–44, 2019a.

Akram Idani, Yves Ledru, Abderrahim Ait-Wakrime, Rahma Ben-Ayed, and Simon Collart-Dutilleul. Incremental Development of a Safety Critical System Combining formal Methods and DSMLs — Application to a Railway System. In *24th International Conference on Formal Methods for Industrial Critical Systems (FMICS'2019)*, volume 11687 of *LNCS*, pages 93–109. Springer, 2019b.

Akram Idani, Yves Ledru, Abderrahim Ait-Wakrime, Rahma Ben-Ayed, and Philippe Bon. Towards a Tool-Based Domain Specific Approach for Railway Systems Modeling and Validation. In *Third International Conference on Reliability, Safety, and Security of Railway Systems (RSSRail'2019)*, volume 11495 of *LNCS*, pages 23–40. Springer, 2019c.
# Structure

1. Section 5.1: applies Meeduse to the execution semantics of PNML (Petri-Net Markup Language), the international standard ISO/IEC 15909 for Petri-nets, and shows the capabilities of the B method in the Petri-net field. This application led to a full-fledged tool called MeeNET (Meeduse for Petri-Nets).

2. Section 5.2: deals with railway systems (Idani, A. et al., 2019b,a). This application builds on a graphical DSL that can be used by railway experts to design railroad topologies and simulate (un)safe train movements.

3. Section 5.3: addresses model-to-model transformations (Idani, A. et al., 2019c). This application was carried out during the 12th edition of the transformation tool contest (TTC’19) and won two awards: best verification and audience award.

## 5.1 Application 1: Petri-net Markup Language

The previous chapter showed by practice how a formal model-driven executable Petri-net DSL can be developed, executed and debugged. The discussed example are mainly illustrative and were used to point out a major limitation of MDE tools: the lack of support for verification. Our approach introduces within these tools formal reasoning, which seems highly required especially when the DSL tool, such as a Petri-net based tool, has to be used for safety-critical systems. In the following we present MeeNET<fnref n="1" /> our formal Petri-net designer and animator, that is powered by Meeduse and built on top of PNML (Petri-Net Markup Language), the international standard ISO/IEC 15909 for Petri-nets.

### 5.1.1 PNML

The Petri-net community has worked several years ago on a standardized Petri-net DSL, called PNML (Petri Net Markup Language) (Hillah et al., 2009, PNML Homepage, 2020). The language provides an agreed-on interchange format that is compliant with a formal definition of Petri-nets. The standardization process ISO/IEC 15909 were set up by the community in order to provide a commonly used specification for Petri-nets. The standard covers three classes of Petri-nets: High-Level Petri Nets (HLPN), Symmetric Nets, and Place/Transition Nets (PT-Nets). Models of following sections belong to the third class (PT-nets). Nonetheless our approach can be applied to the two other classes.

We believe that for scalability it is important, for MDE tools and works that are dedicated to executable DSLs, to go beyond the illustrative case study and propose realistic applications based on PNML. Indeed, existing MDE tools have reached a good level of maturity and provide several powerful facilities such as omniscient debugging, trace optimisation, visualization,

<footnote n="1">¹ Demo videos can be found at: http://vasco.imag.fr/tools/meeduse/meenet/</footnote>
etc. Furthermore, open-source implementations of PNML and the underlying meta-models are already integrated within EMF. There exist two major platforms: The ePNK ePNK Homepage (2020) and PNML Framework Homepage (2020). In our work, as far as an ECore file of the meta-model is defined, Meeduse can be used, first to extract the formal static semantics from the file and prove its correctness, and then to execute input models if the formal B machine of the operational semantics is provided.

The aim of MeeNET is to provide a scalable executable formal specification of Petri-nets and experiment our approach on realistic input models. The underlying formal specification is currently experimented within The ePNK because this platform provides an extension point, so that new Petri-net types can be plugged in to the existing tool without touching the code of The ePNK. This mechanism is interesting from the Meeduse point of view because it is a kind of DSL refinement, which is a challenging topic for DSL execution and verification. As refinements are apart of the B method, then the tool opens interesting perspectives to this work. We partially address this perspective in the remainder.

## 5.1.2 The PNML Meta-model

PNML identifies concepts that are common to the three classes of Petri-nets in a so-called PNML Core model (figure 5.1). The common concepts are mainly places, transitions and arcs, and these objects can have some kind of label. The PNML core model provides means for splitting up larger Petri-nets into pages; connections between nodes on different pages can be established by reference places or reference transitions. PNML defines all kinds of graphical information that can be attached to the different elements, such as position, size, font-type, and font-size. Our objective is to formalise the executable part of PNML, so not all the PNML concerns are taken into account. For this reason Meeduse provides an annotation mechanism allowing the DSL developer to select the concepts to be translated into B. This mechanism provides also a way to precise the namings and to strengthen the properties of the meta-model such as multiplicities when required. Note that the current version of MeeNET does not yet cover the splitting of Petri-nets over pages, it is rather focused on the basic constructs. Classes RefPlace and RefTrans, for example, are not transformed into B.

In The ePNK, the PT-Nets class of Petri-nets is defined using an extension mechanism called Petri-net type definition (PNTD). Figure 5.2 shows the corresponding meta-model. It is the purpose of the PNTD to define the specialisations of meta-class Label that are possible in a specific class of Petri-nets, and also to define the additional restrictions on the legal connections. Figure 5.2 introduces two additional kinds of labels for Place/Transition systems: the initial marking for places, and the inscription for arcs. The initial marking can be any natural number (including 0) and the inscription for arcs can be any positive number. Technically, figures 5.1 and 5.2 are two distinct meta-models but one is the extension of the other (PT-Nets is the extension of PNML Core). In our approach, we support this extension mechanism using B refinements.
<figure><img src="image_63.png" /><figcaption>Figure 5.1: The PNML core model of ISO/IEC 15909-2 (2011) (ISO/IEC, 2011)</figcaption></figure>

<figure><img src="image_64.png" /><figcaption>Figure 5.2: The PNTD for PT-Nets (ePNK Homepage, 2020)</figcaption></figure>

### 5.1.3 Formal static semantics

In B, there are two kinds of refinements: behaviour refinement and data refinement.

* Behaviour refinement means that an algorithm is changed by another one but without vi-
olating neither the conditions under which the initial algorithm is defined nor its possible
executions. This kind of refinement would be useful to introduce step by step execution
semantics of a DSL. It is not illustrated in this work; we have defined the formal model
of the PT-nets execution semantics once and for all.

* Data refinement applies a new set of data in the refined model, that is some data can be replaced and some data can be added. This kind of refinement would be useful to introduce incrementally the static semantics of a DSL. This is suitable for the PT-nets class because its data are defined by introducing some additional meta-classes and by specializing some meta-classes from PNML Core.

Meeduse extracts from every meta-model a specific B machine defining its structural fea-
tures. In this case study, we get two B machines and then we manually establish a refinement
relation between them. Automatic DSL refinements is left to our future works, but we believe
that it can be automated by exploiting the annotation mechanism of Meeduse. By this approach,
it becomes possible to address the other Petri-net classes without any impact on the Core ele-
ments, because every Petri-net class would be defined as a specific refinement of PNML Core.

Figure 5.3 gives the variables and the invariants generated by Meeduse from PNML Core.
In this machine the inheritance is translated into set inclusion (*Place* ⊆ *PlaceNode* ⊆ *Node* ⊆
*Object* ⊆ *ID*). Variable *ID* refers to the objects identifiers. Regarding transitions and places,
they are not directly related with input and output references such as in the simplified case study.
In PNML Core, they are nodes, and their connections are defined by means of a class Arc.

<figure><img src="image_65.png" /><figcaption>Figure 5.3: Formal static semantics of PNML Core</figcaption></figure>
The formal static semantics of the PT-nets meta-model is given in Figure 5.4. It is a data
refinement of machine PNMLCore introducing several variables. In the meta-model, place
markings and arc annotations are defined with the XML data-types NonNegativeInteger and
PositiveInteger, as attributes of classes PTMarking and PTAnnotation. The translation into B
applies types NAT (natural integers) and NAT₁ (strictly positive natural integers) to the cor-
responding variables PTMarking_text and PTAnnotation_text. The initial marking of places
and the arc inscriptions are optional (multiplicity 0..1) and cannot be shared (because of the
containment). They are then translated into partial injections.

<figure><img src="image_66.png" /><figcaption>Figure 5.4: Formal static semantics of PT-nets</figcaption></figure>

The overall formal specification of the static semantics generated by Meeduse is about 457
lines of code. It provides 38 modeling operations from which the AtelierB prover produced 106
POs (95 were proved automatically and 11 using the interactive prover).

**5.1.4 Operational semantics**

In order to deal with the operational semantics of the PT-nets class of PNML, we introduce two
transient (not serialised) attributes: attribute marking of class Place to represent the current num-
ber of tokens in a place and attribute value of class Arc to represent the number of tokens that
are consumed and/or produced when transitions are fired. These attributes are single-valued,
mandatory and without an initial value. They are translated into total functions: *Place_marking* and *Arc_value*. Figure 5.5 shows the structural part of the execution semantics machine.

If a place is linked to a PTMarking via relation initialMarking then the corresponding value (represented with variable *PTMarking_text*) is assigned to its current marking (*initialMarking* ; *PTMarking_text*) in the initialization, otherwise the attribute is set by default at 0 ((*Place* – *dom*(*initialMarking*)) × {0}). The same principle is applied to attribute value of class Arc, but it takes value 1 if the arc does not have an inscription. In fact, when an inscription is not specified on the input arc (respectively the output arc) of a transition, then by default only one token is consumed from its source place (respectively one token is produced into its target place) when the transition is fired. The proof of correctness of this initialization guarantees that none of the place markings and arc values are missed and that they are conformant to their typing domains (NAT and NAT₁).

<figure><img src="image_67.png" /><figcaption>Figure 5.5: Structural part of the execution semantics</figcaption></figure>

MeeNET integrates Meeduse and the formal static semantics of PT-nets within The ePNK, which allows one to experiment several formal specifications for the execution semantics together with realistic PNML models. For illustration, we propose a different technique than the application of CSP||B. The following formalization (figure 5.6) is inspired by Attiogbe (2009) were Event-B was used to provide a faithful formal semantics to basic and high-level Petri-nets. The notation $\leftarrow$ denotes the overriding of a relation by another one. Operation fire selects non-deterministically a transition *tt* such that all its input places has a sufficient number of tokens; then it overrides relation *Place_marking* in order to update the markings of its input and output places. The various definitions used in this operation are given in figure 5.7 and the complete specification is provided in the appendix.

Sets *inputs*(*tt*) and *outputs*(*tt*) get respectively input and output nodes and arcs of a given transition *tt*. Note that set *inputs*(*tt*) is restricted to places from which the consumption is
fire =

ANY *tt* WHERE

*tt* ∈ Transition ∧

card(Inputs(tt)) = card(target⁻¹[{tt}])

THEN

Place_marking := Place_marking ⇏ consume.tt ;

Place_marking := Place_marking ⇏ produce.tt)

END

<caption>Figure 5.6: Operation fire used in MeeNET</caption>

possible (Arc_value(aa) ≤ Place_marking(pp)). Consumption and production of tokens are also
specified by means of set definitions. Set consume.tt (respectively produce.tt) computes the
new marking of the input (respectively output) nodes of a transition tt.

inputs.tt == {pp, aa | pp ∈ Place ∧ aa ∈ Arc
  ∧ source(aa) = pp ∧ target(aa) = tt
  ∧ Arc_value(aa) ≤ Place_marking(pp)
}

outputs.tt == {pp, aa | pp ∈ Place ∧ aa ∈ Arc
  ∧ target(aa) = pp ∧ source(aa) = tt
  ∧ Place_marking(pp) + Arc_value(aa) ≤ MAXINT
}

consume.tt == {pp, nn | pp ∈ **dom**(inputs.tt))
  ∧ nn = Place_marking(pp) - Arc_value(Inputs.tt)(pp))}

produce.tt == {pp, nn | pp ∈ **dom**(outputs.tt))
  ∧ nn = Place_marking(pp) + Arc_value outputs.tt(pp))}

<caption>Figure 5.7: Definitions</caption>

5.1.5 MeeNET

Figure 5.8 is a screenshot of MeeNET while executing a PNML file of a satellite memory
system. This file is taken from the benchmark of PNML files provided by the 10th edition of
the model-checking contest (MCC’2020)<fnref n="2" />. We designed the graphical and the tabular views in
Sirius in order to visualize graphically the model. For example, the green transitions (t1 and t4)
are transitions that can be fired in the current execution step. They satisfy the guard of operation
fire. The animation view and the state view represent the output of ProB. The animation view
is for interactive debugging, it allows the user to select which transition to fire; and State view
gives the current valuations of the B variables of the static semantics machine.

<footnote n="2">² The benchmark can be found at: https://mcc.lip6.fr/models.php</footnote>
<figure><img src="image_68.png" /><figcaption>Figure 5.8: A satellite memory PNML model</figcaption></figure>

The Petri-net of Figure 5.8 models the behaviour of the mass memory management system in a micro-satellite from the Myriade product line, designed by CNES, the French Space
Agency. The corresponding controller must ensure that there is always a “security buffer” between the sectors pointed by places p9 and p3. The size of this buffer is a parameter Y (whose value in this model is equal to 3). The system should guarantee the following invariant:

$$p3 > p9 \Rightarrow p3 - p9 \geq Y$$

Based on the valued B specification produced by MeeNET, the ProB model-checker explored all the state-space and showed that this property is preserved all along the execution of the Petri-net model. Other properties, such as LTL properties, are provided with the model and ProB was also able to check them.

We have tried several PNML files from the MCC’2020 in MeeNET (even the biggest ones) and it was able to produce a valued B specification that is further used in ProB for verification purposes. Nevertheless, our objective is not to evaluate the verification capabilities of ProB or its performance based on the resulting B models. The contribution of our work is that it made possible the use of ProB in the Petri-nets field. Further works and experiments are required if one would like to apply ProB to compete with established Petri-net based model-checkers.

## 5.2 Application 2: Railway systems

The emergence of DSL tools in safety-critical systems (James et al., 2013, Svendsen et al., 2012, Vu et al., 2014) allows domain experts themselves to provide useful structural models to the software system engineer who will then develop the operational aspects of the system. However, as far as we know, none of the existing works in the safety-critical domain, proposes a way to define proved formal links between the behavioural aspects of a system (in Petri-nets or other well known formalisms) and DSL tool development. In this section, we give an overview the work that we presented in (Idani, A. et al., 2019b). We start from an intuitive description of a safety critical system where the operational aspects are specified thanks to high-level Petri-nets, especially coloured Petri-nets (CP-nets), and the structural aspects are designed in a dedicated DSL. The challenge is therefore to merge both worlds (that of CP-Nets and that of DSLs) and then apply AtelierB in order to prove the correctness of the resulting system. Figure 5.9 gives the overall architecture that we propose to address this challenge.

The DSL meta-model and CP-Net models are automatically translated into B specifications which are enhanced by safety invariants and proved. Then, our approach defines linkage machines allowing to control the functional model and the associated DSL-tool thanks to the CP-Net specifications. Every linkage machine refines a CP-Net model and includes the functional model. This technique is different from the one discussed in section 5.1 for basic Petri-nets, since the objective is not to execute CP-nets, but rather use CP-nets in order to define the operational semantics of a given DSL. Indeed, by executing a CP-Net model, Meeduse plays with the DSL and verifies, via ProB, that the linkage invariants are preserved all along the animation.
<figure><img src="image_69.png" /><figcaption>Figure 5.9: Merging CP-Nets and DSLs in a formally defined framework</figcaption></figure>

### 5.2.1 ERTMS/ETCS Case Study

This work was funded by the NExTRegio project of IRT Railenium. The project aims at performing a system level analysis of a railway signalling system taking into account emergent solutions for train automation. Indeed, in the last decade, new technologies have been considered in railway systems in order to improve automation on the one hand and to reduce the operating costs on the other hand. In particular, the European ERTMS/ETCS<fnref n="3" /> (ERA, 2016, Schon et al., 2014) has emerged to replace various national signalling systems. There are three levels of ERTMS/ETCS which differ by the used equipments and the operating mode. The first two levels are already operational. However, ERTMS Level 3 is still in design and experimentation phases: it aims at replacing signalling systems by a global european one which is a GPS-based solution for the acquisition of train positions. In 2018, the ABZ conference (Butler et al., 2018), which gathers several formal methods communities, proposed a case study<fnref n="4" /> to model ERTMS/ETCS level 3 and has published several formal models. Unfortunately, these models do not combine the power of formal methods with domain specific approaches and hence they favour verification rather than domain expert validation. The application presented in this section contributes to the design phase of ERTMS/ETCS level 3 by mixing formal techniques and domain specific modeling in a well-known Model Driven Engineering (MDE) paradigm which makes easier domain expert validation.

An ERTMS Level 3 solution is based on train position and train integrity confirmation, both transmitted by the on-board train system (called EVC<fnref n="5" />) to the trackside system (called RBC<fnref n="6" />). Given this information, the traffic agent, via RBC, assigns a movement authority to a train allowing it to move to a given point. In the RBC, track-circuits exist in a logical form by means of trackside train detection sections (called TTD) which are in turn divided into virtual subsections (called VSS). Figure 5.10, taken from the ERTMS 3 reference document (ERA, 2016), illustrates a track circuit divided into two TTDs and four VSSs, and where a train is located on

<footnote n="3">³ ERTMS: European Rail Traffic Management System.</footnote>

<footnote>ETCS: European Train Control System.</footnote>

<footnote n="4">⁴ https://www.southampton.ac.uk/abz2018/information/case-study.page</footnote>

<footnote n="5">⁵ European Vital Computer.</footnote>

<footnote n="6">⁶ Radio Block Center.</footnote>
VSS23. This simplified view of section conventions, used by railway experts, applies specific domain representations to represent a situation where a train went through TTD2 and reached its ending VSS.

<figure><img src="image_70.png" /><figcaption>Figure 5.10: Section conventions ERA (2016)</figcaption></figure>

## 5.2.2 Coloured Petri-nets

Several high-level variants of Petri-nets, like coloured petri-nets or predicate-transition nets, were applied in safety-critical systems and were assisted by formal verification techniques such as animation, model-checking or proofs. Moreover, some experiences like that of the Oslo subway, reported in (Hagalisletto et al., 2007), show that in addition to their formal semantics, high-level Petri-nets favoured communication with domain experts, because chief engineers from railroad infrastructure and traffic department who are not specialists in Petri-nets nor in formal methods, were not only able to understand the models, but also to suggest improvements.

We use coloured petri-nets (CP-Nets), which abstract away structural constraints and focus on safety-critical behaviours. CP-Nets combine the strengths of classical Petri-nets with the strengths of high-level programming languages (Gehlot and Nigro, 2010), to allow handling data types with pre-defined functions. For a formal description of CP-nets, one can refer to (Jensen, 1981); nonetheless, the main concepts used here are:

*   **Data types:** can be simple types (i.e. Integer, Boolean, ...) or complex types (i.e. arrays, sequences, ...). In this work, we mainly use integer enumerations.

*   **Places:** represent abstractions on data values (called tokens or colours). The place type is called the colour set and it is defined by composing data-types.

*   **Transitions:** they are linked to input and output places. When fired, a transition consumes tokens from its input places such that they match the transition signature. Then, the transition introduces tokens into its output places.

*   **Predefined functions:** describe some computations done by the transitions when they are fired. In this paper, we use three basic functions: calculation of the next ($n^{++}$) and the previous value ($n^{--}$) given a token $n$ when $n$ is of type integer, and the negation value ($\neg n$) when $n$ is of type boolean.
5.2.2.1 Level 1: Simple train movements

Our first CP-net (figure 5.11) defines simple train movements without train integrity nor move-
ment authorities. This abstract level is mainly intended to guarantee the absence of accidents.

<figure><img src="image_71.png" /><figcaption>Figure 5.11: Simple movement described in a CP-net</figcaption></figure>

This model describes train movements using transitions *moveEven* and *moveOdd* which
move the train forward or backwardand; and *changeSens* which switches the train moving di-
rection. Place *Position* contains pairs (*t*, *v*) which record the current VSS *v* occupied by a train
*t*. Place *Free* gathers the sections which are not occupied by any train and place *Sens* registers
for every train its current direction. For our first CP-net model, we would like to prove five
safety properties:

1. Absence of accidents meaning that at most one train occupies a Vss,

2. Every train is located in one and only one Vss,

3. Absence of overlapping between Vss states free and occupied,

4. Vss states cannot be undefined, they are either free or occupied,

5. The train moving direction is never lost

Transition *moveEven* is fired given a train *t* located on section *v*, whose direction is set to *true*, and such that its next section *v++* is free (e.g. (*t*, *v*) ∈ *Position* ∧ (*v++*) ∈ *Free*). When fired, this transition instantly moves train *t* from section *v* to section *v++*. It consumes tokens (*t*, *v*) and (*v++*) respectively from places *Position* and *Free*, and then respectively introduces into these places tokens (*t*, *v++*) and (*v*), meaning that *v++* becomes the new position of train *t*, and section *v* is released. Transition *moveOdd* applies the same principles to trains in direction *false* but selects the previous section *v--* if this section is free. Transition *moveEven* is
fired provided that the train direction is set to *true* while transition *moveOdd* is fired when its direction is *false*.

### 5.2.2.2 Extraction of B specifications

In order to prove the safety properties of our first level CP-net model we translate it into B specifications as follows:

**MACHINE**

CPNData

**CONSTANTS**

maxTrain, maxVss, CPNTrain, CPNVss

**PROPERTIES**

maxTrain ∈ NAT ∧ maxVss ∈ NAT

∧ CPNTrain = 1 .. maxTrain

∧ CPNVss = 1 .. maxVss

REFINEMENT CPNLevel1

REFINES CPNData

**VARIABLES**

Free, Position, Sens

**INVARIANT**

Free ⊆ CPNVss

∧ Position ⊆ CPNTrain × CPNVss

∧ Sens ⊆ CPNTrain × BOOL

First an abstract machine (named *CPNData*) is generated in order to gather the colour sets together with the transition signatures as defined in the CP-net model. Colour sets *Train* and *Vss*, which are integer enumerations, are translated into bounded natural constants *CPNTrain* and *CPNVss*. Places *Free*, *Position* and *Sens* become variables in refinement *CPNLevel1* because their values evolve during the execution of the CP-net. In this refinement, by default the variable typing applies general functions such as sets' cartesian product and inclusion (e.g. *Position* ⊆ *CPNTrain* × *CPNVss*).

Every transition leads to a basic operation defined in machine *CPNData* with a typing pre-condition and a *skip* substitution, like the example below of operation *moveEven*:

/* Operation moveEven in machine CPNData */
moveEven(tt, vv) =
    PRE tt ∈ CPNTrain ∧ vv ∈ CPNVss THEN
    skip
    END

The *skip* substitution of the basic operations is then refined in *CPNLevel1* by introducing the enabledness guards and the expected actions of the transition. In the following we give the refinement of operation *moveEven* in *CPNLevel1*:

/* Refinement of the skip substitution in CPNLevel1 */
moveEven(tt, vv) =
    SELECT
        (tt ↦ vv) ∈ Position ∧ (vv + 1) ∈ Free ∧ (tt ↦ TRUE) ∈ Sens
    THEN
        Free := (Free - {(vv + 1)}) ∪ {(vv)} ||
        Position := (Position - {(tt ↦ vv)}) ∪ {(tt ↦ vv + 1)}
    END;
Transitions *moveOdd* and *changeSens* are translated by applying the same principles. Regarding the five safety properties, they are manually introduced in machine *CPNLevel1* using the following invariants:

$$
\begin{align*}
Position &\in CPNTrain \rightarrow CPNVss /* Properties (1) and (2) */ \\
Free &\cap ran (Position) = \emptyset /* Property (3) */ \\
Free &\cup ran (Position) = CPNVss /* Property (4) */ \\
Sens &\in CPNTrain \rightarrow BOOL /* Property (5) */
\end{align*}
$$

These invariants restrict the state space defined by the typing predicates presented above. For example, the typing predicate of relation *Position* defines all combinations of CPNTrain and CPNVss couples, while the invariant restricts these combinations to those where a CPNTrain is linked to one and only one CPNVss while a CPNVss is linked to at the most one CPNTrain. In our methodology, we consider that if the CP-net model is correct, proofs should be done without any enhancement of the corresponding B specifications. Otherwise, we decide whether the CP-net model is wrong or not, given the AtelierB feedbacks. In all cases we do not modify the generated B operations; we either call the interactive prover when the proof fails due to a limitation in the automatic prover, or we correct the CP-net model and translate it again into B. The initial marking substitutions are introduced without invariant violation:

INITIALISATION

$$
\begin{align*}
Position &\in CPNTrain \rightarrow CPNVss ; \\
Free &:= CPNVss - \mathbf{ran}(Position) ; \\
Sens &\in CPNTrain \rightarrow BOOL
\end{align*}
$$

Based on machines *CPNData* and *CPNLevel1*, and these additional invariants, the AtelierB generated 17 proof obligations and automatically proved 11 amongst them. The 6 other POs were proved using the interactive prover.

5.2.3 A Railway DSL for ERTMS/ETCS

5.2.3.1 The meta-model

In order to provide a tool for domain experts allowing them to draw models like that of figure 5.10, we apply model-driven engineering tools for DSML creation (EMF, Ecore-Tools and Sir-
ius). In MDE, the creation of a DSML starts by the definition of its meta-model and then for
every class in the meta-model a graphical representation is created. Figure 5.12 gives the meta-
model that we use in this work and figure 5.13 gives a screenshot of the resulting DSML-tool
in which a model is designed using the proposed graphical representations.

In our meta-model, a railway system is composed of trains (class *Train*), track sections
called TTD in ERTMS/ETCS 3 (class *Trackside*) and which are divided into portions called VSS
(class *VirtualBlock*). The bottom of figure 5.13 draws an overall railway topology by means of
TTD links. Every portion of a given TTD may be linked to two next and previous portions
<figure><img src="image_72.png" /><figcaption>Figure 5.12: A railway meta-model</figcaption></figure>

<figure><img src="image_73.png" /><figcaption>Figure 5.13: A railway model</figcaption></figure>

at the most. In practice, there are four kinds of portions: track extremity (e.g. *VSS11* and *VSS62*), middle track (e.g. *VSS12*), switch (e.g. *VSS21* and *VSS51*) and diamonds. Association *pSetted/nSetted* provides the currently selected previous/next portion among those to which a portion is linked. This is useful especially for switches and diamonds. For example, the next portions of *VSS21* are *VSS31* and *VSS41*, but the position of the switch sets the currently selected next portion of *VSS21* to *VSS31* and hence the selected previous portion of *VSS31* is *VSS21* but for portion *VSS41* there is no previous selected portion. Portion *VSS41* remains then a track limit until the switch position is changed. Note that relation *pSetted/nSetted* is independent from train direction and a track limit is a portion without a selected next or previous portion.
Class *TrackView* represents linear views that follow the current next/previous selections and where every view starts and ends with track limits. For example, the topology presented in the bottom of figure 5.13, leads to the two views on the top of the figure. The first view covers sections *TTD1*, *TTD2* and *TTD3* and the second view covers the three other sections: *TTD4*, *TTD5* and *TTD6*. If the switches position changes, these views are changed consequently. For example, if the selected next portion of *VSS21* is set to *VSS41*, then the resulting topology would lead to two different views: one composed of *TTD1/TTD2/TTD4/TTD5/TTD6*, and an other view dedicated to *TTD3* only.

Trains have a direction (*even* or *odd*) and their representation depends on the set of portions that their head and rear occupy. In the example of figure 5.13 we consider two trains: T1 whose front and rear occupy the same portion (*i.e.* *VSS21*), and T2 that stretches from portion *VSS42* to *VSS51*. A TTD is occupied when at least one of its portions are occupied. This is represented by the yellow color in the track views and by the red color in the topology representation. The green color is used to represent free TTD and VSS in the track view.

### 5.2.3.2 Formal model

We apply Meeduse to provide domain experts with a formally defined DSL-tool. We give below the translation of classes *Train* and *VirtualBlock* and one basic operation *Train_AddFront* which adds a virtual block to the set of virtual blocks occupied by the head of a train. Several other basic operations are generated by the tool like: *Train_RemoveFront*, *Train_AddRear*, *Train_RemoveRear*, etc.

**MACHINE** *Functional*

**SETS**

*VIRTUALBLOCK; TRACKSIDE*

*Direction* = {*even*,*odd*};

**VARIABLES**

*Train*, *VirtualBlock*, *Train_direction*, *frontOfTrain*, *rearOfTrain*

**INVARIANT**

*Train* ⊆ *TRAIN*

*VirtualBlock* ∈ *VIRTUALBLOCK*

*frontOfTrain* ∈ *Train* ↔ *VirtualBlock*

*rearOfTrain* ∈ *Train* ↔ *VirtualBlock*

*Train_direction* ∈ *Train* → *Direction*

*Train_AddFront(aTrain,aFront) =*

**PRE**

*aTrain* ∈ *Train* ∧

*aFront* ∈ *VirtualBlock* ∧

(*aTrain* ↦→ *aFront*) ∉ *frontOfTrain*

**THEN**

*frontOfTrain* :=

*frontOfTrain* ∪ {*(*aTrain* ↦→ *aFront*)*}

**END;**

Machine Functional generated by Meeduse is about 500 lines with 38 basic operations from which the AtelierB produced 80 proof obligations that were proved automatically. Given a model (like that of figure 5.13) Meeduse injects it as valuations in the B specification and calls ProB in order to compute the list of operations that may be animated from these valuations. For
example, the following initialization is extracted by Meeduse from our graphical model. The
resulting initial state is hence equivalent to the domain model.

INITIALISATION

Train := {T1, T2} ||
VirtualBlock := {VSS11, VSS12, ..., VSS62} ||
frontOfTrain := {(T1 ↦ VSS21), (T2 ↦ VSS42)} ||
rearOfTrain := {(T1 ↦ VSS21), (T2 ↦ VSS51)} ||
Train_direction := {(T1 ↦ even), (T2 ↦ odd)}

Starting from this initial state, when the user asks Meeduse to animate a B operation, the tool
calls ProB and gets the new variable valuations and then it translates back these valuations to
the graphical model. This technique results in an automatic visual animation of domain models.
For example, the animation of operation *Train_AddFront(T1, VSS31)* introduces couple (*T1* ↦ *VSS31*) into relation *frontOfTrain* and then Meeduse modifies the domain model as presented in
figure 5.14 where the head of T1 occupies two virtual blocks *VSS21* and *VSS31*. Since *VSS31*
is one of the portions of *TTD3*, then the visual representation of *TTD3* automatically changes
from green to yellow.

<figure><img src="image_74.png" /><figcaption>Figure 5.14: View 1 after animation of *Train_AddFront(T1, VSS31)*</figcaption></figure>

**5.2.4 Putting it all together**

Section 5.2.2 focused on train behaviours with an abstract Petri-net specification that guarantees the absence of accidents, and section 5.2.3 focused on domain modeling of structural aspects of a railway DSL. In this section, we combine both concerns in order to provide a railway DSL with a proved safe train behaviour. The B specifications extracted from the meta-model of Figure 5.12 represent formal static semantics of our DSL, and those extracted from a CP-net model introduce its operational semantics. In order to merge static and operational semantics we create machine LinkageV1; it refines CPNLevel1 and includes machine Functional:
**REFINEMENT** *LinkageV1*

**REFINES** *CPNLevel1*

**INCLUDES** *Functional*

**VARIABLES**

trainMapping, vssMapping, view

**INVARIANT**

trainMapping ∈ Train ↦→ CPNTrain

∧ vssMapping ∈ VirtualBlock ↦→ CPNVss

∧ view ∈ TrackView

The refinement guarantees the preservation of the safety invariants of *CPNLevel1* and the inclusion allows us to redefine the CP-net transitions and data using the functional variables of the DSL. In this machine the linkage of the DSL and the CP-net model is done via functions *trainMapping* and *vssMapping*. They respectively map variables *Train* and *VirtualBlock* issued from the meta-model to sets *CPNTrain* and *CPNVss* issued from the CP-net. In our approach every view in the DSL is controlled by a CP-net since the CP-net defines the VSS set by a sequence of integers. Then, the mapping functions are applied to a given *view* (*view* ∈ *TrackView*). For example, the *vssMapping* relation is computed in the initialisation of *LinkageV1* as:

```
LET mapVss BE mapVss = ran(({view} ⊳ blocks⁻¹; theVSSs⁻¹)) IN
ANY map WHERE
  map ∈ mapVss ↦→ CPNVss ∧
  ∀ vss . (vss ∈ mapVss ∧ nSetted[{vss}] ≠ ∅
           ⇒ nSetted(vss) ∈ dom(map) ∧ map(nSetted(vss)) = map(vss) + 1)
THEN
  vssMapping := map
END
END
```

Note that *blocks* and *theVSSs* represent respectively association blocks between classes *TrackView* and *Trackside*, and association *vss* between classes *Trackside* and *VirtualBlock*. Local variable *mapVss* defined by: *ran(({view} ⊳ blocks⁻¹; theVSSs⁻¹))* extracts the set of VSS for a given *view* and the mapping is a total injection (→) that maps every VSS in this view to a unique value from set *CPNVss*. This mapping is done under the condition that if a VSS is not a track extremity (*nSetted[{vss}] ≠ ∅*) then its next selected VSS is mapped (*nSetted(vss) ∈ dom(map)*)) and the associated CP-net value is equal to the VSS value plus one. We similarly compute the *trainMapping* relation but under the condition that only trains whose head and rear occupy the same VSS are mapped. In this sense, from the example of figure 5.13 only the first view can be mapped and then controlled by our first level CP-net model.

Given the mapping relations, the safety invariants of *CPNLevel1* are rewritten by means of linkage invariants ensuring the relationship between the various B specifications. For example, invariant *Free ∩ ran一大于(Position)* = ∅ used for *Property* (3) becomes as follows:
$$ (\mathit{frontOfTrain} \cup \mathit{rearOfTrain})^{-1}[\mathit{vssMapping}^{-1}[\mathit{Free}]] = \emptyset $$

This means that for every free VSS in the CP-net model, the corresponding virtual block in the DSML does not contain any train head or rear. Having the linkage invariants, operation `moveEven`($tt$, $vv$) in the linkage machine is applied to a train mapped to $tt$, whose head and rear occupy a VSS mapped to $vv$, and whose direction is `even` and such that the next VSS which is mapped to $vv + 1$ is free. Actions of `moveEven` call basic functional operations issued from machine `Functional`. They simply remove the head and the rear of the train from $vv$ and put them on $vv + 1$. In the following we give the refinement of operation `moveEven` in LinkageV1:

```
moveEven.tt, vv) =
    LET train, vss, nextVss BE
    train = trainMapping⁻¹.tt
    ∧ vss = vssMapping⁻¹(vv)
    ∧ nextVss = vssMapping⁻¹(vv + 1)
IN
    SELECT
        (train ↦ vss) ∈ frontOfTrain ∩ rearOfTrain
        ∧ nextVss ∉ ran(frontOfTrain ∪ rearOfTrain)
        ∧ Train_direction(train) = even
    THEN
        Train_RemoveFront(train, vss); Train_AddFront(train, nextVss);
        Train_RemoveRear(train, vss); Train_AddRear(train, nextVss)
    END
END;
```

41 POs were generated and proved by the AtelierB for machine LinkageV1, which mean that the safety properties (those of machine CPNLevel1) as well as the structural properties (those of machine Functional) are preserved. Regarding the execution of the DSL, it is done by railway experts using the animation facility of Meeduse. By animating operations from the linkage machine, Meeduse automatically updates the corresponding graphical model leading to its execution.

### 5.2.5 Refinements

We also apply the refinement principle of the B method to incrementally define formal operational semantics by means of refined CP-net models. In this section, we only focus on the first refinement level; we refer the reader to (Idani, A. et al., 2019a,b) for further details. The general idea is that at every refinement step we introduce additional conceptual elements with associated safety properties and we prove the preservation of these properties as well as those of the previous level:
* Level 2 (authorized train movements): The assumption made in the first CP-net level, considering that a train moves to the next free virtual section and immediately leaves its current section, is quite simplistic but sufficient in order to model an abstract accident-free behaviour. In this second level we introduce a movement authority mechanism, in order to construct routes to which trains are allowed to move. The additional safety invariants of this second CP-net level are: (6.) a VSS cannot be waiting and at the same time assigned to a movement authority; and (7.) a movement authority cannot be shared by several trains. Given CP-net of Level 2 and the corresponding safety properties, as well as the refinement invariant, the AtelierB prover generated 32 POs, such that 25 were proved automatically and 7 interactively, which means that CP-net Level 2 guarantees its own properties and also those of CP-net Level 1.

* Level 3 (movements with integrity confirmation): In the third refinement level we consider a more realistic train representation than that developed in the two previous levels where a train occupies only one VSS. In this refinement, a train is seen as a logical entity defined by the set of VSS that it occupies: its head (place *Position*), a set of VSS not yet released behind its head (place *Wagon*) and the safe rear end (place *Tail*) which is in our case one additional VSS defining the minimal distance between two trains. Thus, a train occupies at least two virtual sections: one for its head and one behind it. When a train moves, its head is advanced from its current VSS *v* to the next VSS *v*<sup>++</sup>, and then *v* is not freed but a virtual wagon is created over it. Indeed, in ERTMS/ETCS 3, the train must confirm its integrity (*i.e.* it did not lose wagons) before releasing its safe rear end which advances its tail by one VSS and removes the corresponding virtual wagon. Given the B specifications issued from this third level and the associated safety invariants, the AtelierB produced 62 POs and automatically proved 41 among them. The 21 other POs were proved manually.

## 5.3 Application 3: Model transformation

This section summarizes the application of Meeduse to the 2019 edition of the Transformation Tool Contest (Garcia-Dominguez and Hinkel, 2019) and gives the lessons learned from this study<sup>7</sup>. Among other challenges, the contest emphasizes on correctness which motivated us to apply Meeduse. This study allowed us to try how far we can push the abilities of a formal method to be integrated within model-driven engineering. The results showed that Meeduse can be adapted to model transformation which brings to this field formal automated reasoning tools like AtelierB for theorem proving and ProB for model-checking. Meeduse, combined with ProB, provides three strategies: random animation, interactive animation and model-checking. The first strategy runs randomly the transformation rules until it consumes all the elements

<footnote n="7"><sup>7</sup> The proposed solution and demonstration videos can be found at: https://github.com/meeduse/Meeduse_TTC_2019.</footnote>
of the input model and produces the output model. The second strategy applies a step-by-step debugging of the transformation rules, and the third strategy is useful for analysing the reachability of some defined states which allows one to verify whether unwanted situations may happen or not.

Our main objective for the TTC'2019 challenge is to reuse some selected components of Meeduse in order to execute a formal specification of transformation rules given realistic input models. As Meeduse was not initially designed to define model transformations, but to define executable DSLs, we need to rethink the model transformation problem in terms of operational semantics of an abstract machine. However, presenting the full B model of the TTC'2019 case study requires introducing many concepts and properties, which would be inconvenient for readers and take much space in this document. Hence, we decided to introduce in this section our approach and its underlying formal concepts step by step using a simplistic model transformation example inspired by some basic MDE material available on-line. Application of Meeduse to the TTC'2019 case study is described in (Idani, A. et al., 2019c).

Figure 5.15 shows simple input and output meta-models for the example transformation. The input is a model defining persons (of any gender) which may be married (represented by the person1/person2 relation) and the output is a model focused only on married wives and husbands.

<figure><img src="image_75.png" /><figcaption>Figure 5.15: Input/Output meta-models</figcaption></figure>

### 5.3.1 Step 1: merging meta-models

The input of our tool is the meta-model of a DSL. In order to apply it for model-to-model transformation, our idea is first to merge both input and output meta-models into a single one that is automatically translated by Meeduse into B, and then specify the transformation rules as operations of the corresponding B machine. Intuitively, the state of the transformation execution includes the input model, the partially generated output model and any additional information required by transformation rules (for instance, traceability links created by other rules).
To illustrate this idea, figure 5.16 shows the merging meta-model for our simple transformation. We suggest that the semantics of the transformation follows a consumption/production technique: instances of output classes are created while consuming instances of input classes. In order to keep track of the modeling elements that have been processed by the transformation, we introduce an abstract meta-class *Element* to gather modeling elements consumed by the transformation. This class introduces an attribute *name* to identify processed elements and a boolean attribute *done* to identify input elements that have been already consumed.

<figure><img src="image_76.png" /><figcaption>Figure 5.16: Merging meta-models</figcaption></figure>

### 5.3.2 Step 2: generation of the “model construction” specification

From the merging meta-model, Meeduse automatically generates a B specifications with basic modeling operations as well as structural invariants. This technique allows one to write the transformation rules in the B language. Figure 5.17 presents the structural part of the resulting B machine. The behavioral part of the generated B machine provides all basic operations for model manipulation: getters, setters, constructors and destructors; for this reason we refer to this machine as the “model construction” machine. Figure 5.18 shows the specification of two generated operations. Operation *Husband_NEW* is a constructor that creates an instance of class *Husband*. This operation takes an element from the possible objects defined by abstract set *ELEMENT* and adds it to the set of existing instances of class *Husband*. Operation *Husband_SetWife* is a setter that straightforwardly assigns a value to the bi-directional reference husband/wife. Notice that this step is analogous to what happens in MDE tools that generate code from meta-models. For instance, from a given meta-model definition EMF can generate Java modeling code (getters, setters, etc), that can be used to program model transformation in Java. In the same way, Meeduse generates a B machine that can in turn be used to specify model transformations in B.

The B specification issued from our simple meta-model is about 335 lines of code with 34 basic operations which are proved correct (with respect to the structural invariant) by construc-
tion. Proofs were carried out using AtelierB, for this simple specification it generated 120 proof obligations, which were all automatically proved by the theorem prover. This means that the use of these modeling operations guarantees the preservation of the structural properties (invariant) of the meta-model.

<figure><img src="image_77.png" /><figcaption>Figure 5.17: Structural part of the modeling specification</figcaption></figure>

<figure><img src="image_78.png" /><figcaption>Figure 5.18: Generated constructor and setter for class Husband</figcaption></figure>

### 5.3.3 Step 3: writing the transformation rules

A model transformation is manually written in a new B machine as a set of B operations that can reuse the modeling operations defined in the *simpleModel* machine (figures 5.17 and 5.18). Each transformation rule is defined as a B operation composed of two parts: the guard and the
action. The guard gives the conditions under which the rule can be triggered, and the action specifies a sequence of calls to modeling operations (from machine *simpleModel*) whose effect is to create the output model. Figure 5.19 gives the two transformation rules that we defined for our simple example.

<figure><img src="image_79.png" /><figcaption>Figure 5.19: Transformation rules written in B</figcaption></figure>

Operation *Input2Output* creates an *OutputModel* for each *InputModel*. It takes any existing instance of class *InputModel* (*input* ∈ *InputModel*) which has not been yet transformed (condition *input* ∉ *OutputModel*) and then its action creates the new instance of *OutputModel* by calling basic operation *OutputModel_NEW*(*input*).

Operation *Person2HusbandWife* takes two instances of class *Person* representing a married couple (defined by parameters *p1* and *p2*) and translates them into instances of classes *Husband* and *Wife* in the resulting output model. The enabling conditions for this transformation rule are:

* there exists an output model (*output* ∈ *OutputModel*)
* the input instances satisfy a pattern, *p1* is a male (*Person gender*(*p1*) = male), *p2* is a female (*Person gender*(*p2*) = female) and they are married ((*p1* ↦ *p2*) ∈ *person*_1_2 ∨ (*p2* ↦ *p1*) ∈ *person*_1_2)

* The input instances have not been already processed (*Element_done*[{*p1*, *p2*}] = {FALSE} and (*husbands* ∪ *wifes*)[{*p1*, *p2*}] = ∅)

### 5.3.4 Step 4: animation and debugging

In Meeduse the user can load an EMF input model and injects it in the B specifications as variable valuations. After loading the model, Meeduse asks ProB to animate the initialization and then gets the initial state of the machine. Given this state, ProB computes the list of operations whose guards are satisfied and that can then be animated from the initial state. Figure 5.20 is a screen-shot of Meeduse after loading an example input model containing six persons (View ①). The state of the machine after the initialization is displayed in View ③ of figure 5.20 (called *Output State View*). The list of operations that can be triggered in the current state is shown in view ② of figure 5.20 (*the animation view*). In our case, the only operation that can be animated at the initial state is *Input2Output*, with parameter *MyModel*.

<figure><img src="image_80.png" /><figcaption>Figure 5.20: Meeduse screenshot: initial values</figcaption></figure>

This interactive animation technique applies the transformation rules step-by-step to the input EMF model which is useful for debugging. The animation stops when the B specification
reaches a deadlock: a state from which there is no other possible operation to animate. It also stops when an invariant violation is detected. Figure 5.21 gives the result of the animation at the final state. In the output model, two husbands (Bob and Chuck) and two wives (Alice and Laurence) were created, with the corresponding marriage relation. The valuations of the B variables showed in the output state view are equivalent to the EMF model since Meeduse maintains this equivalence at every animation step.

<figure><img src="image_81.png" /><figcaption>Figure 5.21: Meeduse screenshot: after animation of all rules</figcaption></figure>

When the domain expert agrees with the behaviors showed by animation, transformation rules can be played without any human interaction. After loading a model the user can enable the automatic runner from the *animation view* by clicking on the corresponding icon. This runner executes a random animation: at every step it chooses randomly an operation from those provided by ProB and automatically animates it until reaching the ending state where a deadlock or an invariant violation is detected.

### 5.3.5 Step 5: Proving the transformation

Application of a formal method to model transformation brings several benefits to this field. Indeed, since Meeduse produces a formal specification and automatically manages the traceability between EMF models and the B machine valuations, we can go a step further towards the usage of automatic reasoning tools like model-checkers.
The invariants discussed in step 2 define the properties of our meta-model, not those of the transformation. One way to analyze the transformation and have some confidence about its correctness is to define unwanted states and ask ProB to find them by model-checking. In the following we present some example goals that we defined for our simple transformation:

$$GOAL1 == \exists pp . (pp \in \mathit{Husband} \land \mathit{Person\_gender}(pp) = \mathit{female});$$

$$GOAL2 == \exists pp . (pp \in \mathit{Wife} \land \mathit{Person\_gender}(pp) = \mathit{male});$$

$$GOAL3 == \exists (p1, p2). ((p1 \mapsto p2) \in \mathit{husband\_wife} \land \{p1, p2\} \not\subseteq \mathit{dom}(\mathit{person\_1\_2}) \cup \mathit{ran}(\mathit{person\_1\_2}));$$

$$GOAL4 == \mathit{Husband} \cap \mathit{Wife} \neq \emptyset$$

The three first goals are linkage properties between the input and the output meta-model. Goal1 and Goal2 for example state that an instance of class Husband is created but from a Person whose gender is female and vice-versa. Goal3 means that a husband and his wife in the output model are created but without any existing marriage link between the input persons from which they originate. Goal4 represents a forbidden property of the output meta-model and means that someone is husband and wife at same time.

Given the B specification extracted from the initial model (that of figure 5.20), we can ask ProB, from outside Meeduse, to find by model-checking states where one of these goals are satisfied. The answer of ProB is that all state space is explored without finding any of the four goals. Since the state space is entirely bounded thanks to valuations, ProB is able to compute all reachable states. This model-checking proof gives a good confidence about the correctness of the transformation. It can be applied to bigger examples in the limits of space memory and the model-checker capacities.

### 5.3.6 Discussion

We can remark that the chosen style for specifying the transformation rules in B reminds transformation languages available in the MDE community. The specification of the rule guard (clause **ANY**) is similar to some declarative transformation languages (it looks like the *where* condition and *checkonly* patterns in QVT relational for example). Nonetheless, the action part has a more imperative style. As B is not a specialized language for model transformation, some aspects have to be taken care explicitly, for instance we have to check that a rule is not applied several times for the same input. An important aspect that is worth mentioning is that we do not specify explicitly the execution order of the rules. The semantics of a B machine is that, at any given point during the execution, the system considers all enabled operations and makes a non-deterministic choice. The choice of the parameters in the **ANY** clause is also non-deterministic, meaning that at any execution state, the system will select any objects that satisfy the condition and use them as arguments for the operation. However, in this example we have indirectly prescribed an order of execution, because in the guard of the `Person2HusbandWife` rule we check for the existence of an object created by the `Input2Output` rule. This strategy is
also similar to some declarative transformation languages that use traceability information to infer an execution order. The dynamics of a B machine execution will be further explored in the following sections.

A final point concerns the correctness of the transformation rules. As mentioned in the previous section, the individual model construction operations (constructors, setters, ...) were proved correct, then the result of executing a sequence of operations in the action part of a rule will obviously preserve the model structural properties. However, we also need to prove that the order of the sequence of calls is correct, meaning that the preconditions of every operation in the sequence are satisfied. Let's consider for example operation `Husband_SetWife` which can be applied only on existing instances of classes Husband and Wife: `aHusband ∈ Husband ∧ aWife ∈ Wife`. As actions `Husband_NEW` and `Wife_NEW` produce these instances, then the proof of correctness associated to the call of `Husband_SetWife` in rule `Person2HusbandWife` succeeds. For our example rules, the AtelierB generated 13 additional proof obligations, which were automatically proved. This means that we don't need to test the validity of the input models or verify the output model using the EMF validator.

### 5.3.7 The TTC'2019 Case Study

The call for solutions of TTC'2019 was about the transformation of Truth Tables (TT) into Binary Decision Diagrams (BDD). Among the seven participants, Meeduse was the only attempt that addressed V&V; the other solutions addressed flexibility, performance and optimality. Figure 5.22 shows the various views of Meeduse that represent our solution.

<figure><img src="image_82.png" /><figcaption>Figure 5.22: Application of Meeduse to DSL transformation</figcaption></figure>
The B machine extracted from the meta-model is about 1162 lines of code from which the AtelierB generated, and automatically proved 260 proof obligations. This proof gives the guarantee that the model's properties are preserved during the DSL transformation. The operational semantics were introduced using an additional B machine whose length is about 150 lines of code. This is more concise (but may be more difficult to understand) than a reference ATL solution which is about 340 lines of ATL code. The proposed operational semantics of this case study were defined through five B operations and several additional invariants. For this case study the correctness of the operational semantics was ensured by model-checking, rather than by theorem proving because on the one hand it is less time consuming, and on the other hand, it deals with bounded state spaces that can be exhaustively checked by the ProB model-checker.

From a methodological point of view we were able to define how formal executable DSLs can be applied to define model transformations. Merging meta-models required the implementation of an additional driver, but we believe that Meeduse can be adapted to deal with two or several heterogeneous meta-models. This issue is now considered as a possible evolution of the tool. In general, we are satisfied by the application of Meeduse to the model-to-model transformation problem because as far as we know none of the existing works combine theorem proving and model-checking in a publicly available tool and which is well integrated within EMF-based platforms.

Regarding performance, it mainly depends on the performance of ProB. Execution times spent by the tool to generate the output models are given in table 5.1. The number of model elements grow exponentially. For 14 input ports and 2 output ports, Meeduse reached an out of memory. For bigger examples, it should be useful to try the experiments on a machine with higher performances than that on which we have done these measures.

<table><caption>Table 5.1: Some performance measures</caption><thead><tr><th>Input Model</th><th>rows</th><th>input ports</th><th>output ports</th><th>Cells</th><th>Exec. Time</th></tr></thead><tbody><tr><td>GeneratedI402Seed42</td><td>16</td><td>4</td><td>2</td><td>96</td><td>3s</td></tr><tr><td>GeneratedI502Seed5</td><td>32</td><td>5</td><td>2</td><td>224</td><td>5s</td></tr><tr><td>GeneratedI802Seed68</td><td>256</td><td>8</td><td>2</td><td>2560</td><td>1mn3s</td></tr><tr><td>GeneratedI804Seed68</td><td>256</td><td>8</td><td>4</td><td>3072</td><td>2mn1s</td></tr><tr><td>GeneratedI1002Seed68</td><td>1024</td><td>10</td><td>2</td><td>20480</td><td>18mn8s</td></tr><tr><td>GeneratedI1202Seed7634</td><td>4096</td><td>12</td><td>2</td><td>57344</td><td>6h40mn</td></tr></tbody></table>

For readability, we believe that the verbose notation of the B method is accessible because it recalls some programmatic styles. It is often said to be less difficult than other formal notations. Our transformation file is about 150 lines which remains reasonable. However, the B specification that we provide is expected to be readable for a formal methods expert, may be more readable than an ATL or a QVT transformation. But this intuition needs some empirical studies in order to be confirmed.
Conclusion and perspectives

« Maintenant l'abstrait s'était matérialisé,
l'être enfin compris avait aussitôt perdu de son pouvoir de rester invisible, [...]
tout ce qui avait paru, jusque-là, incohérent à mon esprit,
devenait intelligible, se montrait évident, comme une phrase, n'offrant aucun
sens tant qu'elle reste décomposée en lettres disposées au hasard, exprime,
si les caractères se trouvent replacés dans l'ordre qu'il faut,
une pensée que l'on ne pourra plus oublier. »

Marcel Proust

This document presented my research works during the last fourteen years. I addressed two topics: Model-Driven Security and Domain-Specific Languages. The guiding principle of my contributions is the combination of two well-known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE); to which I refer using acronym FMDE. During this period I had the opportunity to (co-)supervise many students for their PhD, M2 or final study engineer projects. I also collaborated with many colleagues and have been member of various research projects. My works led to the development of two tools: B4MSecure (Idani, A. and Ledru, 2015) and Meeduse (Idani, A., 2020b). These tools reached a good level of maturity and are no longer simple prototypes. They have been applied on several realistic case studies and showed by practice their strengths. B4MSecure is currently used in the “Information Security” lecture of the M2 MoSIG at Grenoble. It is exploited in a lab that introduces students to the design of Access Control policies, and also to testing via animation and to the insider threat problem. Regarding Meeduse, it is today the only existing language workbench (LWB) that favours both formal reasoning – via theorem proving – and the execution of the DSL – via animation and model-checking.

Several research directions that are mentioned in the introduction have not been discussed in
details in this document, for space reasons and also because some of them are not yet published.
I'm still actively working on these topics, with several perspectives.
Formal MDS

Nowadays, information technology architectures support interconnection between systems and favour a greater interoperability and a centralized access to data. However, despite these advantages, they expose information systems to a multitude of security risks. Indeed, organisations manage sensitive information and security vulnerabilities can lead to financial loss, dilapidation of the brand image, shutdown of production systems or leakage of confidential information. Hence, information flows must be controlled to adequately ensure information security and to enforce the ACIT properties (Availability, Confidentiality, Integrity, Traceability) of Secure Information Systems. Separation of concerns and abstraction/refinement techniques have been proposed to master the complexity of these systems. First, separation of concerns distinguishes functional aspects of the IS (data model and the associated business logic) from security concerns. Second, it appears that security can be considered at several abstraction levels: from high level ACIT properties, close to the concerns of users, to security techniques and mechanisms of the hardware and software platform.

Significant efforts have been dedicated to the careful definition of security policies and their deployment on a given technology. The Model-Driven Security (MDS) (Basin et al., 2011) approach addresses this challenge by trying to define the relationship between high-level security modeling, expressed in terms of permission rules, and the implementation level. Platform Independent Models (PIM) promote a real separation of concerns between the functional requirements and the security policy. MDS makes the link, using transformation tools, between the PIM and the Platform Specific Model (PSM), where the PSM is a more concrete model that can be mapped to a given technology platform (programming language, operating system, ...). However, validation of the various models remains error prone without the assistance of formal analysis tools and consequently the encoded security policy is poorly understood and difficult to maintain, correct or adapt. Current validation activities are limited to structural aspects of the models, where functional and security models are validated separately. However, evolutions of the functional state of an IS may change the context of several permissions, which may lead to security threats. The validation activities thus require tools that can take into account dynamic aspects of **both functional and security aspects**. These tools can come in the form of model checkers and animation tools, dedicated to formal specification techniques.

My works in this field propose a way to guarantee a **security-by-design** approach in which the MDS benefits from an automated formal support based on the formal B method. Indeed, formal B specifications take into account behavioural aspects of the secure IS and deal with interactions between the various models thanks to its composition mechanism. The formal analysis techniques addressed are intended to exhibit interesting behaviours; for example,

* to check liveness properties of the IS, as security constraints can be too strict and then block the system;

* to check that the access control forbids the system to enter undesirable functional states;
* to find malicious behaviours like insider threats performed by authorized users in order to bypass the security policies;

* to produce positive and negative test scenarios, to check the correctness of normal behaviours and the effects produced by non-nominal (undesired) variations of these normal scenarios;

A backward symbolic search algorithm has been proposed in the PhD thesis of A. Radhouani in order to extract attack scenarios that are made possible by the evolution of the functional state of the IS. In addition, this approach is able to extract malicious behaviours performed by a single user or several users on coalition. The technique presented in Chapter 3 has been complemented with a two-steps approach: the first step focuses on the functional model regardless of users and their roles in order to extract the sequences of functional operations that reach the malicious goal; and the second step guides ProB with a CSP model to identify users able to perform such attacks according to the security model. This work led to the development of GenISIS, a tool that is used to exhibit execution paths from a B modelling of an IS. GenISIS has been experimented with several case studies such as the meeting scheduler example discussed in (Basin et al., 2009, Radhouani et al., 2015), the medical IS studied in (Ledru et al., 2015b) and the conference review IS inspired by (Zhang et al., 2008). For each example, GeneISIS aimed to reach the same malicious goal as handled in the article which addressed the same example, and it was able to extract all reported attacks. Some metrics about these experiments are given in Table 1.

<table><caption>Table 1: Summary table of experiments</caption><thead><tr><th>Case study</th><th>Operations</th><th>Variables</th><th>Permissions</th><th>Roles</th><th>Users</th><th>scenarios</th></tr></thead><tbody><tr><td>Library</td><td>13</td><td>4</td><td>3</td><td>2</td><td>3</td><td>8</td></tr><tr><td>Medical IS<br>(Ledru et al., 2015b)</td><td>15</td><td>9</td><td>3</td><td>4</td><td>3</td><td>10</td></tr><tr><td>Meeting scheduler<br>(Basin et al., 2009)</td><td>23</td><td>7</td><td>5</td><td>3</td><td>3</td><td>8</td></tr><tr><td>Bank IS<br>(Bandara et al., 2010)</td><td>31</td><td>11</td><td>4</td><td>2</td><td>3</td><td>9</td></tr><tr><td>Conference Review<br>(Zhang et al., 2008)</td><td>48</td><td>24</td><td>8</td><td>3</td><td>4</td><td>14</td></tr></tbody></table>

My works mainly addressed the modeling activities and were based on Platform Independent Models (PIM), described using UML models and their associated formal B specifications. However, in addition to modeling notions, MDS also promotes the transformation of the PIM into a PSM. The objective is to translate access control into concrete security mechanisms of a target infrastructure. In practice, this transformation usually includes manual coding activities. The challenge is therefore to guarantee that security models, graphically designed and formally
validated, correspond to a deployed security policy. One way to address this perspective is to
apply conformance testing.

From the PIM level, testing activities can take several directions: (1) validation of the normal behavior of the IS regarding its security rules, (2) automated generation of security tests from valid functional scenarios, etc. The PSM level validation can be done by verifying whether the PSM complies with the specification and its validation activities. In this context the goal is twofold: (1) extract PSM models of target technologies like web applications and databases, and (2) translate the validation activities carried out on PIM models into validation activities at the implementation level. This can be achieved by the extraction of security monitors, and/or the production of log files that can be further analysed applying trace analysis techniques.

Formal xDSLs

Several research works have been devoted by the MDE community in order to deal with ex-
ecutable DSLs. Combemale (2015) state that the intention is to support early validation and
verification in the development process. Indeed, an executable model not only represents the
structural features of a system, but also deals with its behaviour. The model is therefore in-
tended to behave like the final system should run, which provides the capability to simulate,
animate and debug the system’s properties before its implementation. In the literature there are
two major approaches to implement the execution semantics of a DSL: translational approaches
and in-place approaches. The former translate the DSL semantics into a well-established se-
mantic domain that is assisted by numerous tools. The latter weave the execution semantics
into meta-models, which is often done by extending the semantic domain of a DSL with action
languages. Every approach has its strengths and limitations that can be summarized by:

* Translational approaches:

- *Strengths*: apply available tools, such as animators and/or model-checkers to ensure the execution capabilities of the DSL.

- *Limitations*: first, often these approaches require complex transformations to im-
  plement the mapping from the DSL to the target semantic domain, and second, the
  execution results are only obtained in the target domain.

• In-place approaches:

- *Strengths*: allow a more intuitive definition of executable DSLs since the language engineer has only to deal with concepts of the DSL and not with another target language.

- *Limitations*: require to implement for each DSL all the execution-based tools.

Since the objective of an xDSL is to ensure early validation during the development process,
the developer must have some confidence in the underlying verification tool. Nonetheless, on
the one hand, Kosar et al. (2016) and Iung et al. (2020) show that the verification feature of existing language workbenches (LWBs) is very limited; and on the other hand, the dependability of the resulting system is strongly related to the correctness of the DSL. Voelter et al. (2019) analysed the risks of using LWBs regarding the introduction of faults into a critical software component. The authors observed that existing LWBs have not been developed using a safety process and attested that “*particular DSLs could be, but that is only of limited use if the underlying LWB is not*”. In this sense, a translational approach is much more pragmatic because it reuses well-established verification tools, that are often widely accepted by the formal methods community.

In my opinion, bridging the gap between both worlds (xDSLs and FM) does not require innovative solutions and can be done by integrating well-established tools provided by both the Formal Methods community and the MDE community. The lack of automated formal reasoning in LWBs is not due to the complexity of formal methods and their mathematical background, but originates from the lack of initiatives that are dedicated to the integration of both techniques. A supporting argument could be the assertion by Kosar et al. (2016) that “*researchers within the DSL community are more interested in creating new techniques than they are in performing rigorous [empirical] evaluations*”. Unfortunately, not only the integration attempts remain poor, but also the applications of existing approaches remain limited to illustrative examples without going further towards realistic safety-critical requirements. This observation may explain why existing approaches (Rivera et al., 2009, Gargantini et al., 2010b, Merilinna and Pärrssinen, 2010, Tikhonova, 2017b, Zalila et al., 2013) are not discussed at all in the systematic mapping studies of Kosar et al. (2016) and Iung et al. (2020). Meeduse is a LWB providing solutions to this limitation. It allows one to formally define and reason about the semantics of xDSLs using the formal B method. The underlying approach is a translational approach, but it goes a step further in comparison with existing translational approaches by providing effective solutions to the limitations mentioned above. The applications and case studies presented in Chapter 5 show that the integration of executable DSLs together with theorem proving, animation and model-checking is viable and should be explored further.

The usage of B in my works appears as a good choice for two reasons: (1) the availability of a rich UML-to-B state of the art, which provides a viable translation from ECore into B (considering that ECore is conformant to the MOF, which is a restriction of UML); and (2) the usage of theorem proving, in addition to model-checking, to guarantee zero-fault DSLs. In most application domains such as Requirements Engineering, Enterprise Architectures, Business Process Management and Legal Contracts, where DSLs do exist, the commonly used verification tools are model checkers and/or SAT/SMT solvers. Meeduse introduces theorem proving to these domains. Besides my own experience and judgement, the B Method has been compared to other state based formal methods and tools in (Mashkoor et al., 2018) and got several good points. Regarding scalability, which is “*the ability to be well applicable to arbitrarily large and complex projects*”, the B method is ranked (Good). The work also highly ranks the verification features of B and its tool support. Figure 1 gives the evolution time-line of the tool with the
major highlights and current and short-term perspectives.

<figure><img src="image_83.png" /><figcaption>Figure 1: Evolution time-line of Meeduse</figcaption></figure>

The red time-lines refer to DSL tools that are powered by Meeduse and which have their
own existence, such as MeeNET. The latter investigates several interesting research directions
such as DSL refinements and transpilation. Meeduse has been experimented on various kinds of
applications in order to evaluate its strength. For example, in the smart-home domain (project
DomoSur) the objective was the execution of the DSL at run-time, being inspired by (Körner
et al., 2020). The approach also covers model transformations (M2M) and currently, I am work-
ing on bi-directional transformations by addressing two features: (1) proving the isomorphism
of a transformation in B, and (2) updating the input model from changes done in the output
model (propagation).

The xOWL project (executable OWL), started last year, addresses knowledge engineering.
It has a different view and studies the possibility to consider other application domains, which
would allow the analysis of the implications of FMDE outside safety-critical systems. The
motivation of the project is that domain ontologies evolve continuously, which leads to several
problems, especially change impact analysis and resolution. Among existing works, pattern-
driven techniques have been proposed to provide guidance during the ontology evolution so
that it remains consistent. In the xOWL project, ontologies are described via the Ontology Web
Language (OWL). Considering that OWL is a DSL, the proposal is to rethink the underlying
evolution patterns by means of execution semantics that apply the expected changes to a given
ontology. The W3C functional syntax of OWL has been instrumented in Meeduse, leading to a
lightweight development approach. Indeed, the development effort is limited to the specification
of the evolution patterns and their verification and validation. All the other features of xOWL
(execution, verification and debugging) are provided by Meeduse.
Personal opinion

Undoubtedly, the usage of a formal method with well-established verification tools is a solution to neutralize bugs that may originate from a modeling language. The question is: “*how to provide the good mixture between correctness and expressiveness?*”. I believe that the answer depends on the application domain of the language. Indeed, formal methods are often negatively perceived by developers due to their mathematical notations, and consequently translational approaches have a limited usage for general purpose applications. Nonetheless, formal methods showed their strengths in the safety-critical domain, and they became a strong requirement to ensure zero-fault applications. On the other side, MDE provides several benefits to this field due to the usage of DSLs and the ability to share, visualize and communicate about domain concepts. Both formal methods and model-driven engineering are desirable in safety critical systems because domain-specific representations are omnipresent, as well as the use of provers and model-checkers. I assume that the reader may agree with this claim, even if it appears that for larger scale projects formal methods are not as widespread, because of the overhead they may create during the development activities.

Note that The backbone of my works, for MDS and DSLs, is the UML-to-B translation. It can be considered that MDS is a particular case of DSLs and hence an interesting technical perspective would be to revisit B4MSecure using Meeduse. In fact, B4MSecure translates UML and RBAC into B applying model-to-model transformations written in Java. Considering that UML, RBAC and B are DSLs, and having their meta-models, it is possible to rewrite the transformations using B, prove their correctness, and execute them in Meeduse. Even if Meeduse is a recent tool (its reference papers appeared in 2020), the underlying approach is not new since it provides a translation semantics to a DSL. The limitations of this kind of approach were widely discussed in the literature (Bryant et al., 2011). The first one is that it “*is very challenging to correctly map the constructs of the DSL into the constructs of the target language*”. The use of the B method in Meeduse provides objective answers to this observation because the semantics of meta-models is defined by means of OCL constructs in the MOF. These are built on the set theory and the first order predicate logic, which are also the foundations of the B language. Structurally a meta-model is a restriction of UML, which is comforting because this means that mapping a DSL into B is not very challenging. It can be done via a classical UML-to-B approach, which has been addressed in the past (since the 2000s) by a plethora of techniques. My research works made this translation more effective than existing techniques; first, by providing tools and second by embedding ProB in these tools.

Furthermore, the second limitation of translational approaches, as discussed in (Bryant et al., 2011), is that “*the mapping of execution results back into the DSL is not covered*”. Indeed, in the existing works the V&V activities are only obtained in the target domain because getting back the results in the source language is often claimed to be difficult and requires to extend the abstract syntax of the input DSL in order to model these results. Existing works start from a model (in UML or in a given DSL), produce a formal specification and then they “get lost”
in the formal process. By embedding ProB, Meeduse gave a new vision to the integration of
formal methods and modeling languages.

Every UML-to-B approach has its advantages and limitations. Obviously for a better coverage of UML a combination of the various approaches is needed. The major challenge was how to gather into a unifying framework several UML-to-B approaches from the rich state of the art. In B4MSecure and Meeduse the user is able to select the desired UML-to-B transformation technique and also to combine rules coming from various techniques. This is interesting because UML has been mapped into numerous state-based formal languages with similar principles (e.g. Z, Object-Z, etc), and therefore the only remaining piece is to reuse these mappings within the tool. I am aware that in order to broaden the spectrum of B4MSecure and Meeduse several target formal approaches have to be addressed. This objective is reachable since the power of both tools comes from ProB, and ProB is itself a multi-target platform covering (in addition to B) Event-B, Z, Alloy and TLA+.
Bibliography

Abrial, J.-R. (1996). *The B-book: assigning programs to meanings*. Cambridge University Press.

Abrial, J.-R. and Mussat, L. (1998). Introducing dynamic constraints in B. In *B'98: Recent Advances in the Development and Use of the B Method, Second International B Conference, Montpellier, France, April 22-24, 1998, Proceedings*, pages 83–128. LNCS.

Ahn, G.-J. and Hu, H. (2007). Towards realizing a formal rbac model in real systems. In *Proceedings of the 12th ACM Symposium on Access Control Models and Technologies (SAC-MAT'07)*, pages 215–224, New York, NY, USA. Association for Computing Machinery.

Aït-Ameur, Y., Ait-Sadoune, I., Hacid, K., and Oussaid, L. M. (2017). Formal modelling of ontologies within Event-B. In *First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development*. https://hal.archives-ouvertes.fr/hal-01636944/file/IMPEX_2017_paper_3.pdf.

Andova, S., van den Brand, M., Engelen, L., and Verhoeff, T. (2012). MDE basics with a DSL focus. In *Formal Methods for Model-Driven Engineering - 12th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, volume 7320 of LNCS*, pages 21–57. Springer.

Attiogbe, C. (2009). Semantic Embedding of Petri Nets into Event-B. In *Integration of Model-based Formal Methods Tools (IM_FMT @ IFM'2009)*, Dusseldorf, Germany. http://www.lina.sciences.univ-nantes.fr/apcb/IM_FMT2009/index.html.

Baar, T. (2005). Non-deterministic constructs in OCL - what does any() mean. In *Model Driven - 12th International SDL Forum*, volume 3530 of LNCS, pages 32–46. Springer.

Bandara, A., Shinpei, H., Jurjens, J., Kaiya, H., Kubo, A., Laney, R., Mouratidis, H., Nhla-batsi, A., Nuseibeh, B., Tahara, Y., Tun, T., Washizaki, H., Yoshioka, N., and Yu, Y. (2010). *Security Patterns: Comparing Modeling Approaches*. IGI Global.

Basin, D., Clavel, M., Doser, J., and Egea, M. (2009). Automated analysis of security-design models. *Information & Software Technology*, 51.
Basin, D., Clavel, M., and Egea, M. (2011). A Decade of Model-Driven Security. In *Proceedings of the 16th ACM Symposium on Access Control Models and Technologies*, SACMAT’11, pages 1–10. ACM.

Basin, D., Doser, J., and Lodderstedt, T. (2006). Model driven security: From UML models to access control infrastructures. *ACM Trans. Softw. Eng. Methodol.*, 15(1).

Becker, M. Y. and Nanz, S. (2010). A logic for state-modifying authorization policies. *ACM Trans. Inf. Syst. Secur.*, 13(3):20:1–20:28.

Bert, D., Potet, M.-L., and Stouls, N. (2005). GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties. In H. Treharne, S. King, M. C. Henson, and S. A. Schneider, editors, *ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users*, volume 3455 of LNCS. Springer-Verlag.

Bjørner, D. (2010). Rôle of domain engineering in software development. In *Perspectives of Systems Informatics*, pages 2–34. Springer.

Bousse, E., Leroy, D., Combemale, B., Wimmer, M., and Baudry, B. (2018). Omniscient debugging for executable dsls. *Journal of Systems and Software*, 137:261–288.

Bryant, B. R., Gray, J., Mernik, M., Clarke, P. J., France, R. B., and Karsai, G. (2011). Challenges and directions in formalizing the semantics of modeling languages. *Comput. Sci. Inf. Syst.*, 8(2):225–253.

Butler, M. J., Körner, P., Krings, S., Lecomte, T., Leuschel, M., Mejia, L., and Voisin, L. (2020). The first twenty-five years of industrial use of the b-method. In ter Beek, M. H. and Nickovic, D., editors, *Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings*, volume 12327 of *Lecture Notes in Computer Science*, pages 189–209. Springer.

Butler, M. J. and Leuschel, M. (2005). Combining CSP and B for specification and property verification. In *International Symposium of Formal Methods - FM 2005*, volume 3582 of *Lecture Notes in Computer Science*, pages 221–236. Springer.

Butler, M. J., Raschke, A., Hoang, T. S., and Reichl, K. (2018). *Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th Int. Conference, ABZ 2018*, volume 10817 of LNCS. Springer.

Combemale, B. (2015). *Towards Language-Oriented Modeling*. Habilitation à diriger des recherches, Université de Rennes 1.

Cuadrado, J. S. and Molina, J. G. (2007). A phasing mechanism for model transformation languages. In *SAC*, pages 1020–1024.
Czarnecki, K. and Helsen, S. (2006). Feature-based survey of model transformation approaches.
*IBM Systems Journal*, 45(3):621–646.

Deantoni, J. (2016). Modeling the behavioral semantics of heterogeneous languages and their coordination. In *2016 Architecture-Centric Virtual Integration (ACVI)*, pages 12–18.

Dijkstra, E. W. (1975). Guarded Commands, Nondeterminacy and Formal Derivation of Programs. *Communication of the ACM*, 18(8):453–457.

Eclipse (2012). Acceleo.

Eclipse (2021). Eclipse QVT Operational 2021-12 (3.10.5).
https://projects.eclipse.org/projects/modeling.mmt.qvt-oml. Accessed: 20-12-2021.

Efftinge, S. (2006). openarchitectureware 4.1 expressions framework reference.

ePNK Homepage, T. (2020). http://www2.compute.dtu.dk/~ekki/projects/ePNK/index.shtml. Accessed: 15-12-2020.

EProvide (2020). http://eprovide.sourceforge.net. Accessed: 15-12-2020.

ERA, UNISIG, E. E. U. G. (2016). System Requirements Specification, SUBSET-026. Technical report, European Railway Agency. Version 3.6.0.

Essamé, D. (2004). La méthode B et l'ingénierie Système. *TSI (Technique et Science Informatics)*, 23(7):929–938.

Ferraiolo, D. F., Sandhu, R. S., Gavrila, S. I., Kuhn, D. R., and Chandramouli, R. (2001). Proposed NIST standard for Role-based Access Control. In *ACM Transactions on Information and System Security (TISSEC)-01*, pages 224–274.

Fisler, K., Krishnamurthi, S., Meyerovich, L. A., and Tschantz, M. C. (2005). Verification and change-impact analysis of access-control policies. In *Proceedings of the 27th International Conference on Software Engineering, ICSE '05*, pages 196–205, New York, NY, USA. ACM.

Floyd, R. W. (1993). *Assigning Meanings to Programs*. Springer Netherlands, Dordrecht.

Fowler, M. (2005). Language workbenches: The killer-app for domain specific languages? http://martinfowler.com/articles/languageWorkbench.html.

Garcia-Dominguez, A. and Hinkel, G. (2019). Truth Tables to Binary Decision Diagrams. In Garcia-Dominguez, A., Hinkel, G., and Krikava, F., editors, *Proceedings of the 12th Transformation Tool Contest, a part of the Software Technologies: Applications and Foundations (STAF 2019) federation of conferences*, CEUR Workshop Proceedings. CEUR-WS.org.
Gardner, T., Griffin, C., Koehler, J., and Hauser, R. (2003). A review of OMG MOF 2.0 Query / Views / Transformations submissions and recommendations towards the final standard. Meta-Modelling for MDA Workshop.

Gargantini, A., Riccobene, E., and Scandurra, P. (2010a). Combining formal methods and mde techniques for model-driven system design and analysis. *Advances in Software*, 3(1&2).

Gargantini, A., Riccobene, E., and Scandurra, P. (2010b). Combining formal methods and mde techniques for model-driven system design and analysis. *International Journal On Advances in Software*, 1.

Gehlot, V. and Nigro, C. (2010). An introduction to systems modeling and simulation with colored petri nets. In *Proceedings of the 2010 Winter Simulation Conference, WSC 2010, USA, 5-8 December 2010*, pages 104–118.

Gogolla, M., Büttner, F., and Richters, M. (2007). Use: A uml-based specification environment for validating uml and ocl. *Science of Computer Programming*, 69(1):27–34. Special issue on Experimental Software and Toolkits.

Greitzer, F. L. (2019). Insider Threats: It's the HUMAN, Stupid! In *Proceedings of the North-west Cybersecurity Symposium, NCS '19, New York, NY, USA. Association for Computing Machinery*.

Hagalisletto, A. M., Bjørk, J., Yu, I. C., and Enger, P. (2007). Constructing and refining large-scale railway models represented by petri nets. *IEEE Trans. Systems, Man, and Cybernetics, Part C*, 37(4):444–460.

Harel, D. and Rumpe, B. (2004). Meaningful modeling: What's the semantics of "semantics"? *Computer*, 37:64 – 72.

Hartmann, T. and Sadilek, D. A. (2008). Undoing operational steps of domain-specific modeling languages. In *Proceedings of the 8th OOPSLA Workshop on Domain-Specific Modeling (DSM'08) - University of Alabama at Birmingham*.

Hazem, L., Levy, N., and Marcano-Kamenoff, R. (2004). UML2B : un outil pour la génération de modèles formels. In *Julliard, J., editor, AFADL'2004 - Session Outils*.

Hillah, L. M., Kindler, E., Kordon, F., Petrucci, L., and Trèves, N. (2009). A primer on the Petri Net Markup Language and ISO/IEC 15909-2. *Petri Net Newsletter*, 76:9–28.

Hoare, C. A. R. (1969). An axiomatic basis for computer programming. *Communication of the ACM*, 12(10):576–580.

Hoare, C. A. R. (1985). *Communicating Sequential Processes*. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
Höhn, S. and Jürjens, J. (2008). Rubacon: Automated support for model-based compliance engineering. In *Proceedings of the 30th International Conference on Software Engineering, ICSE'08*, pages 875–878, New York, NY, USA. Association for Computing Machinery.

Homepage, P. F. (2020). https://pnml.lip6.fr. Accessed: 15-12-2020.

Homoliak, I., Toffalini, F., Guarnizo, J., Elovici, Y., and Ochoa, M. (2019). Insight Into Insiders and IT: A Survey of Insider Threat Taxonomies, Analysis, Modeling, and Countermeasures. *ACM Computing Surveys*, 52(2).

Infrabel (2017). Stabilisation du nombre de dépassements de signaux sur le rail en 2016. https://www.infrabel.be/fr/presse/stabilisation-du-nombre-depassements-signaux-rail-2016.

International Union of Railways (UIC) (2016). RailTopoModel - Railway infrastructure topological model. ISBN 978-2-7461-2513-1.

ISO/IEC (2011). *Systems and software engineering – High-level Petri nets – Part 2: Transfer format*, International Standard ISO/IEC 15909-2.

Iung, A., Carbonell, J., Marchezan, L., Rodrigues, E. M., Bernardino, M., Basso, F. P., and Medeiros, B. (2020). Systematic mapping study on domain-specific language development tools. *Empirical Software Engineering*, 25(5):4205–4249.

Idani, A. (2006). *B/UML : Mise en relation de spécifications B et de descriptions UML pour l'aide à la validation externe de développements formels en B*. PhD thesis, Université de Grenoble 1.

Idani, A. (2009). UML models engineering from static and dynamic aspects of formal specifications. In *14th International Conference Exploring Modeling Methods for Systems Analysis and Development (EMMSAD)*, held at CAiSE 2009, volume 29 of LNBIP, pages 237–250. Springer.

Idani, A. (2020a). Dependability of Model-Driven Executable DSLs, Critical Review and Solutions. In *14th European Conference on Software Architecture, Companion Proceedings*, volume 1269 of CCIS, pages 358–373. Springer.

Idani, A. (2020b). Meeduse: A tool to build and run proved DSLs. In Dongol, B. and Troubitsyna, E., editors, *16th International Conference on Integrated Formal Methods (IFM)*, volume 12546 of LNCS, pages 349–367. Springer.

Idani, A. (2021). A Lightweight Development of Outbreak Prevention Strategies Built on Formal Methods and xDSLs. In *2nd ACM European Symposium on Software Engineering (ESSE)*. ACM.
Idani, A. (2022). Formal model-driven executable DSLs. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 18(1).

Idani, A., Boulanger, J.-L., and Philippe, L. (2009). Linking paradigms in safety critical systems. *International Journal of Computers and their Applications (IJCA), Special Issue on the Application of Computer Technology to Public Safety and Law Enforcement*, 16(2).

Idani, A. and Coulette, B. (2008). Towards reverse-engineering of UML views from structured formal developments. In Cordeiro, J. and Filipe, J., editors, *Proceedings of the Tenth International Conference on Enterprise Information Systems (ICEIS)*, pages 94–103.

Idani, A., Labiadh, M., and Ledru, Y. (2010a). Infrastructure dirigée par les modèles pour une intégration adaptable et évolutive de UML et B. *Ingénierie des Systèmes d'Information*, 15(3):87-112. Extended version.

Idani, A., Labiadh, M., and Ledru, Y. (2010b). Infrastructure dirigée par les modèles pour une intégration adaptable et évolutive de UML et B. *Ingénierie des Systèmes d'Information*, 15(3):87-112. Extended version.

Idani, A. and Ledru, Y. (2015). B for Modeling Secure Information Systems, The B4MSecure Platform. In Butler, M. J., Conchon, S., and Zaidi, F., editors, *17th International Conference on Formal Engineering Methods (ICFEM)*, Paris, France, November 3-5, volume 9407 of LNCS, pages 312–318. Springer.

Idani, A., Ledru, Y., Ait-Wakrime, A., Ben-Ayed, R., and Bon, P. (2019a). Towards a Tool-Based Domain Specific Approach for Railway Systems Modeling and Validation. In *Third International Conference on Reliability, Safety, and Security of Railway Systems (RSS-Rail'2019)*, volume 11495 of LNCS, pages 23–40. Springer.

Idani, A., Ledru, Y., Ait-Wakrime, A., Ben-Ayed, R., and Collart-Dutilleul, S. (2019b). Incremental Development of a Safety Critical System Combining formal Methods and DSMLs – Application to a Railway System. In *24th International Conference on Formal Methods for Industrial Critical Systems (FMICS'2019)*, volume 11687 of LNCS, pages 93–109. Springer.

Idani, A., Ledru, Y., and Vega, G. (2020). Alliance of Model Driven Engineering with a Proof-based Formal Approach. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 16(3):289-307.

Idani, A., Vega, G., and Leuschel, M. (2019c). Applying Formal Reasoning to Model Transformation: The Meeduse solution. In *Proceedings of the 12th Transformation Tool Contest, co-located with STAF'2019, Software Technologies: Applications and Foundations*, volume 2550 of CEUR Workshop Proceedings, pages 33–44.

Jackson, D. (2002). Alloy: A Lightweight Object Modelling Notation. *ACM Trans. Softw. Eng. Methodol.*, 11(2):256–290.
James, P., Knapp, A., Mossakowski, T., and Roggenbach, M. (2013). Designing DSLs - A Craftsman's Approach for the Railway Domain Using CASL. In *Recent Trends in Algebraic Development Techniques*. Springer.

Jensen, K. (1981). Coloured Petri Nets and the invariant-method. *Theoretical Computer Science*, 14:317–336.

Jézéquel, J.-M., Combemale, B., Barais, O., Monperrus, M., and Fouquet, F. (2013). Mashup of Meta-Languages and its Implementation in the Kermeta Language Workbench. *Software and Systems Modeling*.

Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I., and Valduriez, P. (2006). Atl: A qvt-like transformation language. In *Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications*, OOPSLA ’06, pages 719–720, New York, NY, USA. ACM.

Jürjens, J. (2010). *Secure Systems Development with UML*. Springer-Verlag.

Jürjens, J., Lehrhuber, M., and Wimmel, G. (2005). Model-based design and analysis of permission-based security. In *10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’05)*, pages 224–233.

Koleini, M. and Ryan, M. (2011). A knowledge-based verification method for dynamic access control policies. In *Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings*, volume 6991 of LNCS, pages 243–258. Springer.

Kont, M., Pihelgas, M., Wojtkowiak, J., Trinberg, L., and Osula, A.-M. (2018). *Insider Threat Detection Study*. The NATO Cooperative Cyber Defence Centre of Excellence.

Körner, P., Bendisposto, J., Dunkelau, J., Krings, S., and Leuschel, M. (2019). Embedding high-level formal specifications into applications. In *International Conference on Formal Methods (FM)*, volume 11800 of LNCS. Springer.

Körner, P., Bendisposto, J., Dunkelau, J., Krings, S., and Leuschel, M. (2020). Integrating formal specifications into applications: the prob java api. *Formal Methods in System Design*.

Kosar, T., Bohra, S., and Mernik, M. (2016). Domain-specific languages: A systematic mapping study. *Information and Software Technology*, 71:77–91.

Kuhlmann, M., Sohr, K., and Gogolla, M. (2013). Employing UML and OCL for designing and analysing role-based access control. *Mathematical Structures in Computer Science*, 23(4).

Laleau, R. and Mammar, A. (2000). An Overview of a Method and Its Support Tool for Generating B Specifications from UML Notations. In *15th IEEE International Conference on Automated Software Engineering*, pages 269–272. IEEE Computer Society Press.
Laleau, R. and Polack, F. (2002). Coming and going from uml to b: A proposal to support traceability in rigorous is development. In *2nd International Conference of B and Z Users*, volume 2272 of LNCS, pages 517–534. Springer.

Langer, P., Mayerhofer, T., and Kappel, G. (2014). Semantic model differencing utilizing behavioral semantics specifications. In *17th International Conference Model-Driven Engineering Languages and Systems - MODELS*, volume 8767 of LNCS, pages 116–132. Springer.

Lano, K., Clark, D., and Androutsopoulos, K. (2004). UML to B: Formal Verification of Object-Oriented Models. In *Integrated Formal Methods*, volume 2999 of LNCS. Springer.

Ledang, H. (2001). Automatic translation from uml specifications to b. In *Automated Software Engineering*, page 436.

Ledru, Y. (2006). Using jaza to animate roz specifications of UML class diagrams. In *30th Annual IEEE / NASA Software Engineering Workshop (SEW-30)*, pages 253–262. IEEE Computer Society.

Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J.-L., and Labiadh, M.-A. (2014). Validation of IS security policies featuring authorisation constraints. *International Journal of Information System Modeling and Design (IJISMD)*.

Ledru, Y., Idani, A., and Richier, J. (2015a). Validation of a security policy by the test of its formal B specification - A case study. In *3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE*, pages 6–12. IEEE Computer Society.

Ledru, Y., Idani, A., Ayed, R. B., Wakrime, A. A., and Bon, P. (2019). A separation of concerns approach for the verified modelling of railway signalling rules. In Dutilleul, S. C., Lecomte, T., and Romanovsky, A. B., editors, *Third International Conference on Reliability, Safety, and Security of Railway Systems - Modelling, Analysis, Verification, and Certification (RSSRail)*, volume 11495 of LNCS, pages 173–190. Springer.

Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J., and Labiadh, M. (2015b). Validation of IS security policies featuring authorisation constraints. *International Journal of Information System Modeling and Design*, 6(1):24–46.

Leroy, X. (2009). Formal verification of a realistic compiler. *Communications of the ACM*, pages 107–115.

Leuschel, M. and Butler, M. (2003). ProB: A Model Checker for B. In *FME 2003: Formal Methods Europe*, volume 2805 of LNCS. Springer-Verlag.

Leuschel, M. and Butler, M. (2008). Prob: an automated analysis toolset for the b method. *International Journal on Software Tools for Technology Transfer*, 10(2):185–203.
Lienhard, A., Gîrba, T., and Nierstrasz, O. (2008). Practical object-oriented back-in-time debugging. In Vitek, J., editor, *ECOOP 2008 – Object-Oriented Programming*, pages 592–615. Springer.

Mammar, A. and Frappier, M. (2015). Proof-based verification approaches for dynamic properties: application to the information system domain. *Formal Asp. Comput.*, 27(2):335–374.

Mandell, R. and Estrin, G. (1966). A meta-compiler as a design automation tool. In *Proceedings of the SHARE Design Automation Project*, DAC’66, pages 1–13, USA. ACM.

Martin, S. (2003). The Best of Both Worlds Integrating UML with Z for Software Specifications. *Journal of Computing and Control Engineering*, 14:8–11.

Mashkoor, A., Kossak, F., and Egyed, A. (2018). Evaluating the suitability of state-based formal methods for industrial deployment. *Softw. Pract. Exp.*, 48(12):2350–2379.

Matulevicius, R. and Dumas, M. (2010). Towards model transformation between secureuml and umlsec for role-based access control. In Barzdins, J. and Kirikova, M., editors, *Databases and Information Systems VI (DB&IS’10), July 5-7, volume 224 of Frontiers in Artificial Intelligence and Applications*, pages 339–352. IOS Press.

Mayerhofer, T., Langer, P., Wimmer, M., and Kappel, G. (2013). Towards xmof: Executable dsmls based on fuml. In *International Conference on Software Language Engineering - SLE*, volume 8225 of LNCS, pages 56–75. Springer.

Meeduse (2020). http://vasco.imag.fr/tools/meeduse/. Accessed: 15-12-2020.

Merilinna, J. and Pärssinen, J. (2010). Verification and validation in the context of domain-specific modelling. In *Proceedings of the 10th Workshop on Domain-Specific Modeling*, pages 9:1–9:6, New York, NY, USA. ACM.

Merkle, D. and Middendorf, M. (2006). Ant colony optimization. *European Journal of Operational Research*, 168(1):269–271.

Meyer, E. (2001). *Développements formels par objets : utilisation conjointe de B et d’UML*. PhD thesis, Université de Nancy 2.

Muller, P.-A., Fleurey, F., and Jézéquel, J.-M. (2005). Weaving executability into object-oriented meta-languages. In *Proceedings of MODELS/UML’2005*, Montego Bay, Jamaica.

Object Management Group (2011). *Semantics of a Foundational Subset for Executable UML Models (fUML)*. https://www.omg.org/spec/FUML/.

Object Management Group (2015). *Meta Object Facility (MOF) 2.5.1 Core Specification*. https://www.omg.org/spec/MOF/2.5.1/.
OMG (2003). MDA Guide Version 1.0.1. http://www.omg.org/mda/. http://www.omg.org/cgi-bin/doc?omg/03-06-01.pdf.

Oxford (2020). *The Oxford Dictionary*. Oxford University Press.

Petri, C. A. and Reisig, W. (2008). Petri net. *Scholarpedia*, 3(4):6477.

Petri-net ecore file (2020). https://github.com/gemoc/petrinet/blob/master/petrinetv1/fr.inria.diverse.sample.petrinetv1.model/model/petrinetv1.ecore. Accessed: 15-12-2020.

PNML Homepage (2020). http://www.pnml.org. Accessed: 15-12-2020.

Pouzancre, G. (2003). How to Diagnose a Modern Car with a Formal B Model? In Bert, D., Bowen, J. P., King, S., and Waldén, M., editors, *ZB 2003: Formal Specification and Development in Z and B*, pages 98–100, Berlin, Heidelberg. Springer Berlin Heidelberg.

Power, D., Slaymaker, M., and Simpson, A. (2010). On the modelling and analysis of Amazon Web Services access policies. In *Proceedings of Abstract State Machines, Alloy, B and Z (ABZ 2010)*, page 394. Springer-Verlag LNCS, volume 5977.

Probst, C. W., Hunker, J., Gollmann, D., and Bishop, M., editors (2010). *Insider Threats in Cyber Security*, volume 49 of *Advances in Information Security*. Springer.

Qamar, N., Ledru, Y., and Idani, A. (2011a). Evaluating RBAC supported techniques and their validation and verification. In *Sixth International Conference on Availability, Reliability and Security (ARES), Vienna, Austria, August 22-26*, pages 734–739. IEEE Computer Society.

Qamar, N., Ledru, Y., and Idani, A. (2011b). Validation of security-design models using Z. In Qin, S. and Qiu, Z., editors, *13th International Conference on Formal Engineering Methods (ICFEM), Durham, UK, October 26-28*, volume 6991 of LNCS, pages 259–274. Springer.

Radhouani, A., Idani, A., Ledru, Y., and Rajeb, N. B. (2015). Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. *LNCS Transactions on Petri Nets and Other Models of Concurrency*, 10:131–152.

RailML (2018). RailML Latest Release 3.1. https://www.railml.org/en/home.html. Accessed: 2021-12-03.

Rivera, J., Durán, F., and Vallecillo, A. (2009). Formal specification and analysis of domain specific models using maude. *Simulation*, 85:778–792.

Sarna-Starosta, B. and Stoller, S. D. (2004). Policy analysis for security-enhanced linux. In *Proceedings of the 2004 Workshop on Issues in the Theory of Security (WITS)*, pages 1–12. Available at http://www.cs.sunysb.edu/~stoller/WITS2004.html.
Schaad, A. and Moffett, J. D. (2002). A lightweight approach to specification and analysis of role-based access control extensions. In *Proceedings of the Seventh ACM Symposium on Access Control Models and Technologies*, pages 13–22, New York, NY, USA. Association for Computing Machinery.

Schon, W., Larraufie, G., MoÃ¤«ns, G., and PorÃ©, J. (2014). *Railway signalling and automation Volume 3. La vie du rail*.

Snook, C. and Butler, M. (2004). U2B-A tool for translating UML-B models into B. In Mermet, J., editor, *UML-B Specification for Proven Embedded Systems Design*.

Snook, C. and Butler, M. (2006a). UML-B: Formal Modeling and Design Aided by UML. *ACM Transactions of Software Engineering Methodologies*, 15(1):92–122.

Snook, C. and Butler, M. (2006b). UML-B: Formal modeling and design aided by UML. *ACM Transactions on Software Engineering and Methodology*, 15(1).

Sohr, K., Drouineaud, M., Ahn, G.-J., and Gogolla, M. (2008). Analyzing and managing role-based access control policies. *IEEE Transactions on Knowledge and Data Engineering*, 20(7):924–939.

Spivey, J. M. (1992). The Z Notation: A reference manual (2nd ed.). Prentice Hall.

Steinberg, D., Budinsky, F., Paternostro, M., and Merks, E. (2008). *EMF: Eclipse Modeling Framework*. Addison-Wesley, 2nd edition.

Steinberg, D., Budinsky, F., Paternostro, M., and Merks, E. (2009). *EMF: Eclipse Modeling Framework 2.0*. Addison-Wesley Professional, 2nd edition.

Svendsen, A., Haugen, Ø., and Møller-Pedersen, B. (2012). Synthesizing software models: Generating train station models automatically. In *Integrating System and Software Modeling*, pages 38–53. Springer.

The Standish Group (2008). Chaos report. http://www.cs.nmt.edu/~cs328/reading/Standish.pdf – last visited 15th of June, 2008.

Thong, W. J. and Ameedeen, M. A. (2015). A survey of petri net tools. In *Advanced Computer and Communication Engineering Technology*, pages 537–551, Cham. Springer.

Tikhonova, U. (2017a). *Engineering the dynamic semantics of domain specific languages*. PhD thesis, Department of Mathematics and Computer Science. Proefschrift.

Tikhonova, U. (2017b). Reusable specification templates for defining dynamic semantics of dsls. *Software & Systems Modeling*.
Tikhonova, U., Manders, M., Brand, van den, M., Andova, S., and Verhoeff, T. (2013). Applying model transformation and event-b for specifying an industrial dsl. In Boulanger, F., Famelis, M., and Ratiu, D., editors, *MoDeVVa 2013: Workshop on Model Driven Engineering, Verification and Validation: Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation co-located with 16th International Conference on Model Driven Engineering Miami, Florida, October 1st, 2013*, CEUR Workshop Proceedings, pages 41–50. CEUR-WS.org.

Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., and Bordbar, B. (2009a). Ensuring spatio-temporal access control for real-world applications. In *Proceedings of the 14th ACM Symposium on Access Control Models and Technologies*, pages 13–22, New York, NY, USA. Association for Computing Machinery.

Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., and Bordbar, B. (2009b). Ensuring spatio-temporal access control for real-world applications. In *Proceedings of the 14th ACM Symposium on Access Control Models and Technologies*, SACMAT ’09, pages 13–22, New York, NY, USA. ACM.

Vallecillo, A. and Gogolla, M. (2017). Adding random operations to OCL. In *Proceedings of MODELS 2017 Satellite Event*, CEUR Workshop Proceedings, pages 324–328. CEUR-WS.org.

Vergu, V., Neron, P., and Visser, E. (2015). DynSem: A DSL for Dynamic Semantics Specification. In Fernández, M., editor, *26th International Conference on Rewriting Techniques and Applications (RTA 2015)*, volume 36 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 365–378. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

Voelter, M., Kolb, B., Birken, K., Tomassetti, F., Alff, P., Wiart, L., Wortmann, A., and Nordmann, A. (2019). Using language workbenches and domain-specific languages for safety-critical software development. *Softw. Syst. Model.*, 18(4):2507–2530.

Vu, L., Haxthausen, A., and Peleska, J. (2014). A domain-specific language for railway interlocking systems. *10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems*, pages 200–209.

Wachsmuth, G. (2008). Modelling the operational semantics of domain-specific modelling languages. In Lämmel, R., Visser, J., and Saraiva, J., editors, *Generative and Transformational Techniques in Software Engineering II (GTTSE)*, pages 506–520. Springer Berlin Heidelberg.

Wagelaar, D. and Straeten, R. V. D. (2006). A comparison of configuration techniques for model transformations. In *ECMDA-FA*, pages 331–345.

Wakrime, A. A., Ayed, R. B., Dutilleul, S. C., Ledru, Y., and Idani, A. (2018). Formalizing railway signaling system ERTMS/ETCS using uml/event-b. In Abdelwahed, E. H., Bella-
treche, L., Golfarelli, M., Méry, D., and Ordonez, C., editors, *8th International Conference on Model and Data Engineering - MEDI*, volume 11163 of LNCS, pages 321-330. Springer.

Warmer, J. and Kleppe, A. (1999). *The Object Constraint Language: Precise Modeling with UML*. Object Technology Series. Addison-Wesley.

Wildmoser, M. and Nipkow, T. (2004). Certifying machine code safety: Shallow versus deep embedding. In Slind, K., Bunker, A., and Gopalakrishnan, G., editors, *Theorem Proving in Higher Order Logics (TPHOLs 2004)*, volume 3223 of LNCS, pages 305-320. Springer.

Yangui, R. (2016). *Modélisation UML/B pour la validation des exigences de sécurité des règles d'exploitation ferroviaires*. PhD thesis.

Yu, L., France, R., Ray, I., and Ghosh, S. (2009). A Rigorous Approach to Uncovering Security Policy Violations in UML Designs. In *2009 14th IEEE International Conference on Engineering of Complex Computer Systems*, pages 126-135.

Yuan, C., He, Y., He, J., and Zhou, Z. (2006). A verifiable formal specification for RBAC model with constraints of separation of duty. In *Inscrypt*, pages 196-210. LCNS 4318, Springer.

Zalila, F., Crégut, X., and Pantel, M. (2013). Formal verification integration approach for dsml. In *Model-Driven Engineering Languages and Systems*, pages 336-351. Springer.

Zao, J., Wee, H., Chu, J., and Jackson, D. (2003). RBAC schema verification using lightweight formal model and constraint analysis. In *Proceedings of the 8th ACM Symposium on Access Control Models and Technologies*. ACM.

Zhang, N., Ryan, M., and Guelev, D. P. (2005). Evaluating access control policies through model checking. In *Information Security, 8th International Conference, ISC 2005, Singapore, September 20-23, 2005, Proceedings*, volume 3650 of LNCS, pages 446-460.

Zhang, N., Ryan, M., and Guelev, D. P. (2008). Synthesising verified access control systems through model checking. *Journal of Computer Security*, 16(1):1-61.
Abstract

My research works are dedicated to the integration of two well known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE). This integration is called Formal MDE (FMDE) all along the current document. In fact, several works have been already done in order to strengthen the MDE paradigm with formal reasoning, and therefore make it more viable as far as safety and security concerns have to be addressed. When taken separately, these works provide a partial coverage of MDE, but when combined they can address a wide range of models and languages. During the last decade, I investigated two directions in which the FMDE paradigm proved its value: (i) Model-Driven Security (MDS), and (ii) Domain-Specific Languages (DSLs). Under the MDE umbrella, both the MDS and DSL communities advocate for the use of models throughout the development process, providing solutions to the validation problem ('do the right system'). Nonetheless, the verification problem ('do the system right') is still a major challenge, perhaps because formal reasoning (i.e. model-checking and/or theorem proving) was not apart of the MDE initiative. To be pragmatic my contributions build on well-established notations: mainly UML and B, and — at a smaller scale — BPMN, CSP, Z and Petri-Nets. Besides, the obtained results can be inspiring and, in my opinion, should be extended with other (semi-)formal languages, which would confer to FMDE a broader spectrum. This document summarizes for every research direction (respectively MDS and DSLs) the challenges that guided my works, and give an overview of my contributions and publications in the field.