212 lines
7.1 KiB
HTML
212 lines
7.1 KiB
HTML
|
<?xml version="1.0" encoding="UTF-8"?>
|
||
|
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
|
||
|
|
<html xmlns="http://www.w3.org/1999/xhtml">
|
||
|
|
<head>
|
||
|
|
<meta content="text/html; charset=utf-8" http-equiv="Content-Type"/>
|
||
|
|
<meta content="Pentabarf" name="generator"/>
|
||
|
|
<meta content="2011-04-24" name="DC.date"/>
|
||
|
|
<title>EH2011: Correct-by-Construction</title>
|
||
|
|
<link type="text/css" href="../style.css" rel="Stylesheet" media="screen,print"/>
|
||
|
|
</head>
|
||
|
|
<body>
|
||
|
|
<div class="noprint" id="conference-logo">
|
||
|
|
<a href="http://easterhegg2011.hamburg.ccc.de">
|
||
|
|
<img alt="Easterhegg 2011" src="../images/conference-128x128.png"/>
|
||
|
|
</a>
|
||
|
|
</div>
|
||
|
|
<div class="noprint" id="menu">
|
||
|
|
<ul>
|
||
|
|
<li>
|
||
|
|
<a href="../index.en.html">
|
||
|
|
<span class="normal">Index</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../day_2011-04-22.en.html">
|
||
|
|
<span class="normal">Karfreitag - 2011-04-22</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../day_2011-04-23.en.html">
|
||
|
|
<span class="normal">Ostersamstag - 2011-04-23</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../day_2011-04-24.en.html">
|
||
|
|
<span class="normal">Ostersonntag - 2011-04-24</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../day_2011-04-25.en.html">
|
||
|
|
<span class="normal">Ostermontag - 2011-04-25</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../speakers.en.html">
|
||
|
|
<span class="normal">Speakers</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="../events.en.html">
|
||
|
|
<span class="normal">Events</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<ul class="track">
|
||
|
|
<li class="track-hacking">
|
||
|
|
<a href="../track/Hacking/index.en.html">
|
||
|
|
<span class="normal">Hacking</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li class="track-administration">
|
||
|
|
<a href="../track/Administration/index.en.html">
|
||
|
|
<span class="normal">Administration</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li class="track-gesellschaft">
|
||
|
|
<a href="../track/Gesellschaft/index.en.html">
|
||
|
|
<span class="normal">Gesellschaft</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li class="track-making">
|
||
|
|
<a href="../track/Making/index.en.html">
|
||
|
|
<span class="normal">Making</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li class="track-historylessons">
|
||
|
|
<a href="../track/history lessons/index.en.html">
|
||
|
|
<span class="normal">history lessons</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
<li class="track-meta">
|
||
|
|
<a href="../track/Meta/index.en.html">
|
||
|
|
<span class="normal">Meta</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
</ul>
|
||
|
|
</li>
|
||
|
|
</ul>
|
||
|
|
</div>
|
||
|
|
<div id="content">
|
||
|
|
<p class="release">EH2011 - 21</p>
|
||
|
|
<p class="intro">
|
||
|
|
<strong>Easterhegg 2011</strong>
|
||
|
|
<br/>
|
||
|
|
<em>the ccc family event</em>
|
||
|
|
</p>
|
||
|
|
<div class="section vevent" id="event">
|
||
|
|
<div id="infobox">
|
||
|
|
<table>
|
||
|
|
<tr>
|
||
|
|
<th colspan="2">Speakers</th>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td>
|
||
|
|
<a href="../speakers/1924.en.html">
|
||
|
|
<img height="32" width="32" src="../images/person-0-32x32.png"/>
|
||
|
|
</a>
|
||
|
|
</td>
|
||
|
|
<td>
|
||
|
|
<a href="../speakers/1924.en.html">Alexander Bernauer</a>
|
||
|
|
</td>
|
||
|
|
</tr>
|
||
|
|
</table>
|
||
|
|
<table>
|
||
|
|
<tr>
|
||
|
|
<th colspan="2">Schedule</th>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Day</td>
|
||
|
|
<td class="value">Ostersonntag - 2011-04-24</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Room</td>
|
||
|
|
<td class="value location">Raum 0</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Start time</td>
|
||
|
|
<td class="value dtstart" title="2011-04-24T11:00:00+02:00">11:00</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Duration</td>
|
||
|
|
<td class="value duration" title="P01H00M00S">01:00</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<th colspan="2">Info</th>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">ID</td>
|
||
|
|
<td class="value" title="4365@EH2011@pentabarf.org">4365</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Event type</td>
|
||
|
|
<td class="value">Lecture</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Track</td>
|
||
|
|
<td class="value">Making</td>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="keyword">Language used for presentation</td>
|
||
|
|
<td class="value">German</td>
|
||
|
|
</tr>
|
||
|
|
</table>
|
||
|
|
<table>
|
||
|
|
<tr>
|
||
|
|
<th colspan="2">Feedback</th>
|
||
|
|
</tr>
|
||
|
|
<tr>
|
||
|
|
<td class="feedback" colspan="2">
|
||
|
|
Did you attend this event? <br/>
|
||
|
|
<a href="https://cccv.pentabarf.org/feedback/EH2011/event/4365.en.html">Give Feedback</a>
|
||
|
|
</td>
|
||
|
|
</tr>
|
||
|
|
</table>
|
||
|
|
</div>
|
||
|
|
<h1 class="title summary">Correct-by-Construction</h1>
|
||
|
|
<p class="subtitle">Proving instead of testing</p>
|
||
|
|
<img class="event-image" src="../images/event-4365-128x128.png"/>
|
||
|
|
<div class="abstract">
|
||
|
|
<p>Writing correct software is often crucial but nevertheless very hard to accomplish. While in the public perception testing appears to be the answer, formal methods are evolving and become serious alternatives.</p>
|
||
|
|
|
||
|
|
<p>This lecture will give an introduction to formal methods in general and model proving in particular. By means of a simple example application we will explore the formal method approach to correct-by-construction software.</p> </div>
|
||
|
|
<div class="description">
|
||
|
|
<p>Testing code is good and clearly helps in writing correct software. Nevertheless, just the fact that the tests execute successfully does not mean that there are no bugs in the code. This limitation is inherent to testing. In contrast, formal methods strive to provide complete and sound verification of software.</p>
|
||
|
|
|
||
|
|
<p>This lecture will first give an overview of various formal method approaches. Among all those options we will then focus on model proving. Instead of writing code and validating it afterwards, in this approach the code is generated from a model which is proven to be correct according to a given specification.</p>
|
||
|
|
|
||
|
|
<p>To demonstrate the applicability, we will use Rodin, a workbench for the Event-B formal method. We will create a simple example model, specify some system properties, prove that the model fulfills these requirements and generate executable code from it.</p> </div>
|
||
|
|
<div class="links">
|
||
|
|
<h2>Links</h2>
|
||
|
|
<ul>
|
||
|
|
<li>
|
||
|
|
<a href="http://www.event-b.org/" rel="bookmark">Event-B website</a>
|
||
|
|
</li>
|
||
|
|
<li>
|
||
|
|
<a href="http://" rel="bookmark">http://</a>
|
||
|
|
</li>
|
||
|
|
</ul>
|
||
|
|
</div>
|
||
|
|
<div id="navigation">
|
||
|
|
<a href="../events/4367.en.html">
|
||
|
|
<span class="previous" title="Code Attestation with Compressed Instruction Code"><<<</span>
|
||
|
|
</a>
|
||
|
|
<a href="../events/4381.en.html">
|
||
|
|
<span class="next" title="Cryptdroid">>>></span>
|
||
|
|
</a>
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
</div>
|
||
|
|
<div class="noprint" id="conference-logo">
|
||
|
|
<a href="http://easterhegg2011.hamburg.ccc.de/index.shtml">
|
||
|
|
<img src="'http://easterhegg2011.hamburg.ccc.de/img/eh2011_banner_final_o_LOGO.png" alt="Easterhegg 2011" width="1280" height="160"/>
|
||
|
|
</a>
|
||
|
|
</div>
|
||
|
|
<li>
|
||
|
|
<a href="http://easterhegg2011.hamburg.ccc.de/index.shtml">
|
||
|
|
<span class="normal">Home</span>
|
||
|
|
</a>
|
||
|
|
</li>
|
||
|
|
</body>
|
||
|
|
</html>
|