# Modeling and verifying an arrival manager using the formal Event-B method

Amel Mammar, Michael Leuschel

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

## To cite this version:

Amel Mammar, Michael Leuschel. Modeling and verifying an arrival manager using the formal Event-B method. International Journal on Software Tools for Technology Transfer, 2024. hal-04855142

HAL Id: hal-04855142

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

Submitted on 24 Dec 2024

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

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

<figure><img src="image_2.png" /></figure>
# Modeling and Verifying an Arrival Manager using EVENT-B *

Amel Mammar<fnref n="1" />, Michael Leuschel<fnref n="2" />

Received: date / Revised version: date

**Abstract.** The present paper describes an EVENT-B model of the Arrival MANager system (called AMAN), the case study provided by the ABZ'23 conference. The goal of this safety critical interactive system is to schedule the arrival times of aircraft at airports. This system includes two parts: an autonomous part which predicts the arrival time of an aircraft from external sources (flight plan information, radar and weather information, etc.) and an interface part that permits the Air Traffic Controller (ATCo) to submit requests to AMAN like changes regarding the arrival times of aircraft. To formally model and verify this critical system, we use a correct-by-construction approach with the EVENT-B formal method and its refinement process. We mainly consider functional features of the case study; all proof obligations have been discharged using the provers of the RODIN platform under which we carried out our development. To help users understand how AMAN works and its main functionalities, a visualisation of the EVENT-B models was achieved using the VISB component of PROB. Our models have been validated using PROB by checking scenarios related to different functional aspects of the system.

**Key words:** System modeling, EVENT-B method, Refinement, Verification

## 1 Introduction

In this paper, we introduce a formal model of the Arrival MANager system (called AMAN). This system has been

provided as a case study in the context of the ABZ'23 conference. The main objective of the AMAN system is to help the Air Traffic Controller (ATCo) manage the arrival of aircraft approaching the considered airport by providing it with an arrival sequence. To predict the arrival times of aircraft, AMAN uses external sources like flight plan data, radar data, weather information, etc. The process of calculating concrete arrival times itself is out of the scope of this paper, only its output is considered.

The AMAN system works in collaboration with the ATCo who can suggest some modifications on the arrival sequence to the AMAN. The ATCo can also block periods of time (for runway cleaning for instance) notifying the AMAN that these time slots are no longer available; any predicted arrival corresponding to these slots must be thus moved. The ATCo also has the possibility to put an already predicted aircraft on hold, informing the AMAN that this latter must be removed from the arrival sequence. Finally, the interface permits the ATCo to focus on specific aircraft that are predicted to land within the next minutes (between 15 and 45) by selecting a zoom level. In that case, only these related aircraft are displayed within the interface.

In [22], a first formal model of the AMAN system using the EVENT-B formal method has been presented. The current paper describes a new EVENT-B model of the same system with fewer variables and more natural expression of the requirements. The use of the EVENT-B formal method with its refinement technique permits to master the complexity of a system by gradually introducing its different elements and characteristics. Building a formal model of such a system permits to verify the expected properties including the safety ones. Our approach to model this system follows the four-variable model of Parnas and Madey [26] that distinguishes two classes of variables, environment and controller variables (see Section 2). The first class denotes

<footnote n="1">¹SAMOVAR, Télécom SudParis, Institut Polytechnique de Paris, France</footnote>

<footnote n="2">²Institut für Informatik, Universität Düsseldorf</footnote>

<footnote>Send offprint requests to: Amel Mammar, E-mail: amel.mammar@telecom-SudParis.eu</footnote>

<footnote>* This work was supported in part by the ANR projet DISCONT.</footnote>
the elements that are outside the controller and whose states are read by the sensors. The state of the environment variables are updated when the system sends commands to them through the actuators. The second class includes the inputs and the outputs of the system. To master the complexity of this system, we deal with one environment/controller variable at each refinement step.

The Event-B models have been built by the first author. Her past industrial experience in the formal specification and verification of railway interlocking systems, in collaboration with Thales and RATP, helped her in this task. The knowledge acquired during this experience has been put in practice and reinforced through the different modelling of the previous ABZ case studies [24, 20, 21, 19]. The development of the EVENT-B models took two months and has been done using the Rodin platform [12] that provides editors, provers and several other plugins for various tasks like animation and model checking with PROB [17]. Our EVENT-B model considers most of the requirements except those related to the interface appearance (See Table 1). In this paper, we used PROB in order to animate the built models with three purposes: discovering the potential scenarios (a sequence of events) that violate the invariant before going in a hard/long proof phase, validating the specification by simulating the provided scenarios in order to be sure that we have specified the right system, and constructing a visualisation of the EVENT-B models using the VISB component of PROB.

## 1.1 EVENT-B method

EVENT-B [3] is the successor of the B method [2] for developing correct discrete systems using mathematical notations. This method is well-suitable for complex systems thanks to its refinement concept that permits incrementally introducing details by starting with an abstract view of model that it is then enriched until obtaining a model that includes all the elements of the system.

An EVENT-B model includes two elements: context and machine. A context describes the static part of an EVENT-B specification; it consists of constants C and sets S (user-defined types) together with axioms A that specify their properties. The dynamic part of a system is included in a machine that defines variables V and a set of events E. The possible values that the variables hold are restricted using an invariant, denoted Inv, written using a first-order predicate on the state variables. Each event, of the form (ANY X WHEN G THEN Act END), is enabled when all the conditions G, named guards, prior to its triggering hold. When several events are enabled, only one is triggered. In this case, substitutions Act, called actions, are applied over variables. In this paper, we restrict ourselves to the becomes equal substitution, denoted by $(x := e)$.

Refinement is a process of enriching or modifying a model in order to augment the functionality being modeled, or/and explain how some purposes are achieved. Both EVENT-B elements context and machine can be refined. A context can be extended by defining new sets $S_r$ and/or constants $C_r$ together with new axioms $A_r$. A machine is refined by introducing new variables and/or replacing existing variables with new ones $V_r$ that are typed with an additional invariant $Inv_r$. New events can also be introduced to implicitly refine a skip event. In this paper, the refined events have the same form ANY $X_r$ WHEN $G_r$ THEN Act_r END. The semantics of the EVENT-B notations used in this paper is provided in Appendix B.

To ensure the correctness of the specification, proof obligations are generated for the first abstract model and for each refinement level. These proof obligations aim at proving invariant preservation by each event, but also to ensure that the guard of each refined event is stronger than that of the abstract event. These guard strengthening refinement proof obligations ensure that event parameters are properly refined. More information on proof obligations can be found in [3]. Basically:

1. For each event, we have to establish that its triggering maintains the invariant, that is:

