1 of 25

MODELING AND VERIFYING AN ARRIVAL MANAGER USING EVENT-B

AMEL MAMMAR, MICHAEL LEUSCHEL

2 of 25

MODELING STRATEGY AND ASSUMPTIONS

  • Modelling strategy:
    • Periodically, AMAN reads all the ATCO inputs at once, then computes and displays a new arrival sequence

​

​

  • Assumptions:
    • All the arrival times fit on one day
    • The arrival times are scheduled for the next 3 hours

​

​

2

31/05/2023

3 of 25

EVENT-B METHOD

  • State–based formal method
  • A model is made up on:
      • Contexts: sets (user types), constants and axioms
      • Machines/Refinements: variables, invariants, events
  • Proof correctness:
    • Machine/Refinement: each event must preserve the invariant of the machine/refinement
    • Refinement:
      • The guard of the refined event must be stronger than that of the abstract one
      • The effect of a concrete event is included in that of the abstract one

​

​

​

3

31/05/2023

4 of 25

EVENT-B MODEL STRUCTURE

4

31/05/2023

M1

M2

C1

C2

EXTENDS

SEES

REFINES

M5

M6

M7

M8

Displaying the arrival

times sequence

Putting a label on hold

Landing requests

Mouse interactions

Historical information

AMAN failure

ATCO interactions

AMAN functionnalities

AMAN failure

M4

Blocked zones

5 of 25

FIRST LEVEL: DISPLAY OF LABELS ARRIVAL TIMES

  • An arrival time may be associated with a label

​

​

  • Two different labels should be seperated by a security distance
  • According to a zoom level, some labels are displayed on the screen

6 of 25

6

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

7 of 25

7

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

Landing labels

8 of 25

8

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

New arrival times

9 of 25

9

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

Security distance

10 of 25

10

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

Labels to display

11 of 25

11

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

Arrival time update

12 of 25

12

31/05/2023

1. Increasing the current time by an amount of seconds (10 seconds)

2. Re-computing the new arrival times of a set of labels

Current time update: +10s

13 of 25

SECOND LEVEL: LABELS ON HOLD

  • A label may be made on hold…
  • …, in that case it should be removed from the arrival sequence

​

13

31/05/2023

(Seconds)

14 of 25

S

14

31/05/2023

A label made on hold does not belong to the new planned labels

15 of 25

FOURTH LEVEL: BLOCKED ZONES

  • Some zones may be blocked
  • No label can be planned in a blocked zone

15

31/05/2023

blockedZones ⊆ Minutes × Hours

∀ x,y· x↦y∈ blockedZones

⇒

blockTime(x↦y)≤curTimeSec(curTimeS, curTimeM, curTimeH)

∀x, y· x↦y ∈ blockedZones ∧

blockTime(x↦y) < curTimeSec(curTimeS, curTimeM, curTimeH)

⇒

(∀l· l∈ dom(arrivalM)⇒

curTimeMin(x, y) ≠ curTimeMin(arrivalM(l),arrivalH(l)))

(Seconds)

blockTime ∈ blockedZones→ℕ

16 of 25

S

16

31/05/2023

ran(arr)∩(⋃ x,y·x↦y∈ blockedZones∣{curTimeMin(x,y)})=∅

no label can be planned in a blocked zone

17 of 25

FIFTH LEVEL: LANDING REQUESTS

17

31/05/2023

Refinement of the event display: requests are dealt with according to FIFO strategy

Refinement of the event display: the labels for which arrival times are computed:

Landing requests are modeled as an injective sequence

18 of 25

SOME STATISTICS

  • Two months development/proof:
    • Most of the functional requirements are covered: 18/23
    • 32 variables + 15 events
  • Models are proved and verified:
    • Model checking: ProB for detecting obvious invariant violations
    • Validation: ProB on our own scenarios
    • Proof obligations correctness:
      • 349 proof obligations:
        • 124 automatic (35%)
        • 225 interactive

​

​

​

18

31/05/2023

19 of 25

PROB-VISB VISUALISATION

VISB ARCHITECTURE

19

31/05/2023

20 of 25

PROB-VISB VISUALISATION

  • Same Visualisation was used for two models
  • Event-B model here has significant differences with

other Event-B model from Geleßus et al.

    • different variables
    • different way of modelling selections
    • different encoding of time
    • different events and refinement hierarchy

​

20

31/05/2023

21 of 25

21

31/05/2023

22 of 25

22

31/05/2023

23 of 25

REUSING THE VISUALISATION FOR TWO MODELS

23

31/05/2023

24 of 25

EXPORTING TRACES

TO STAND-ALONE HTML FILES

​

24

31/05/2023

25 of 25

25

31/05/2023