 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||
| |||||||||||||||||||||||
| |||||||||||||||||||||||
|
| ||||||
|  | | | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Erfahrung |
|
Formale Methoden in der Software-Entwicklung |
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| Beschreibung der Erfahrung | ||||||||||||||||
| ||||||||||||||||
| 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. Der durchgeführte ForumBB-Themenabend "Formale Methoden in der Software-Entwicklung" behandelte 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. Der erste Fachvortrag gab einen Überblick über das große Gebiet der formalen Methoden und zeigte, dass es auch praxistaugliche formale Methoden gibt. Anhand eines konkreten Projekts aus der Automatisierungstechnik wurde im zweiten Fachvortrag die praktische Anwendbarkeit des Modelchecking als ein Ansatz zur automatischen Beweisführung bei der Überprüfung der Funktions- und Sicherheitsanforderungen von Steuerungsprogrammen gezeigt. Hierbei wurde 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. Einzelheiten sowie Literaturhinweise sind den folgenden Vortragsfolien zu entnehmen. | ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| Downloads | ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
| ||||||||||||||||
Eintrag kommentieren
| ||||
| ||||
| ||||
| ||||
| Formale Methoden in... | ||||
| ||||
| ||||
| ||||
| ||||
 | Adressiert Technologien | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
| ||||
| | | ||
| ||||||||||||||
|
