Modeling Feedback: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Mathieu m preliminary notes |
imported>Mathieu mNo edit summary |
||
| (One intermediate revision by the same user not shown) | |||
| 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]]). | ||
| Line 22: | Line 23: | ||
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. | ||
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:
- Modeling activity for a railway interlocking system (by Systerel).
- Modeling activities for a train tracking system (by Systerel).
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.
