Difference between revisions of "Modeling Feedback"

From Event-B
Jump to navigationJump to search
imported>Mathieu
imported>Mathieu
m
 
Line 1: Line 1:
 +
{{TOCright}}
 
Hereafter is a gathering of some modeling feedbacks, which may be useful to the whole community. They come from:
 
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 Feedback|''railway interlocking'' system]] (by [[Systerel]]).
 
* Modeling activity for a [[Railway Interlocking Feedback|''railway interlocking'' system]] (by [[Systerel]]).

Latest revision as of 13:44, 28 October 2008

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.