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.