# Modeling Feedback

From Event-B

Jump to navigationJump to searchHereafter is a gathering of some modeling feedbacks, which may be useful to the whole community. They come from:

- Modeling activity for a
*railway interlocking*system (by Systerel). - Modeling activities for a
*train tracking*system (by Systerel).

## What is the goal of a model

Real goal is to obtain a proof, not a model.

The model is only our mean of choice to obtain a proof.

Highly iterative task between *proof* and *model*.

## What is a safe system?

**TODO**: *Safety preservation*

## What is a good model?

**TODO**: *model validation via animation*

## How to take into account degraded cases

**TODO**: *model must be totally closed*

## WD PO may bear essential model semantic

Safety at some point, unexpectedly relied upon a WD PO:

is well defined.

## Abstraction is heavily needed

Concepts provided in informal specification are insufficient to express safety property.