In der Raumfahrt können Unfälle schnell zu lebensbedrohlichen Situationen und sehr hohen und unvorhergesehenen Kosten führen. Sicherheit spielt daher eine wichtige Rolle.

Im Umgang mit den komplexen, technischen Systemen in diesem Bereich ist die Interaktion zwischen Mensch und Maschine eine häufige Fehlerquelle. Es sind daher Techniken zur Entwicklung von robusten Nutzerschnittstellen gefragt, die optimal auf die Bedürfnisse der Nutzer angepasst sind.

Auch in anderen Bereichen, wie der Luftfahrt oder bei der Bedienung von industriellen Kraftwerken oder medizinischen Geräten, hat sich die Mensch-Maschine-Interaktion häufig als eine der Ursachen von Unfällen erwiesen. Dabei ist die Ursache nicht nur beim menschlichen Bediener zu suchen. Einerseits wird in vielen Fällen die Wahrscheinlichkeit eines Bedienfehlers durch ein ungünstiges Interaktionsdesign erhöht. Andererseits ist die Nutzerschnittstelle oft nicht robust gegenüber typischen Bedienfehlern konzipiert.

Unfallanalysen zeigen, dass bestimmte Gruppen von Bedienfehlern immer den gleichen Strukturen folgen, die sich bei der Interaktion mit vielen unterschiedlichen Systemen zeigen. Hier setzt nun das Projekt VASCO an. In Zusammenarbeit mit Astrium Bremen und dem belgischen KMU Symbio sammelt und formalisiert OFFIS diese Fehlerstrukturen.

Bei der Entwicklung von neuen Mensch-Maschine-Schnittstellen soll diese formale Darstellung von Bedienfehlern genutzt werden, um bereits früh im Entwicklungsprozess Schwachstellen zu suchen, die anfällig für eben diese Fehlerarten sind. Die formale Darstellung ebnet zudem den Weg, um für die Suche automatisierte Verifikationsverfahren zu verwenden. Um das Potential dieses Vorgehen zu untersuchen, wird es innerhalb von VASCO anhand des Lebenserhaltungssystems des europäischen Columbus Moduls der Internationalen Raumstation getestet.

Formale Verifikation