Difference between revisions of "Modeling Feedback"
From Event-B
Jump to navigationJump to searchimported>Mathieu m (preliminary notes) |
(No difference)
|
Revision as of 13:43, 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:
Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \texttt{next(head$_{train}$)} is well defined.
Abstraction is heavily needed
Concepts provided in informal specification are insufficient to express safety property.