| Beginn: | 16.09.2004, 18:00Uhr |
| Ende: | 16.09.2004, 20:00Uhr |
| Ort: | Fraunhofer ISST, Mollstraße 1, 10178 Berlin |
Das Berlin-Brandenburger Software-Forum des VSEK-Projekts lädt zu folgender Veranstaltung ein:
Formale Methoden in der Software-EntwicklungProf. Dr. Monika Heiner, Dr. Heinrich Rust (BTU Cottbus)Software-basierte Systeme sind aus unserem Alltag nicht mehr wegzudenken. Sie halten Einzug in nahezu alle Bereiche unseres Lebens. Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung nur allzu oft auf der Strecke. In manchen Bereichen mag dies tolerierbar sein, sobald aber durch fehlerhafte Software Menschenleben gefährdet sind oder hohe finanzielle Schäden zu befürchten sind, muss auf die Qualität, insbesondere auf die Korrektheit der Software besonderen Wert gelegt werden. Die zunehmende Komplexität moderner Software und das verständliche Sicherheitsbedürfnis der Endanwender erfordern Methoden und Herangehensweisen, mit denen sich die Korrektheit und Sicherheit nicht nur exemplarisch überprüfen, sondern auch erschöpfend beweisen lässt. Heute benutzte Verfahren beziehen sich hauptsächlich auf einen mehr oder weniger gründlichen Test der Software, der jedoch niemals vollständig sein kann. Die Veranstaltung thematisiert deshalb den Einsatz formaler Methoden in der Software-Entwicklung. Formale Methoden haben in der Software-Entwicklung einen schlechten Ruf: Ein hoher Aufwand, so der Verdacht, führt nur zu geringem Ertrag. Ein Überblick über das große Gebiet der formalen Methoden zeigt aber, dass es auch praxistaugliche formale Methoden gibt. Nicht selten liegt das Erfolgsrezept in der Verpackung. Wir sehen uns Beispiele an. Anhand eines konkreten Projekts aus der Automatisierungstechnik wird die praktische Anwendbarkeit des Modelchecking als ein Ansatz zur automatischen Beweisführung bei der Überprüfung der Funktions- und Sicherheitsanforderungen von Steuerungsprogrammen gezeigt. Hierbei wird eine dedizierte Spezifikationssprache vorgestellt, mit der die Anforderungen an ein Steuerungsprogramm in einer weitestgehend natürlichen Sprache verfasst werden können, die trotzdem ausreichend formal für eine automatische Beweisführung ist. Das Programm sieht folgende Punkte vor:
Die Teilnahme ist kostenlos. Da die Kapazität begrenzt ist, wird um eine Anmeldung bis zum 13.09.2004 auf der Webseite http://www.forumbb.de gebeten. Ihre Teilnahmebestätigung berechtigt Sie dann zur Teilnahme. |