$$ \forall S, C, X. (A \wedge G \wedge Inv \wedge BA_{Act} \Rightarrow Inv') $$

where $BA_{Act}$ is the before-after predicate of the actions of an event and $Inv'$ is the invariant applied to the after values.

2. To prove that a refinement is correct, we have to establish the following two proof obligations:

- **guard strengthening**: the guard of the refined event should be stronger than the guard of the abstract one:

$$ \forall (S, C, S_r, C_r, V, V_r, X, X_r). (A \wedge A_r \wedge Inv \wedge Inv_r \Rightarrow (G_r \Rightarrow G)) $$

- **Simulation**: the effect of the refined action should be stronger than the effect of the abstract one:

$$ \forall (S, C, S_r, C_r, V, V_r, X, X_r). (A \wedge A_r \wedge Inv \wedge Inv_r \wedge G_r \wedge BA_{Act_r} \Rightarrow BA_{Act} \wedge Inv_r') $$

- **Convergence**: convergence of new events is optional and has not been used in this case study because it was not necessary, new events being allowed to loop forever, according to the requirements.

To discharge the proof obligations, we used the automatic provers integrated to the RODIN platform<fnref n="1" /> and also the external SMT [14] and Atelier B [11] provers that we have imported as plugins to RODIN. The RODIN platform also offers a theory component that allows us to extend the mathematical concepts of EVENT-B by defining user-types and their associated operators [7]. The use

<footnote n="1">¹ http://www.event-b.org/install.html</footnote>
of the theory component also permits to cope with the
complexity of a system by importing and reusing exist-
ing theories.

1.2 *The PROB model checker*

In this paper, we used the animator and model checker
PROB [18] for validating our models in order to ensure
that they are error-free and their behaviors correspond
to the expected ones.

PROB<fnref n="2" /> has been developed over twenty years and
contains a model checker for verifying LTL (Linear Tem-
poral Logic) [27] and CTL (Computational Tree Logic)
[10] properties. The core of PROB is written in Prolog;
its purpose is to be a comprehensive tool in the area of
formal verification methods. Its main functionalities can
be summarized as follows.

1. PROB permits to exhibit scenarios (a sequence of events) that, starting from a valid initial state of the system, reach a state that violates its invariant.

2. PROB allows the animation of the B/EVENT-B models, that is, the user can simulate different scenarios from a given starting state that satisfies the invariant. Via its graphical user interface, the animator provides the user with: (i) the current state, (ii) the history of the event triggering that has led to the current state and (iii) a list of all the enabled events, along with proper parameters instantiations. In this way, the user does not have to guess the right values for the event parameters.

3. PROB allows to detect absolute/relative deadlocks,

4. PROB provides many features to visualise an individual state or the entire state space.

1.3 Contributions

The contributions of this paper with respect to [22] are
as follows:

- a more detailed description of the modeling strategy used (see Section 2);

- A new EVENT-B model which defines fewer variables and more natural expression of the different invariants. In this model, we timestamp each variable with the current time (see Section 3);

- additional examples and explanations about the ver-
  ification phase using model-checking and scenarios
  (see Section 4.3);

- more details about the development of the visualisa-
  tion (see Section 4.4);

- a comparison with similar solutions using different approaches/formal languages (see Section 5).

1.4 The structure of the paper

The rest of this paper is structured as follows. Section 2 presents our modelling strategy. Then, Section 3 describes our model in more details. The validation and verification of our model are discussed in Section 4 along with a visualisation of the model using the VISB component of PROB. Section 5 compares our specification with similar specifications that use different languages/approaches. Finally, Section 6 concludes the paper.

2 Requirements and modeling strategy

This section presents the principles of control systems
and an overview of the EVENT-B architecture corre-
sponding to the modeling of the AMAN system.

## 2.1 Control abstraction

In this paper, we use the concepts described by Parnas
and Madey in [26]. The AMAN system can be consid-
ered as a control system that reads information from the
environment elements (e.g., the desired arrival time of an
aircraft, radar information) using sensors and uses a set
of actuators to transmit the adequate orders to these el-
ements (see Figure 1). A sensor measures the value of
an environment element *m*, called a *monitored* variable
(e.g., the desired arrival time of an aircraft, radar in-
formation), and provides this measure (e.g., the desired
hour/minute) to the software controller as an *input* vari-
able *i*.

The objective of the commands, called *output* variable *o* and sent to the actuators, is to modify the value of some characteristics of the environment, called a *controlled* variable *c*. Variables *m* and *c* are called *environment variables*. Variables *i* and *o* are called *controller variables*. Finally, a controller has its own internal state variables to perform computations. In this case study, we use EVENT-B state variables to represent both environment and controller variables. We model neither sensor/actuator failures nor their delays.

A well-known architecture of a control system is a
control loop that reads all input variables at once, at a
given moment, and then computes all output variables in
the same iteration. But, it can be also viewed as a contin-
uous system that can be interrupted by any change in the
environment represented by a new value sent by a sen-
sor. In this paper, we adopt a hybrid view: every 10 sec-
onds, the AMAN reads various sensor inputs and makes
a new prediction to display. Moreover, the AMAN in-
stantaneously reacts to some ATCo's requests by up-
dating the display. The use of the four-variable model
permits to cope with the complexity of such systems
and define a generic methodology for modeling them us-
ing EVENT-B. This methodology consists in defining a

<footnote n="2">² https://prob.hhu.de/</footnote>
separate event for each input received by the system or output sent towards the environment. Therefore, modelling the AMAN with EVENT-B consists in defining one event for each input corresponding to the ATCo's interaction with its environment and an additional event display representing the output of the system, that is, calculating and displaying a new prediction performed by the AMAN.

## 2.2 Modeling structure

The EVENT-B specification presented in this paper is incrementally built using refinement. It is composed of seven levels (seven machines and two contexts) and defines and uses a theory to deal with, among others, sequences, the absolute value, etc. (see Figure 2).

- Context C1 mainly defines the following constants: Labels to represent the aircraft, Hours, Minutes and Seconds to denote the possible values of these time units, zoomLevels representing the possible values for the zoom level.

- Machine M1 sees the context C1 and defines, among others, an event for determining and displaying the arrival times of aircraft and an event for selecting the zoom level.

- Machine M2 models the holding of an aircraft. This machine sees the context C1.

- Machines M3 and M4 respectively introduce the moving of a scheduled aircraft to change its arrival time and the blocking of time slots by the ATCo. Both machines M3 and M4 see the context C1.

- Machine M5 represents the request of an aircraft for landing. It sees the context C1. In each of the machines (M1-M5), we model the historical functions that permit the AMAN to provide the ATCo with the previous predictions.

- Machine M6 models the interaction between the ATCo and the AMAN using the mouse. This machine sees the context C2 that defines some constants to describe a mouse in terms of its possible states (, released) and also the different elements on which a mouse may click.

- Machine M7 specifies the AMAN breakdown for failure for instance. It sees the context C2.

Roughly speaking, the structure of the EVENT-B specification is constructed as follows: the outputs (AMAN's functionalities, that are, the prediction and display of the arrival times) are modeled first in the machine M1, then the ATCo's interactions are modelled in a second step (Machines M2-M6). Finally, the last level M7 models the failure of the AMAN.

## 2.3 Formalisation of the requirements and tasks

Table 1 shows where and how the requirements, listed in [25] and summarized in Appendix A, are specified in

our EVENT-B models. As one can remark, depending on the kind of the requirement, this later is specified as an invariant, a guard, an elementary variable (like the variable mouseState), an event with specific guards, etc. Requirements Req22 and Req23 for instance cannot be easily expressed as an invariant since it would require to introduce at least three additional variables: (i) a variable mouseStateP to store the previous state of the mouse, (ii) a variable mousePositionP to store the previous position of the mouse and (iii) a variable isEnabled to know whether the hold button is enabled or not. In that case, the invariant would be expressed as follows:

$$ 
\begin{align*}
& \text{mouseStateP=clicked} \land \text{mousePositionP=hold} \\
& \text{mouseState=released} \land \text{mousePosition=hold} \\
\Rightarrow \quad & \text{isEnabled} = \text{TRUE}
\end{align*}
$$

We did not choose this option because these additional variables make the specification more complex; we have to manage their updates by each event. Finally, let us note that some requirements (Requirements Req17-18 and Req20) are not covered because they are related to the interface appearance and not to the system functionalities. Indeed, the EVENT-B method is dedicated to specifying the state of a system and its evolution and not to describing the visual appearance of its components. In addition to the requirements listed in Table 1, we have specified some additional properties that we consider of good sense. For instance, we have specified that the requests are dealt with according to the FIFO strategy (First In First Out) to ensure fairness. More details are given in the next section.

Table 2 shows the correspondence between the ATCo's actions/AMAN tasks and the events of the built specification.

# 3 Description of the EVENT-B Models

In this section, we give a brief description of some key refinement levels of the EVENT-B modeling of the AMAN. The complete archive of the EVENT-B project is available in [23]. Our modeling makes the assumption that the AMAN predictions are done for a single day, that is, no aircraft is planned for the next day.

## 3.1 Machine M1

Machine M1 models the prediction of the arrival times of aircraft (called labels in the rest of the paper) and its display on the screen. This machine sees the context C1 that defines: the set of all possible objects of the system (Elements), the set of possible labels (Labels), the units of time (Seconds, Minutes and Hours), the zoom levels (zoomLevels), the time progression step (step) and the security distance between two distinct labels (sep):
<figure><img src="image_3.png" /><figcaption>Fig. 1. Four-variable model</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 2. EVENT-B structure of the project</figcaption></figure>

<table><caption>Table 1. Cross-reference between the components of our model and the requirements of [25]</caption><thead><tr><th>Requirements</th><th>Components</th><th>EVENT-B element</th></tr></thead><tbody><tr><td>Req1</td><td>Machine M5</td><td>Invariant inv1</td></tr><tr><td>Req2</td><td>Machine M2</td><td>Invariant inv1</td></tr><tr><td>Req3</td><td>Machine M3</td><td>Invariant inv6</td></tr><tr><td>Req4</td><td>Machine M2</td><td>Event removeLabel</td></tr><tr><td>Req5</td><td>Machines M1 and M3</td><td>Invariants inv10(M1) and inv5(M3)</td></tr><tr><td>Req6</td><td>Machine M4</td><td>Invariants inv1 and inv2</td></tr><tr><td>Req7</td><td>Machine M3</td><td>Invariant inv6</td></tr><tr><td>Req8</td><td>Machine M7</td><td>At any moment, the Boolean Variable isStopped can be updated by the event stopStart. All other events are guarded by (isStopped=FALSE)</td></tr><tr><td>Req9<br>to<br>Req13</td><td>Machines M1-M6</td><td>HTimed variables V_T</td></tr><tr><td>Req14</td><td></td><td>Not covered</td></tr><tr><td>Req15</td><td>Machine M6</td><td>Event holdLabel is enabled only if a label is selected (guard grd2)</td></tr><tr><td>Req16</td><td>Context C1</td><td>Axiom axm6</td></tr><tr><td>Req17<br>Req18</td><td></td><td>Not covered</td></tr><tr><td>Req19</td><td>Machine M1</td><td>Invariant inv12</td></tr><tr><td>Req20</td><td></td><td>Not covered</td></tr><tr><td>Req21</td><td>Machine M6</td><td>Variable mouseState</td></tr><tr><td>Req22<br>Req23</td><td>Machine M6</td><td>Guard grd4 of the event holdLabel</td></tr></tbody></table>
<table><caption>**Table 2.** Cross-reference between the components of our model and the ATCo's actions/AMAN tasks of [25]</caption><thead><tr><th>Tasks</th><th>Components</th><th>EVENT-B element</th></tr></thead><tbody><tr><td>Compute/Display LS</td><td>M1</td><td>Event Display</td></tr><tr><td>Change zoom</td><td>M1</td><td>Event selectZoom</td></tr><tr><td>Put Aircraft on hold</td><td>M2</td><td>Events holdLabel and removeholdLabel</td></tr><tr><td>Change LS</td><td>M3</td><td>Event moveLabel</td></tr><tr><td>Block time slot</td><td>M4</td><td>Events addBlockedZone and deleteBlockedZone</td></tr><tr><td>Stop Manage LS</td><td>M7</td><td>Event stopStart</td></tr></tbody></table>

**SETS** *Elements*

**CONSTANTS** *Labels, Seconds, Minutes, Hours, zoomLevels, step, sep*

**AXIOMS**

axm1: finite(Elements) ∧ Labels ⊆ Elements

axm2: Seconds = 0..59 ∧ Minutes = 0..59 ∧ Hours = 0..23

axm3: zoomLevels ⊆ N1 ∧ zoomLevels ≠ ∅

axm4: step ∈ N1 ∧ sep ∈ N1

The machine M1 defines the following invariants to characterise the possible arrival times of a set of labels where `curTimeMin` (resp. `curTimeSec`) gives the time in terms of minutes (resp. seconds):

inv1 labels_T ∈ (∪ k. k̄ ∈ N ∧ step × k ≤ curTimeSec(curTimeS, curTimeM, curTimeH) | step × k) → P(Labels)

inv2 arrivalM_T ∈ (∪ k. k ∈ N ∧ step × k ≤ curTimeSec(curTimeS, curTimeM, curTimeH) | step × k) → (Labels → Minutes)

inv3 arrivalH_T ∈ dom(arrivalM_T) → (Labels → Hours)

inv4 ∀ t. t ∈ dom(arrivalM_T)

$$ \Rightarrow \quad \begin{aligned} & \ dom(arrivalM_T(t)) \subseteq \ labels\ T(t) \\ & \ inv5: \ \forall t, l. t \in \ dom(arrivalM_T) \land l \in \ dom(arrivalM_T(t)) \end{aligned} $$

⇒ curTimeMin((arrivalM_T(t))(l), (arrivalH_T(t))(l)) ≥ t ÷ 60

inv6: ∀ t, l1, l2. t ∈ dom arrivalH_T) ∧ l1 ∈ dom (arrivalM_T(t)) ∧ l2 ∈ dom (arrivalM_T(t)) ∧ l1 ≠ l2

$$ \Rightarrow \quad \begin{aligned} & \ abs(curTimeMin((arrivalM_T(t))(l1), (arrivalH_T(t))(l1)), \\ & \ curTimeMin((arrivalM_T(t))(l2), (arrivalH_T(t))(l2))) \geq sep \end{aligned} $$

inv7: zoomLevel ∈ zoomLevels ∧ displayedLabels ⊆ dom(arrivalM_T(t))

inv8: displayedLabels = (∪ l. l ∈ dom (arrivalM_T(t)) ∧ curTimeMin((arrivalM_T(t))(l), (arrivalH_T(t))(l)) ≤ curTimeMin(curTimeM, curTimeH) + zoomLevel | {l})

Invariant `inv1` defines the set of existing labels at each moment. Invariants `inv2`, `inv3` and `inv4` describe the arrival times of a set of labels. Invariant `inv5` states that the arrival time of an aircraft is later than the current time while `inv6` ensures the security of passengers by separating the labels by at least `sep` minutes. Finally, the invariants `inv7` and `inv8` specify the set of labels displayed on the screen according to their arrival times and the selected zoom `zoomLevel`. Variable `zoomLevel` is an integer (between 15 and 45) that defines the display window of the labels: a label is displayed if its arrival time falls into this window (`inv8`). We have chosen to model the zoom functionality and the calculation of the label arrival times at the same level because both modify the variable `displayedLabels`. As stated in Section 1.1, all events modifying a variable must be specified

in the same machine where the variable is defined. Another option would be to define the variables *displayedLabels* and *zoomLevel* in an other refinement level. We did not choose this option because it adds a refinement level while including them in M1 does not add any complexity.

Machine M1 defines the event *display* as follows:

Event display ≅
any
where

* t, landingLabs, labsToDisp, labsSch, arr, ns, nm, nh
* grd1: t=curTimeSec(curTimeS, curTimeM, curTimeH) +step
* grd2: landingLabs=(∪ l. l ∈ dom (arrivalM_T(t-step)) ∧ curTimeMin(nm, nh))>
* curTimeMin((arrivalM_T(t-step))(l), (arrivalM_T(t-step))(l)) | {l})
* grd3: labsSch ⊆ labels_T(t-step) \ landingLabs
* grd4: arr ∈ labsSch → curTime(nm, nh)..curTime(nm, nh)+180
* grd5: ∀ l1, l2. l1 ∈ dom (arr) ∧ l2 ∈ dom (arr) ∧ l1 ≠ l2 ⇒ abs (arr(l1), arr(l2)) ≥ sep
* grd6: toDisp=(∪ l. l ∈ dom (arr) ∧ arr(l) ≤ curTimeMin(nm, nh) + zoomLevel | {l})
* grd7: ...

then

* act1: displayedLabels:=toDisp
* act2: arrivalM_T(t) := (λ l. l ∈ dom (arr) | arr(l) mod 60)
* act3: arrivalH_T(t) := (λ l. l ∈ dom (arr) | arr(l) ÷ 60)
* act4: curTimeS := ns
* act5: curTimeM := nm
* act6: curTimeH := nh
* act7: labels_T(t) := labels_T(t-step)

end

where `ns` (resp. `nm, mh`) denotes the second (resp. minute, hour) unit of the current time plus 10 seconds. Roughly speaking, this event starts by calculating the set of labels that have already landed (Guard `grd2`), then it makes a prediction for a subset `labsSch` of other existing labels (Guards `grd3` and `grd4`) by ensuring that the labels are separated by at least `sep` minutes (Guard `grd5`). Finally, it calculates the set of the labels to display according to their arrival times and the selected zoom level (Guard `grd6`). Actions update different variables by stamping them with the current time `t`.

Let us remark that the guard `grd4` specifies that the predictions are made for the next 3 hours. We put this hypothesis in order to improve the PROB performance and make the animation of the models possible. Accord-
ing to the case study authors, such an assumption is very
reasonable and is not a limitation of the model.

## 3.2 Machine M2

Machine M2 models labels put on hold. For that purpose, the following invariants are defined. Invariant `inv1` types the introduced variable `holdLabels_T`. Invariant `inv2` states that a label made on hold must be removed from the arrival sequence of the next cycle (`x+step`).

$$
\begin{align*}
\text{inv1: } \text{holdLabels}_T &\in (\bigcup k. k \in \mathbb{N} \wedge \text{step} \times k \le \text{curTimeSec}(\text{curTimeS}, \text{curTimeM}, \text{curTimeH}) \mid \text{step} \times k) \rightarrow \mathbb{P}(\text{Labels}) \\
\text{inv2: } \forall x. x \in \text{dom}(\text{holdLabels}_T) \wedge & \\
& x + \text{step} \in \text{dom}(\text{arrivalM}_T) \\
& \Rightarrow \text{holdLabels}_T(x) \cap \text{dom}(\text{arrivalM}_T(x + \text{step})) = \emptyset
\end{align*}
$$

$$
\begin{align*}
\text{inv2: } \forall x. x \in \mathbf{dom}(\mathbf{holdLabels}_T) \wedge \\
& x + \text{step} \in \mathbf{dom}(\mathbf{arrivalM}_T) \\
& \Rightarrow \\
& \mathbf{holdLabels}_T(x) \cap \mathbf{dom}(\mathbf{arrivalM}_T(x + \text{step})) = \emptyset
\end{align*}
$$

Machine M2 defines an event holdLabel that permits to put on hold a displayed label *l* by adding it to hold-Labels.

$$
\begin{array}{l}
\text{Event } \text{holdLabel} \triangleq \\
\quad \text{any} \\
\quad \text{where} \\
\quad \text{grd1: } t=\text{curTimeSec}(\text{curTimeS},\text{curTimeM},\text{curTimeH})
\end{array}
$$

$$
\begin{array}{l}
\text{grd2: } l \in \mathbf{dom}(\mathbf{arrivalM}_T(t)) \setminus \mathbf{holdLabels}_T(t) \\
\text{then} \\
\quad \text{act1: } \mathbf{holdLabels}_T(t) := \mathbf{holdLabels}_T(t) \cup \{l\} \\
\text{end}
\end{array}
$$

The event display is refined by adding the guard (`lab-sSch` ∩ `holdLabels_T(t-step)=Ø`) in order to maintain the invariant `inv2` by removing the held labels from the arrival sequence.

## 3.3 Machine M3

Machine M3 models the request of the ATCo that would
like to change the arrival time of a label by defining the
following invariants. Invariants `inv1` and `inv2` define the
new arrival times of a given label. Invariant `inv3` states
that only scheduled labels, which are not put on hold,
can be moved and new arrival times are suggested by the
ATCo. Invariant `inv4` models the requirement **Req5** to
avoid overlapping labels.

$$
\begin{align*}
\text{inv1: } \mathit{newArrivalM_T} \in & (\bigcup k. k \in \mathbb{N} \wedge \mathit{step} \times k \le \mathit{curTimeSec}(\mathit{curTimeS}, \mathit{curTimeM}, \mathit{curTimeH}) \mid \mathit{step} \times k) \rightarrow (\mathit{Labels} \rightarrow \mathit{Minutes}) \\
\text{inv2: } \mathit{newArrivalM_T} \in \mathbf{dom}(\mathit{newArrivalM_T}) \rightarrow & (\mathit{Labels} \rightarrow \mathit{Hours})
\end{align*}
$$

$$
\begin{array}{l}
\text{inv2: } \mathit{newArrivalM_T} \in \mathbf{dom}(\mathit{newArrivalM_T}) \rightarrow \\
\quad (\mathit{Labels} \leftrightarrow \mathit{Hours})
\end{array}
$$

$$
\begin{align*}
\text{inv3: } \forall x. x \in \mathbf{dom}(\mathbf{newArrivalM_T}) & \\
& \Rightarrow \\
& \mathbf{dom}(\mathbf{newArrivalM_T}(x)) \subseteq \\
& \phantom{\mathbf{dom}(} \mathbf{sdom}(\mathbf{arrivalM_T}(x)) \setminus \mathbf{holdLabels_T}(x)
\end{align*}
$$

$$
\begin{align*}
\text{inv4: } \forall t, x, y. t \in \mathbf{dom}(\mathbf{newArrivalM_T}) \wedge \\
& x \in \mathbf{dom}(\mathbf{newArrivalM_T}(\bar{t})) \wedge \\
& y \in \mathbf{dom}(\mathbf{newArrivalM_T}(t)) \wedge \\
& x \neq y \\
& \Rightarrow \\
& (\mathbf{newArrivalM_T}(t) \otimes \mathbf{newArrivalH_T}(t))(x) \\
& \quad \neq \\
& (\mathbf{newArrivalM_T}(t) \otimes \mathbf{newArrivalH_T}(t))(y)
\end{align*}
$$

As stated in the requirement document, a moving re-
quest might be rejected by the AMAN if it would re-
quire a speed-up of the aircraft beyond the capacity of
the aircraft. To model such a requirement, we added the
following guards to the event display that specify that the
labels that cannot be moved must keep their original ar-
rival times (guard `grd2`), whereas others are moved to the
new ones (guard `grd3`). Guard `grd4` permits to cover the
requirement **Req7** by stating that the labels that ask
for delaying its arrival time should be satisfied. Func-
tion `canBeMoved` permits to abstract from the details
and calculations made by the AMAN to decide whether
a label can be moved or not. Such details can be intro-
duced later by refining this function. As the requirement
document does not give enough information about this
point, we kept the function `canBeMoved` in its abstract
form.

$$
\begin{align*}
\text{grd1: } & \text{canBeMoved} \in \\
& \mathbf{dom}(\mathit{newArrivalM_T}(t - \text{step})) \setminus \mathit{landingLabs} \rightarrow \mathbf{BOOL}
\end{align*}
$$

$$
\begin{align*}
\text{grd2: } & \text{canBeMoved}^{-1}[\{\mathbf{TRUE}\}] \triangleleft \text{arr} = \\
& (\lambda x. x \in \text{canBeMoved}^{-1}[\{\mathbf{TRUE}\}] \mid \\
& \qquad \text{curTimeMin}((\text{newArrivalM_T}(t - \text{step}))(x), \\
& \qquad (\text{newArrivalH_T}(t - \text{step}))(x)))
\end{align*}
$$

$$
\begin{align*}
\text{grd3: } & \text{canBeMoved}^{-1}[\{\mathbf{FALSE}\}] \triangleleft \text{arr} = \\
& (\lambda x. x \in \text{canBeMoved}^{-1}[\{\mathbf{FALSE}\}] \mid \\
& \qquad \text{curTimeMin}((\text{newArrivalM_T}(t - \text{step}))(x), \\
& \qquad (\text{newArrivalH_T}(t - \text{step}))(x)))
\end{align*}
$$

$$
\begin{align*}
\text{grd4: } & (\bigcup x. x \in \mathbf{dom}((\mathit{newArrivalM_T}(t - \mathit{step}))) \setminus \mathit{landingLabs} \\
& \wedge \\
& \phantom{\bigcup} \mathit{curTimeMin}((\mathit{newArrivalM_T}(t - \mathit{step}))(x), \\
& \phantom{\bigcup} \quad ((\mathit{newArrivalH_T}(t - \mathit{step}))(x))) \\
& > \\
& \phantom{\bigcup} \mathit{curTimeMin}((\mathit{newArrivalM_T}(t - \mathit{step}))(x), \\
& \phantom{\bigcup} \quad (\mathit{newArrivalH_T}(t - \mathit{step}))(x)))|\{x\} \\
& \subseteq \\
& \mathit{canBeMoved}^{-1}[\{\mathbf{TRUE}\}]
\end{align*}
$$

Machine M3 is refined by the machine M4 to model the
blocked slots. As its EVENT-B modeling is very similar
to that of held labels, this paper does not give more
details about the machine M4.

## 3.4 Machine M5

The machine M5 models the flights approaching an airport as an injective sequence of requests submitted to the AMAN (Invariants `inv1` and `inv2`). For that purpose, we have specified a theory to define the sequence data structure along with its associated operations like inserting/deleting elements.

$$
\begin{align*}
\text{inv1: } \text{requests}_T & \in \\
& (\bigcup k. k \in \mathbb{N} \wedge \text{step} \times k \le \text{curTimeSec}(\text{curTimeS}, \\
& \qquad \text{curTimeM}, \text{curTimeH}) \mid \text{step} \times k) \rightarrow \text{seq}(\text{Labels})
\end{align*}
$$

$$
\begin{align*}
\text{inv2: } \forall t, x, y. t \in \mathbf{dom}(\text{requests}_T) \wedge x \in \mathbf{dom}(\text{requests}_T(t)) \wedge \\
& y \in \mathbf{dom}(\text{requests}_T(t)) \wedge x \neq y \\
& \Rightarrow \\
& (\text{requests}_T(t))(x) \neq (\text{requests}_T(t))(y)
\end{align*}
$$

Moreover, to ensure that the requests are fairly pro-
cessed, that is, the label that made a request in first will
get an arrival time earlier than others (FIFO strategy),
we have defined the following invariant:
$$
\begin{align*}
\text{inv3:} \quad & \forall t, l1, l2 \cdot t \in \mathbf{dom}(\text{requests}_T) \wedge \\
& t + \text{step} \in \mathbf{dom}(\text{arrivalM}_T) \wedge l1 \in \mathbf{ran}(\text{requests}_T(t)) \wedge \\
& l2 \in \mathbf{ran}(\text{requests}_T(t)) \wedge \\
& (\text{requests}_T(t))^{-1}(l1) < (\text{requests}_T(t))^{-1}(l2) \\
& \Rightarrow \\
& \quad \text{curTimeMin}((\text{arrivalM}_T(t+\text{step}))(l1), \\
& \quad \quad (\text{arrivalH}_T(t+\text{step}))(l1)) \\
& < \\
& \quad \text{curTimeMin}((\text{arrivalM}_T(t+\text{step}))(l2), \\
& \quad \quad (\text{arrivalH}_T(t+\text{step}))(l2))
\end{align*}
$$

Machine M5 also defines an event to add/delete requests. Moreover, we have added the following guards to the event **display**: the guard `grd1` states that the AMAN should predict arrival times for the labels having made requests and the already scheduled labels that are not made on hold or landed. The guard `grd2` specifies the FIFO strategy for request processing.

$$
\begin{align*}
\text{grd1:} \quad & \text{labsSch} = (\text{ran}(\text{requests}_T(t - \text{step})) \cup \\
& \qquad \mathbf{dom}(\text{arrivalM}_T(t - \text{step}))) \setminus \\
& \qquad (\text{landingLabs} \cup \text{holdLabels}_T(t - \text{step}))
\end{align*}
$$

$$
\begin{align*}
\text{grd2:} \quad & \forall x, y. \ x \in \mathbf{dom}(\text{requests}_T(t - \text{step})) \wedge \\
& \qquad y \in \mathbf{dom}(\text{requests}_T(t - \text{step})) \wedge x > y \\
& \Rightarrow \\
& \quad \begin{align*}
& \text{arr}((\text{requests}_T(t - \text{step}))(x)) > \\
& \quad \text{arr}((\text{requests}_T(t - \text{step}))(y))
\end{align*}
\end{align*}
$$

3.5 Machine M6

This machine models the interactions of the ATCo with
the AMAN using the mouse. Context C1 is extended
by the context C2 that defines the set Elements as a
partition of Labels, the button hold, the slide-bar zoom
for changing the zoom and nothing to model the mouse
that clicks on any other zone of the interface. A set rep-
resenting the possible states of the mouse is also defined:

ax1: partition (mouseStates, {released}, {clicked})

ax2: partition (Elements, Labels, {nothing}, {hold}, {zoom})

In the machine M6, we introduced two additional vari-
ables clickedElement and selectedElement to respectively
denote the element the mouse clicks on or selects. Both
variables belong to ((displayedLabels ∪ {nothing, hold,
zoom}) \ holdLabels). We also describe a set of events
to model the behavior of the mouse like clicking on or
selecting an element. Event holdLabel is refined by:

Event holdLabel $\equiv$
refines holdLabel
where
grd1: selectedElement $\in$ domarrivalM T(t)
\ holdLabels T(t)
grd2: selectedElement $\notin$ domnewArrivalM T(t)
grd3: mousePosition=hold $\wedge$ mouseState=clicked
with
1: l =selectedElement
then
act1: holdLabels T(t) := holdLabels T(t) $\cup$
{selectedElement}
act2: selectedElement := nothing
act3: clickedElement := nothing
act4: mouseState := released
end

The refinement of the event holdLabel states that the
label *l* to hold denotes the label selected by the mouse
(the *with* clause). To put the selected label on hold, the
guard *grd3* specifies that the mouse must be in the state
clicked and positioned on the hold button.

4 Validation and Verification

To verify the correctness of our models and ensure that
we built the right system, we have performed the four
steps detailed hereafter.

4.1 Model checking of the specification

As one can remark, some refinement levels contain invariants that depend on several variables. In that case, it becomes quite difficult to find the right specification (guards/actions) the first time. The PROB model checker has proven very useful in finding actions/guards to add to some events in order to establish these invariants. Basically, before performing the proof that may be tedious, we used the PROB model checker to exhibit some possible scenarios that violate the invariant. A scenario is a sequence of events that, starting from a valid initial state of the machine, leads to a state that violates the related invariant. Analysing such scenarios helps us correct the specification by adding guards/actions to some events but also sometimes to revise the invariants. For this particular case study, the use of PROB helped us particularly to find the following elements:

- the definition of the term (∪ k. k ∈ N ∧ step × k ≤ curTimeSec(curTimeS, curTimeM, curTimeH) | step × k) used to type the historical variables: inv1 of the machine M1 for instance,

- the action act7 on the variable labels<sub>T</sub>(t) in order to maintain the history of the existing labels;

- the guards `grd2-grd4` added to the event `disply` in the machine M3.

4.2 Proof of the specification

Even if PROB does not find any scenario that violates
the invariant, this does not mean that the models are
correct. Indeed, by default PROB limits the number of
explored parameter values per event. Some of the events
like addRequest have a very large number of possible
valuations of the parameters, which prevents the model
checker from exploring the full state space and explor-
ing certain scenarios. It is, however, possible in the an-
imator interface of PROB to provide explicit values for
the event parameters and thus check given scenarios by
trace replay. Still, proof is indispensable for exhaustive
verification. Proof in Event-B aims at verifying that each
event does preserve the invariant and that the guard of
each refined event is stronger than that of the abstract
<table><thead><tr><th>Element Name</th><th>Tot.</th><th>Aut.</th><th>Man.</th><th>Rev.</th><th>Und.</th></tr></thead><tbody><tr><td>STTT_AMAN</td><td>329</td><td>178</td><td>151</td><td>0</td><td>0</td></tr><tr><td>C1</td><td>12</td><td>8</td><td>4</td><td>0</td><td>0</td></tr><tr><td>C2</td><td>1</td><td>1</td><td>0</td><td>0</td><td>0</td></tr><tr><td>C3</td><td>1</td><td>1</td><td>0</td><td>0</td><td>0</td></tr><tr><td>M1</td><td>74</td><td>44</td><td>30</td><td>0</td><td>0</td></tr><tr><td>M2</td><td>29</td><td>18</td><td>11</td><td>0</td><td>0</td></tr><tr><td>M3</td><td>53</td><td>25</td><td>28</td><td>0</td><td>0</td></tr><tr><td>M4</td><td>46</td><td>22</td><td>24</td><td>0</td><td>0</td></tr><tr><td>M5</td><td>60</td><td>25</td><td>35</td><td>0</td><td>0</td></tr><tr><td>M6</td><td>53</td><td>34</td><td>19</td><td>0</td><td>0</td></tr><tr><td>M7</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td></tr><tr><td>M8</td><td>0</td><td>0</td><td>0</td><td>0</td><td>0</td></tr></tbody></table>

Tot.: Total; Aut.: Automatic; Man.: Manual; Rev.: Reviewed; Und.: Undischarged.

<caption>Fig. 3. RODIN proof statistics of the case study</caption>

one. The corresponding proof obligations are automatically generated by RODIN. Figure 3 provides the proof statistics of the case study: 329 proof obligations have been generated, of which 54% (178) were automatically proved by the various provers<fnref n="3" />. The interactive proof of the remaining proof obligations (manual ones) took about one week since they are more complex (in particular those that depend on the historical variables) and require several inference steps and need the use of external provers (like the Mono Lemma prover, Dis-prove with PROB and STM provers). During an interactive proof, users ask the internal prover to follow specific steps to discharge a proof obligation. A step proof consists in applying a deductive rule, adding a new hypothesis that is in turn proved or calling external provers. The external Mono Lemma prover has been very useful for arithmetic formulas, even if we had to add the following theorem on the modular operator:

$$ \forall x, y. x \in \mathbb{N} \land y \in \mathbb{N} \Rightarrow x = x \mod y + x \div y \times y $$

It is worth noting that performing interactive proofs does not decrease the confidence of the models since the proofs are discharged under the RODIN platform by enriching the prover only by theorems that are proved as well.

## 4.3 Validation with scenarios

Defining and simulating scenarios enables us to validate whether we have built models that behave as expected. Unfortunately, the requirement document does not provide scenarios that would help us in such a task. Therefore, we have defined our own scenarios based on our understanding of the system. Basically, we have defined

a validation scenario for each AMAN functionality and ATCo interaction. From a practical point of view, for each invariant modeling a property, we define a scenario to check whether the built models fulfill the related property. Using the animation capability of PROB, we have checked, among others, the following behaviours:

- moving a label $l_1$ to a slot that does not respect the 3 minutes separation with an other label $l_2$: in that case, the AMAN also moves $l_2$ and its neighbours to maintain this security requirement (Invariant inv6 of the machine M1).

- putting a label on hold results in removing it from the landing sequence: such an effect is not instantaneous; it is performed by the AMAN in the next processing cycle (Invariant inv2 of the machine M2).

- blocking a slot time results in moving all the labels scheduled in this slot into other available slots.

- the landing requests received by the AMAN are dealt with according to the FIFO strategy. Moreover, the corresponding labels are scheduled after the already scheduled ones (Invariant inv3 of the machine M5).

- selecting a zoom level does display only the labels that are scheduled in the corresponding slot (next (current time + zoom) minutes). Contrary to the previous scenarios, the effect of this ATCo action is instantaneous (Invariant inv8 of the machine M1).

## 4.4 Validation with Visualisation

We used visualisation to better debug counter examples and scenarios, but also during interactive animation. Our visualisation of the model was achieved using the VisB [30] component of PROB. The visualisation uses a SVG graphics file and a JSON glue file. The latter contains a mapping between the B model and the graphics file, and can add, show, hide, move and alter elements from the SVG file.

To develop our visualisation we built on the VisB files developed for another Event-B model [15] of the AMAN case study. Even though this Event-B model was developed independently and has a quite different structure (cf. Section 5 below), we managed to reuse the SVG file and adapt the JSON glue file. This was possible thanks to several extensions to the VisB JSON glue file format, not available in the first version [30]: e.g., allowing to add objects to the SVG file or allowing to provide local definitions visible within VisB expressions (in addition to variables and constants coming from the model). Here we describe the core contents of our VisB JSON glue file:

- a pointer to the SVG file. In our case this is the SVG file developed for [15]. This SVG file contains many objects visible in Fig 4, such as the rectangle bt_hold or the text field tx_hold:

```
<rect id="bt_hold" fill="black"
```

<footnote n="3">³ The theory gives 24 additional proof obligations, of which 23 have been interactively proved. Unfortunately, RODIN does not include the proof obligations related to theories in the statistics of the project.</footnote>
```
visibility="visible" width="120"
height="30" x="650" y="500"/>
<text id="tx_hold" stroke="red"
fill="red" visibility="true"
x="688" y="520">HOLD</text>
```

- a list of additional SVG objects added to the ones in the SVG file. In our case, we added a text field to display the status of the mouse.

- a list of local definitions. For example, the definitions header contains this entry, mimicking the set of known and visible planes as well as a boolean variable from [15]:

```json
"definitions": [
  {
    "name":"known planes",
    "value": "labels"
  },
  {
    "name":"visible planes",
    "value": "displayedLabels"
  },
  {
    "name": "no.airplane_is selected",
    "value": "bool (selectedElement = nothing)"
  },
```

Other defined the Airplanes constant in [15], deriving it from Elements:

```json
{
  "name": "Airplanes",
  "value": "Elements - {nothing,hold,zoom}",
  "comment": "Remove special elements"
},
```

These three definitions computes explicitly the current landing sequence:

```json
{
  "name": "arrivalH",
  "value": "arrivalH_T(curTimeSec(curTimeS,
                                curTimeM, curTimeH))"
},
{
  "name": "arrivalM",
  "value": "arrivalM_T(curTimeSec(curTimeS,
                                curTimeM, curTimeH))"
},
{
  "name": "landing_sequence",
  "value": "%plane.(plane:dom(arrivalH) |
                      arrivalH/plane)*60+arrivalM/plane) -
          currentTime+1)"
},
```

- a list of updates, called items.

The following VISB item uses the above definition to set the visibility attribute of the hold button (visible in Figure 4).

```json
{
  "id": "bt_hold",
  "attr": "visibility",
  "value":"IF no.airplane_is selected=TRUE
          THEN "/"hidden/"
          ELSE "/"visible/"
          END"
},
```

<figure><img src="image_5.png" /><figcaption>Fig. 4. Visualising the state of the model (M8) using PROB and VisB</figcaption></figure>

Observe that the value is a classical B expression, which has access to PROB's IF-THEN-ELSE for expressions and data types such as strings and reals, as well as PROB's external B functions to manipulate them.

- a list of events.

The VISB file also associates the event holdLabel with the hold button; i.e., it is executed when the button is clicked. A hover is also specified, that updates the image when the mouse hovers above the button.

```json
{
  "id": "bt_hold",
  "event": "holdLabel",
  "hovers" : [{"id":"bt_hold","attr":"fill",
               "enter":"gray", "leave":"black"}]
},
```

Observe, that Fig 4 also shows a mouse pointer over the hold button: this is also part of the visualisation and is based on the mousePosition variable of the model. Another interesting aspect is that validation traces can be exported to standalone HTML files using PROB (see [29]). These traces can be reused to step through the traces and inspect the visualisation and the variable values, without access to either PROB, Rodin or the Event-B model. We used those HTML trace files as a means of (email) exchange between ourselves, e.g., to point out and discuss tricky aspects of the models. (Some of these traces are available at https://stups.hhu-hosting.de/models/AMAN/ and [23] for reference.).

## 5 Discussion and Comparison

In a companion paper [15] an Event-B model was developed independently.<fnref n="4" /> The models have very different

<footnote n="4">⁴ The model of this paper was developed by the first author; the second author only intervened in the validation and verification, not in the writing of this model.</footnote>
<figure><img src="image_6.png" /><figcaption>**Fig. 5.** The event refinement hierarchies of our model (top) and of the companion model [15] bottom (generated by PROB)</figcaption></figure>

refinement strategies, as can be guessed from looking at Figure 5. The figure shows the event refinement hierarchy: on the left you can see all events of the most abstract model, while the most concrete model is depicted on the right. Newly introduced events (refining skip) are shown with a red border, while unchanged events are shown in light gray and are not connected with an arrow (just a straight line). Extended events are shown in brown. Our most abstract model (on the top left in Fig. 5) already has four events and twelve variables modeling the concepts of labels and zooming, while the most abstract model of [15] has just one event and variable and zooming is only added in machine M4.

Note that [15] has two more refinement levels not shown in Fig. 5: M9 introducing mouse movements and M10 adding precise pixel locations (something which we did not model in this article). The models also have a quite different set of variables: M8 of our model at ABZ'2023 had 32 variables, the current version has merged some of them and now has 18 variables (see Fig. 6), the comparable M9 of [15] has 17 variables). Still, as seen above, we were able to reuse its VISB visualisation for our model.

Our development models the current time (as three variables for hours, minutes and seconds), which increases during execution (of the autonomous AMAN event dis-

<figure><img src="image_7.png" /><figcaption>**Fig. 6.** The variable refinement hierarchies of our model (generated by PROB)</figcaption></figure>

play). This is better for simulation, but more tricky for model checking as the full state space is automatically infinite (unless we restrict model checking to a particular time interval). In the companion model, the authors normalize the current time to 0; in other words, all times are relative to the current time (cf. [28] or [16]). In addition, the other model only models time as relative minutes, abstracting away both hours and seconds. The use of relative time makes state space finite, but for deeper levels it is too large without other restrictions as well (there are $2^{45}$ values already just for blocking time slots).

In this article, we have used the theory plugin [8] to deal with sequences and with time. For sequences we use the standard Rodin theory, providing direct definitions for sequence operators (like `seqAppend` to concatenate two sequences). The Time theory provides operators to manipulate times and time differences expressed in minutes, hours and seconds. The theory also contains an absolute value function, which is encoded in a context in [15] (which is possible, as the function is not polymorphic). The sequence operations were encoded “by hand” in [15] using relational operators.

In this model, we have also three special elements `hold`, `nothing` and `zoom`, while the other model only has airplane elements and encodes the special values via sets. E.g., `selectedElement=nothing` corresponds to `selectedAirplane = Ø` in [15]. The set encoding requires an additional invariant `card(selectedAirplane) ≤ 1` in [15]. On the one hand, this makes it easier to adapt the model to allow selecting multiple airplanes later, but, on the other hand induces a few more well-definedness POs (due to the use of `card`), which were
surprisingly tedious to discharge. We did not notice any
fundamental differences otherwise. It is thus worth not-
ing that the models represent two alternative EVENT-B
specifications of the same system.

In [5], the model-view-controller (MVC) pattern [1]
has been extended to integrate ASM formal specifica-
tions for the development of user interfaces (UI). Mainly,
the approach is composed of three steps: (1) an MVC
pattern is specified to model the interface of the system
and users; (2) the behavior of the considered system is
then formally specified using ASM notations [6]; in the
last step (3) the MVC elements which represent the user
interaction with the system are linked to ASM elements
using Java annotations. This is very similar to the use
of VISB with EVENT-B models for the purpose of ani-
mation. As for EVENT-B, properties are specified as in-
variants and guaranteed by attaching guards to ASM
actions that make them enabled only if these guards
are fulfilled. For the purpose of verification, some safety
properties are modelled as LTL formulas and then veri-
fied using the NuSMV model checker [9]. We think that
some of them can be simply modelled as invariants since
they depend on variables whose values are taken in the
same state. The main drawback of this approach is that
all the properties are specified at the first refinement
level; this makes it cumbersome.

In [13], the ALLOY formal language is used to model
and verify the AMAN system. The authors propose first
a generic specification of the HAMSTERS task model
(structural and semantics aspects)[4] in ALLOY, then
this latter is instantiated on the AMAN system in or-
der to verify properties on the user interactions with the
system. This approach also considers the robustness of
the AMAN system against ATCo errors represented as
unexpected ATCo actions. Properties to verify are spec-
ified as ALLOY assertions that are then checked using
the bounded model checking engine of Alloy 6. The ver-
ification phase emphasises on the user interaction rather
than the internal functionalities of the AMAN system.
Consequently, this approach does not consider all the
requirements reported in [25].

The approaches presented in [5, 13] both use bounded
model-checkers for verification. To avoid the well-known
problem of state space explosion related to such tools,
the properties verification is only performed for a bounded
number of objects (labels, slots, etc.).

6 Conclusion

In this paper, we presented an EVENT-B formal model of
the Arrival MANager system (called AMAN), the case
study provided in the ABZ2023 conference. Our specifi-
cation takes most requirements into account and defines
additional ones that can be considered common sense,
like a fair processing of landing requests. Compared to
previous case studies proposed in the ABZ conferences,

this present case study contains fewer invariants (65 invariants) but most of them are dynamic and require thus the introduction of several auxiliary variables to store the previous system state. This implies the definition of additional invariants to relate the before and current values of each variable. These additional invariants produce a great number of proof obligations since we have to establish that each event maintains these invariants.

For this particular case study, the expression of invariants that depend on the previous state proved to be difficult since variables are interrelated: at the instant *t*, the arrival times of aircraft depend on the moved labels, requests and aircraft put on hold during the last 10 seconds (at the instant (*t*-step)). The use of PROB helped us in defining the correct expression of these invariants by model checking invariants and simulating some scenarios to validate/fix them. The user-friendly graphical visualisation makes the validation phase easier.

Compared to the previous ABZ case studies [21,24],
the present case study is time-dependent. Indeed, its
main objective is to assign arrival times to aircraft; this
is why we introduced timed aspect from the first specifi-
cation level along with the event display that makes the
time evolve.

In future work, we plan to study and model how
AMAN can decide whether a label can be moved or not.
For this purpose, we can assume that an arrival time in-
terval is associated with each label. In that case, AMAN
would allow the moving of a label *iff* it remains within its
associated interval. Unfortunately, we fell short of time
to deeply investigate this solution. Future improvements
also include exploring the use of decomposition plugins
available in RODIN for structuring the built models into
smaller and thus more manageable units. We can see the
system as a set of independent parts (each of them corre-
sponding to a single ATCo interaction) and the AMAN
as a root part that uses their information to calculate a
new prediction.

**Acknowledgements** We would like to thank Fabian Vu for developing the VISB visualisation of the companion model. We thank David Geleibus and Sebastian Stock for fruitful discussions about the case study. We also thank anonymous referees for their useful feedback.

References

1. Model-View-Controller Pattern, pp. 353–402. Apress, Berkeley, CA (2009), https://doi.org/10.1007/978-1-4302-2370-2_20

2. Abrial, J.R.: The B-Book - Assigning Programs to Mean-ings. Cambridge University Press (1996)

3. Abrial, J.: Modeling in Event-B. Cambridge University Press (2010)

4. Amor, M.B.: Hamsters: A New Task Model for Interac-tive Systems (2009)
5. Bombarda, A., Bonfanti, S., Gargantini, A.: Formal MVC: A Pattern for the Integration of ASM Specifications in UI Development. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14010, pp. 340–357. Springer (2023)

6. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer (2003)

7. Butler, M., Maamria, I.: Mathematical Extension in Event-B through the Rodin Theory Component (2010)

8. Butler, M.J., Maamria, I.: Practical Theory Extension in Event-B. In: Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. pp. 67–81 (2013)

9. Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A New Symbolic Model Checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000), https://doi.org/10.1007/s100090050046

10. Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking - History, Achievements, Perspectives. Lecture Notes in Computer Science, vol. 5000, pp. 196–215. Springer (2008)

11. Clearsy: https://www.atelierb.eu/en/presentation-of-the-b-method/formal-proof-presentation/

12. Consortium, E.B.: http://www.event-b.org/

13. Cunha, A., Macedo, N., Kang, E.: Task Model Design and Analysis with Alloy. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14010, pp. 303–320. Springer (2023)

14. Event-B Consortium: SMT Solvers Plug-in. https://wiki.event-b.org/index.php/SMT_Solvers_Plug-in

15. Geleusus, D., Stock, S., Vu, F., Leuschel, M., Mashkoor, A.: Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14010, pp. 284–302. Springer (2023)

16. Lamport, L.: Real-Time Model Checking Is Really Simple. In: Proceedings CHARME 2005. pp. 162–175 (2005)

17. Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From Animation to Data Validation: The ProB Constraint Solver 10 Years On. In: Boulanger, J.L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, chap. 14, pp. 427–446. Wiley ISTE, Hoboken, NJ (2014)

18. Leuschel, M., Butler, M.J.: ProB: An Automated Analysis Toolset for the B Method. International Journal on Software Tools for Technology Transfer 10(2), 185–203 (2008)

19. Mammar, A., Frappier, M.: Modeling of a Speed Control System using Event-B. In: Raschke, A., Méry, D.,

Houdek, F. (eds.) Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12071, pp. 367–381. Springer (2020)

20. Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: A Formal Refinement-Based Analysis of the Hybrid ERTMS/ETCS Level 3 Standard. Int. J. Softw. Tools Technol. Transf. 22(3), 333–347 (2020)

21. Mammar, A., Frappier, M., Laleau, R.: An Event-B Model of an Automotive Adaptive Exterior Light System. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12071, pp. 351–366. Springer (2020)

22. Mammar, A., Leuschel, M.: Modeling and Verifying an Arrival Manager using Event-B. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14010, pp. 321–339. Springer (2023)

23. Mammar, A., Leuschel, M.: Modeling and Verifying an Arrival Manager using Event-B. Available at https://github.com/AmelMammar/AMAN (January 2024)

24. Mammar, A., Laleau, R.: Modeling a Landing Gear System in Event-B. Int. J. Softw. Tools Technol. Transf. 19(2), 167–186 (2017)

25. Palanque, P.A., Campos, J.C.: AMAN Case Study. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14010, pp. 265–283. Springer (2023)

26. Parnas, D.L., Madey, J.: Functional Documents for Computer Systems. Science of Computer Programming 25(1), 41–61 (1995)

27. Pnueli, A.: The Temporal Logic of Programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence. pp. 46–57. IEEE Computer Society (1977)

28. Rehm, J., Cansell, D.: Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method. In: ISOLA. pp. 179–190 (2007)

29. Vu, F., Happe, C., Leuschel, M.: Generating interactive documents for domain-specific validation of formal models. Int. J. Softw. Tools Technol. Transf. 26(2), 147–168 (2024), https://doi.org/10.1007/s10009-024-00739-0

30. Werth, M., Leuschel, M.: VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. In: Raschke, A., Méry, D., Houdek, F. (eds.) Proceedings ABZ 2020. pp. 260–265. LNCS 12071 (2020)
A An excerpt of the requirements

<table><caption>Table 3: An excerpt of the requirements from [25]</caption><thead><tr><td>Requirement label</td><td>description</td></tr></thead><tbody><tr><td>Req1</td><td>Planes can be added to the flight sequence e.g. planes arriving in a closerange of the airport.</td></tr><tr><td>Req2</td><td>Planes can be removed from the flight sequence e.g. planes changing their landing airport for some reason.</td></tr><tr><td>Req3</td><td>Planes moved earlier or later on the timeline by the PLAN ATCo thus requiring from AMAN the processing of a new prediction.</td></tr><tr><td>Req4</td><td>Planes put on hold by the PLAN ATCo. Planes removed from HOLD will appear as normal aircrafts handled by AMAN.</td></tr><tr><td>Req5</td><td>Aircraft labels should not overlap.</td></tr><tr><td>Req6</td><td>An aircraft label cannot be moved into a blocked time period.</td></tr><tr><td>Req7</td><td>Moving an aircraft label might not be accepted by AMAN if it would require a speed up of the aircraft beyond the capacity of the aircraft.</td></tr><tr><td>Req8</td><td>If AMAN is not functioning (e.g. no update after 10 seconds) the ATCo must be informed about the failure and landing sequence preparation will be done manually (without AMAN).</td></tr><tr><td>Req9</td><td>Displays should provide recognisable feedback on entries made by the ATCo into the system so that the ATCo can detect and correct errors.</td></tr><tr><td>Req10</td><td>Displays should provide recognisable feedback on present state of the automated system or mode of operation. (What is it doing?).</td></tr><tr><td>Req11</td><td>Displays should provide recognisable feedback on actions taken by the system to achieve or maintain a desired state. (What is it trying to do?).</td></tr><tr><td>Req12</td><td>Displays should provide recognisable feedback on future states scheduled by the automation. (What is it going to do next?).</td></tr><tr><td>Req13</td><td>Displays should provide recognisable feedback on transitions between system states.</td></tr><tr><td>Req14</td><td>The set of tasks identified must be feasible on the interactive systems; this may be ensured by checking behavioural equivalence of the task model with respect to a model of the interactive application.</td></tr><tr><td>Req15</td><td>The HOLD button must be available only when one aircraft label is selected.</td></tr><tr><td>Req16</td><td>The zoom value cannot be bigger than 45 and smaller than 15.</td></tr><tr><td>Req17</td><td>Aircraft labels must always be positioned in front of a small bar of the timeline.</td></tr><tr><td>Req18</td><td>Lift of the zoom slider should always be located on the slider bar.</td></tr><tr><td>Req19</td><td>The value displayed next to the zoom slider must belong to the list of seven acceptable values for the zoom.</td></tr><tr><td>Req20</td><td>Each movement of the mouse on the ATCo table must be reflected by a movement of the cursor on the screen</td></tr><tr><td>Req21</td><td>There must be one and only one mouse cursor on the screen</td></tr><tr><td>Req22</td><td>Hold(aircraft) function can only be triggered after a mouse press and a mouse released have been performed on the HOLD button.</td></tr><tr><td>Req23</td><td>Hold(aircraft) function must not be triggered if there is not a mouse press and a mouse released performed on the HOLD button.</td></tr></tbody></table>

B B symbols

Table 4 gives the semantics of the different mathematical symbols used in the paper where:

- A and B denote any sets of elements,

- If a and b are elements of A and B respectively, $a \mapsto b$ denotes the tuple $(a, b)$,
- $A_1$ and $B_1$ denote any subsets of $A$ and $B$ respectively,

- $P$ denotes a predicate,

- $S$ denotes any set expression.
<table><caption>Table 4: Some EVENT-B symbols and their semantics</caption><thead><tr><th>Concept</th><th>Notation</th><th>Semantics</th></tr></thead><tbody><tr><td>A<sub>1</sub>, ..., A<sub>n</sub> is a partition of A</td><td>partition<br>(A<sub>1</sub>, A<sub>2</sub>, ..., A<sub>n</sub>)</td><td>A<sub>i</sub> &sube; A &and; &cup; A<sub>i</sub> = A<br>∀i, j, i &ne; j &rarr; A<sub>i</sub> &cap; A<sub>j</sub> = Ø</td></tr><tr><td>Set of parties of A</td><td>P(A)</td><td>P(A) = {A<sub>1</sub> &cdot; A<sub>1</sub> &sube; A &cap; A}</td></tr><tr><td>Set of non empty parties of A</td><td>P1(A)</td><td>P1(A) = {A<sub>1</sub> &cdot; A<sub>1</sub> &sube; A &and; A<sub>1</sub> &ne; Ø}</td></tr><tr><td>Quantified union</td><td>U z. P | S</td><td>if ∀z.(P &rarr; S &sube; T, then U z. P | S = {y | y &in; T &and; ∃z.(z &in; T &and; P &and; y &in; S)})</td></tr><tr><td>Lambda expression</td><td>λx.(x &in; T &and; P | E)</td><td>If ∀x.(x &in; T &rarr; E | U),<br>λx.(x &in; T &and; P | E) = {x, y | x, y &in; T &times; U &and; P &and; y = E}</td></tr><tr><td>R is a relation from A to B</td><td>R &in; A &leftrightarrow; B</td><td>R &sube; {a &rarr; b, a &in; A &and; b &in; B}</td></tr><tr><td>R<sup>-1</sup> is the inverse of R</td><td>R<sup>-1</sup></td><td>R<sup>-1</sup> = {b &rarr; a &cdot; a &rarr; b &in; R}</td></tr><tr><td>Difference</td><td>R<sub>1</sub> \ R<sub>2</sub></td><td>if R<sub>1</sub> &in; A &leftrightarrow; B and R<sub>2</sub> &in; A &leftrightarrow; B then,<br>R<sub>1</sub> \ R<sub>2</sub> = {a &rarr; b, a &rarr; b &in; R<sub>1</sub> &and; a &rarr; b &notin; R<sub>2</sub>}</td></tr><tr><td>Override of R<sub>1</sub> by R<sub>2</sub></td><td>R<sub>1</sub> &larr; R<sub>2</sub></td><td>if R<sub>1</sub> &in; A &leftrightarrow; B and R<sub>2</sub> &in; A &leftrightarrow; B then,<br>R<sub>1</sub> &larr; R<sub>2</sub> = {a &rarr; b, a &rarr; b &in; R<sub>2</sub> &or; (a &rarr; b &in; R<sub>1</sub> &and; a &notin; dom(R<sub>2</sub>))}</td></tr><tr><td>Direct product of R<sub>1</sub> and R<sub>2</sub></td><td>R<sub>1</sub> &otimes; R<sub>2</sub></td><td>if R<sub>1</sub> &in; A &leftrightarrow; B and R<sub>2</sub> &in; A &leftrightarrow; C then,<br>R<sub>1</sub> &otimes; R<sub>2</sub> = {a &rarr; (b &rarr; c), a &rarr; b &in; R<sub>1</sub> &and; a &rarr; c &in; R<sub>2</sub>}</td></tr><tr><td>Image of A<sub>1</sub> by R</td><td>R[A<sub>1</sub>]</td><td>R[A<sub>1</sub>] = {b<sub>1</sub> &cdot; (b<sub>1</sub> &in; B &and; ∃a<sub>1</sub> &cdot; (a<sub>1</sub> &in; A<sub>1</sub> &and; a<sub>1</sub> &rarr; b<sub>1</sub> &in; R))}</td></tr><tr><td>Domain of R</td><td>dom(R)</td><td>dom(R) = {a<sub>1</sub> &cdot; (a<sub>1</sub> &in; A &and; ∃b<sub>1</sub> &cdot; (b<sub>1</sub> &in; B &and; a<sub>1</sub> &rarr; b<sub>1</sub> &in; R))}</td></tr><tr><td>Range of R</td><td>ran(R)</td><td>ran(R) = {b<sub>1</sub> &cdot; (b<sub>1</sub> &in; B &and; ∃a<sub>1</sub> &cdot; (a<sub>1</sub> &in; A &and; a<sub>1</sub> &rarr; b<sub>1</sub> &in; R))}</td></tr><tr><td>Domain restriction of R</td><td>A<sub>1</sub> &larr; R</td><td>A<sub>1</sub> &larr; R = {a &rarr; b &cdot; (a &rarr; b &in; R &and; a &in; A<sub>1</sub>)}</td></tr><tr><td>Partial function f</td><td>f &in; A &rarr; B</td><td>f &in; A &leftrightarrow; B &and; ∀a.(a &in; A &rarr; card(f[{a}]) &le; 1)</td></tr><tr><td>Total function f</td><td>f &in; A &rarr; B</td><td>f &in; A &leftrightarrow; B &and; dom(f) = A</td></tr><tr><td>skip substitution</td><td>skip</td><td>Do nothing: all the variables are not modified.</td></tr><tr><td>ANY substitution</td><td>ANY X WHERE G THEN S END</td><td>Execute the substitution S for any values of parameters X that satisfy G</td></tr><tr><td>Guard of an event E</td><td>grd(E)</td><td>If E = ANY X WHERE G THEN S then, grd(E) = G</td></tr></tbody></table>