Modeling Feedback

From Event-B
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


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