Fehlerfreie Medizinsoftware
Von der Vision zur Wirklichkeit
Fortsetzung des Artikels von Teil 1
Anforderungen an Verifikation und Validierung
Gemeinsam ist allen Safety-Normen und Regulierungen im Software-Bereich, dass sie die Identifikation funktionaler und nicht-funktionaler Gefahrenstellen fordern sowie den Nachweis, dass die Software die relevanten Sicherheitsziele erfüllt. Dies gilt ohne Einschränkung auch für den Bereich der Medizinsoftware, auch wenn der Detailgrad der Anforderungsbeschreibung deutlich hinter anderen Industrienormen liegt. Es müssen die Codierrichtlinien eingehalten werden, die das Risiko von Programmierfehlern minimieren. Verbreitete Standards sind insbesondere MISRA C [18], SEI CERT C [19], ISO/TS 17951 [20] und CWE (Common Weakness Enumeration) [21]. Eine automatisierte Prüfung durch Softwarewerkzeuge (zum Beispiel Absint RuleChecker [22]) hat sich in sicherheitskritischen Industriebereichen als fester Teil des Entwicklungsprozesses durchgesetzt. Zum Korrektheitsnachweis für funktionale Programmeigenschaften haben sich automatische und modellbasierte Testverfahren neben formalen Methoden wie Model Checking etabliert. Bei der Systemkorrektheit spielen jedoch auch sicherheitsrelevante nicht-funktionale Qualitätseigenschaften eine wichtige Rolle. Es ist offensichtlich, dass ein Programm nicht wegen Speicherfehlern abstürzen darf, und dass die Reaktionen von Echtzeitsoftware innerhalb der vorgegebenen Zeit erfolgen müssen. Die Folgen nicht-funktionaler Fehler können schwerwiegend sein – bekannte Beispiele sind die Explosion der Ariane 5 [23], die unbeabsichtigte Beschleunigung im Toyota Camry [24] und die fehlerhafte Strahlendosisberechnung beim Therac-25 Unfall [25].
Die Überprüfung nicht-funktionaler Programmeigenschaften durch Testverfahren ist problematisch. Tests und Messungen können prinzipiell nicht die Abwesenheit von Fehlern beweisen. Erschwerend kommt hinzu, dass keine spezifischen Testfälle zur Stimulation der maximalen Laufzeit oder des maximalen Stackverbrauchs zur Verfügung stehen. Auch die Bestimmung sinnvoller Testendekriterien für Eigenschaften wie Timing, Stackverbrauch oder das Auftreten von Laufzeitfehlern wie Division durch Null oder arithmetische Überläufe stellt ein ungelöstes Problem dar. Der Testprozesss für nicht-funktionale Softwareanforderungen ist dementsprechend nicht fokussiert; der erforderliche Testaufwand hoch und die Testabdeckung unvollständig.
Statische Analyse durch Abstrakte Interpretation
In den letzten Jahren haben sich statische Analysatoren auf Basis der Abstrakten Interpretation zum Stand der Technik bei der Verifikation nicht-funktionaler Eigenschaften entwickelt. Ein statischer Analysator ist ein Softwarewerkzeug, das zur Ermittlung der Analyseergebnisse keine Ausführung des untersuchten Programmes benötigt. Die sogenannten sicheren statischen Analysatoren, die auf der Theorie der Abstrakten Interpretation basieren, zählen zu den formalen Verifikationsmethoden. Abstrakte Interpretation ist eine semantikbasierte Methodik für Programmanalysen [26]. Sie ermöglicht volle Kontroll- und Datenabdeckung und kann einen formalen Nachweis von Programmeigenschaften erbringen. Die sogenannten False Negatives, also übersehene Fehler, sind ausgeschlossen. Statische Analysen können leicht automatisiert und in den Entwicklungsprozess integriert werden, und sie ermöglichen es, Fehler in frühen Entwicklungsphasen zu entdecken. Moderne statische Analysatoren skalieren gut und erlauben die Analyse vollständiger sicherheitskritischer Industrieanwendungen [27]. Abstrakte Interpretation eignet sich sehr gut, um nicht-funktionale Softwarefehler auszuschließen. Beispiele sind sichere statische Analysatoren zum Nachweis der maximalen Ausführungszeit und des maximalen Stackverbrauchs von Tasks sowie zum Ausschluss des Auftretens von Laufzeitfehlern und Datenwettläufen [28].
Stacküberläufe ausschließen
Stacküberläufe können schwerwiegende Fehler verursachen, die zu fehlerhaften Programmausführungen oder zu Abstürzen führen können. Sie können die Datenintegrität zerstören und damit unerwünschte Interferenzen zwischen Softwarekomponenten verursachen. Das Tool StackAnalyzer [29] von Absint berechnet zum Beispiel, wie die Stackhöhe entlang der verschiedenen Kontrollpfade zu- und abnimmt. Diese Information wird dazu verwendet, den maximalen Stackverbrauch einer Task zu berechnen, womit sich die Abwesenheit von Stacküberläufen beweisen lässt [30].
- Von der Vision zur Wirklichkeit
- Anforderungen an Verifikation und Validierung
- Nachweis der Echtzeitfähigkeit
Lesen Sie mehr zum Thema
