Call for Papers

Formale Methoden in kleinen und mittleren Unternehmen ( Vortrag )

Referent: Sebastian Grobosch, VEMAC GmbH & Co. KG
Vortragsreihe: Test&Qualität
Zeit: 05. Dezember 11:45-12:25
Co-Referenten: Dr.-Ing. Michael Reke, Prof. Dr.-Ing. Stefan Kowalewksi

Zielgruppe

Entwicklung

Themenbereiche

Test & Qualitätssicherung, Software Engineering Management

Kurzfassung

Das Ziel ist es, den Einsatz von formalen Methoden in der Softwareentwicklung von kleinen und mittleren Unternehmen (KMU) anhand von Beispielen darzustellen. Dazu werden zwei Methoden - Modelchecking mit Zeitautomaten und formale Verifikation von binär Code - näher betrachtet. Es wird beschrieben, wie in einem KMU ein Framework zum Einsatz dieser beiden Methoden entwickelt wurde. Weiterhin geht der Vortrag darauf ein, wie man Anforderungen an das System formalisieren kann um diese "Formeln" dann zum Verifizieren von Anforderungen zu verwenden. Abschließend wird der Einsatz dieser Methoden an einem realen Projekt untersucht und die Ergebnisse dargestellt und diskutiert.

Gliederung

- Einführung
-- Was sind formale Methoden?
-- Welche formalen Ansätze gibt es?
-- Wieso ist SW Qualität in KMU wichtig?
-- Was sind die Randbedingungen bei KMU?
- Motivation und Darstellung der Probleme
-- Frühzeitige Abschätzung von Ressourcennutzung auf µControllern (Speicher, Rechenzeit)
-- Wie kann ich sicher stellen, dass die Anforderungen an meine Software erfüllt werden?
- Realisierung
-- Scheduling-Analysen mit Zeitautomaten
-- formale Verifikation mittels binär-Code Model-Checking
- Evaluierung
-- Darstellung der Case Study
-- Ergebnisse der Scheduling-Analysen mit UPPAAL
-- Gefundene Fehler durch den Einsatz von ARCADE für die binär-Code Analyse
- Zusammenfassung und Ausblick
-- Wie kann die Weiterentwicklung aussehen?
-- Welche weiteren formalen Methoden können den SW-Entwicklungsprozess unterstützen?

Nutzen und Besonderheiten

Der Vortrag hat das Ziel, dem Zuhörer die Vorteile von formalen Methoden in der Softwareentwicklung aufzuzeigen. Des Weiteren soll gezeigt werden, dass die Qualität in der Entwicklung durch den Einsatz dieser Methoden gesteigert werden kann. Als weiteres Ergebnis soll der Zuhörer mitnehmen, dass auch bei kleinen Unternehmen die Einführung von formalen Methoden in der Software Entwicklung Sinn macht und einen Mehrwert darstellt. Die Besonderheit des hier gezeigten Ansatzes ist, dass Tools, die in einem eher theoretischen universitären Umfeld entstanden sind, durchaus auch in der täglichen Projektarbeit von Softwareentwicklern genutzt werden können.

Über den Referenten

Herr Sebastian Grobosch erlangte 2007 den Abschluss als Dipl.-Ing. der Elektrotechnik an der RWTH Aachen. Parallel zu seiner Promotion arbeitet er als verantwortlicher Leiter der Software Entwicklung in der VEMAC. Im Rahmen seiner Tätigkeit setzte er federführend Projekte im Bereich der Automatisierungsoftware und in der Entwicklung von Prototypen-Steuergeräten um. Seine Schwerpunkte sind dabei die Verifikation von embedded Software und deren Anwendung in komplexen Automotiven-Projekten.