Verifikation von Code mit hohen Anforderungen an die Zuverlässigkeit

Bei vielen Embedded Software-Projekten besteht das Hauptziel der Verifikation im Aufspüren möglichst vieler Programmfehler in möglichst kurzer Zeit. Die üblicherweise eingesetzten statischen Analyse-Tools eignen sich zwar gut zur Identifikation offensichtlicher Mängel, können aber nicht die Fehlerfreiheit des Quellcodes beweisen. Sie bieten daher keinen Schutz vor endlosen Debugging-Schleifen und einer langatmigen Code-Überprüfung. Deutlich schwerer wiegt aber, dass mit ihnen Fehler mit potenziell katastrophalen Folgen unentdeckt bleiben. Für Anwendungen, die eine hohe Zuverlässigkeit erfordern, ist dies nicht akzeptabel. PolySpace(TM) Code-Verifikationsprodukte verfolgen einen alternativen Ansatz: Sie beweisen mathematisch die Fehlerfreiheit für bestimmte Typen von Laufzeitfehlern.

Autor(en): The MathWorks GmbH

Suche: