EH2011 - 21
Easterhegg 2011
the ccc family event
| Speakers | |
|---|---|
|
Alexander Bernauer |
| Schedule | |
|---|---|
| Day | Ostersonntag - 2011-04-24 |
| Room | Raum 0 |
| Start time | 11:00 |
| Duration | 01:00 |
| Info | |
| ID | 4365 |
| Event type | Lecture |
| Track | Making |
| Language used for presentation | German |
| Feedback | |
|---|---|
|
Did you attend this event? Give Feedback |
Correct-by-Construction
Proving instead of testing
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.
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.
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.
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.
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.
