https://wiki.event-b.org/index.php?action=history&feed=atom&title=User%3AJens%2FCode_generation_Using_Flow_Analysis 2026-06-01T14:02:02Z Revision history for this page on the wiki MediaWiki 1.42.1 https://wiki.event-b.org/index.php?title=User:Jens/Code_generation_Using_Flow_Analysis&diff=10741&oldid=prev 2009-10-20T16:46:57Z

<p><span dir="auto"><span class="autocomment">Concurrent Embedded Programs from Event-B Models</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 16:46, 20 October 2009</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l4">Line 4:</td> <td colspan="2" class="diff-lineno">Line 4:</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>The final step of the method, code generation, is fully automatic  </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>The final step of the method, code generation, is fully automatic  </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>so that the user is concerned only with formal Event-B models but  </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>so that the user is concerned only with formal Event-B models but  </div></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>not with code generation. The target architecture is AUTOSAR, a</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>not with code generation. The target architecture is <ins style="font-weight: bold; text-decoration: none;">[http://www.autosar.org/ </ins>AUTOSAR<ins style="font-weight: bold; text-decoration: none;">]</ins>, a</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>cooperative concurrent real-time architecture used in the automotive</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>cooperative concurrent real-time architecture used in the automotive</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>industry: programs consist threads that are split into blocks,  </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>industry: programs consist threads that are split into blocks,  </div></td></tr> </table>

imported>Jens https://wiki.event-b.org/index.php?title=User:Jens/Code_generation_Using_Flow_Analysis&diff=10740&oldid=prev 2009-10-20T16:44:53Z

<p>New page: == Concurrent Embedded Programs from Event-B Models == We propose a method for concurrent program development in Event-B. The final step of the method, code generation, is fully automati...</p> <p><b>New page</b></p><div>== Concurrent Embedded Programs from Event-B Models ==<br /> <br /> We propose a method for concurrent program development in Event-B. <br /> The final step of the method, code generation, is fully automatic <br /> so that the user is concerned only with formal Event-B models but <br /> not with code generation. The target architecture is AUTOSAR, a<br /> cooperative concurrent real-time architecture used in the automotive<br /> industry: programs consist threads that are split into blocks, <br /> called runnables. These runnables are executed concurrently by an <br /> embedded operating systems. From this description we see that we <br /> immediately face two problems: how to decompose into threads and <br /> how to specify runnables.<br /> <br /> Following the method of sequential program development proposed by<br /> Abrial, the entire development takes place in Event-B only applying<br /> a method for thread and runnable decomposition. Our approach uses<br /> formal control flow analysis to compose programs from events on the<br /> way removing automatically abstract program counters from the Event-B <br /> model.<br /> <br /> In order for the method to work four techniques need to be developed:<br /> # thread decomposition<br /> # runnable decomposition<br /> # control flow analysis<br /> # event composition<br /> Concerning 1. and 2. we can rely on existing work on (concurrent)<br /> decomposition. Concerning 3. we have made preliminary experiments <br /> that look promising, and 4. has been developed by Abrial.</div>

imported>Jens