Difference between revisions of "Modeling Feedback"
From Event-B
Jump to navigationJump to searchimported>Mathieu m (preliminary notes) |
imported>Mathieu |
||
| Line 22: | Line 22: | ||
Safety at some point, unexpectedly relied upon a WD PO: | Safety at some point, unexpectedly relied upon a WD PO: | ||
| − | <math> | + | <math>{next}({head}_{train})</math> is well defined. |
== Abstraction is heavily needed == | == Abstraction is heavily needed == | ||
[[Image:Train-position-abstraction.png|250px|right]] | [[Image:Train-position-abstraction.png|250px|right]] | ||
Concepts provided in informal specification are insufficient to express safety property. | Concepts provided in informal specification are insufficient to express safety property. | ||
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:
- Modeling activity for a railway interlocking system (by Systerel).
- Modeling activities for a train tracking system (by Systerel).
Contents
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.
