Modeling Feedback

From Event-B
Revision as of 13:44, 28 October 2008 by imported>Mathieu
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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

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

Train-position-abstraction.png

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