https://wiki.event-b.org/index.php?action=history&feed=atom&title=Modeling_Feedback Modeling Feedback - Revision history 2026-05-19T20:26:18Z Revision history for this page on the wiki MediaWiki 1.42.1 https://wiki.event-b.org/index.php?title=Modeling_Feedback&diff=6154&oldid=prev imported>Mathieu at 13:44, 28 October 2008 2008-10-28T13:44:24Z <p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en-GB"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 13:44, 28 October 2008</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1">Line 1:</td> <td colspan="2" class="diff-lineno">Line 1:</td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">{{TOCright}}</ins></div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Hereafter is a gathering of some modeling feedbacks, which may be useful to the whole community. They come from:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Hereafter is a gathering of some modeling feedbacks, which may be useful to the whole community. They come from:</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* Modeling activity for a [[Railway Interlocking Feedback|&#039;&#039;railway interlocking&#039;&#039; system]] (by [[Systerel]]).</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* Modeling activity for a [[Railway Interlocking Feedback|&#039;&#039;railway interlocking&#039;&#039; system]] (by [[Systerel]]).</div></td></tr> </table> imported>Mathieu https://wiki.event-b.org/index.php?title=Modeling_Feedback&diff=6153&oldid=prev imported>Mathieu: /* WD PO may bear essential model semantic */ 2008-10-28T13:44:01Z <p><span dir="auto"><span class="autocomment">WD PO may bear essential model semantic</span></span></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en-GB"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 13:44, 28 October 2008</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l22">Line 22:</td> <td colspan="2" class="diff-lineno">Line 22:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Safety at some point, unexpectedly relied upon a WD PO:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Safety at some point, unexpectedly relied upon a WD PO:</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>&lt;math&gt;<del style="font-weight: bold; text-decoration: none;">\texttt</del>{next(head<del style="font-weight: bold; text-decoration: none;">$</del>_{train}<del style="font-weight: bold; text-decoration: none;">$</del>)<del style="font-weight: bold; text-decoration: none;">}</del>&lt;/math&gt; is well defined.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>&lt;math&gt;{next<ins style="font-weight: bold; text-decoration: none;">}</ins>(<ins style="font-weight: bold; text-decoration: none;">{</ins>head<ins style="font-weight: bold; text-decoration: none;">}</ins>_{train})&lt;/math&gt; is well defined.</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Abstraction is heavily needed ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Abstraction is heavily needed ==</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Image:Train-position-abstraction.png|250px|right]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Image:Train-position-abstraction.png|250px|right]]</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Concepts provided in informal specification are insufficient to express safety property.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Concepts provided in informal specification are insufficient to express safety property.</div></td></tr> </table> imported>Mathieu https://wiki.event-b.org/index.php?title=Modeling_Feedback&diff=6152&oldid=prev imported>Mathieu: preliminary notes 2008-10-28T13:43:08Z <p>preliminary notes</p> <p><b>New page</b></p><div>Hereafter is a gathering of some modeling feedbacks, which may be useful to the whole community. They come from:<br /> * Modeling activity for a [[Railway Interlocking Feedback|&#039;&#039;railway interlocking&#039;&#039; system]] (by [[Systerel]]).<br /> * Modeling activities for a &#039;&#039;train tracking&#039;&#039; system (by Systerel).<br /> <br /> == What is the goal of a model ==<br /> Real goal is to obtain a proof, not a model.<br /> <br /> The model is only our mean of choice to obtain a proof.<br /> <br /> Highly iterative task between &#039;&#039;proof&#039;&#039; and &#039;&#039;model&#039;&#039;.<br /> <br /> == What is a safe system? ==<br /> {{TODO|Safety preservation}}<br /> <br /> == What is a good model? ==<br /> {{TODO|model validation via animation}}<br /> <br /> == How to take into account degraded cases ==<br /> {{TODO|model must be totally closed}}<br /> <br /> == WD PO may bear essential model semantic ==<br /> Safety at some point, unexpectedly relied upon a WD PO:<br /> <br /> &lt;math&gt;\texttt{next(head$_{train}$)}&lt;/math&gt; is well defined.<br /> <br /> == Abstraction is heavily needed ==<br /> [[Image:Train-position-abstraction.png|250px|right]]<br /> Concepts provided in informal specification are insufficient to express safety property.</div> imported>Mathieu