Modeling Feedback

Hereafter 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:

${next}({head}_{train})$ is well defined.

Abstraction is heavily needed

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