Analyse des Entwicklungsstandes von Verfahren und entsprechender Tools der formalen Codeverifikation für Echtzeitsysteme

Abstract

In dieser Diplomarbeit wird der derzeitige Entwicklungsstand von Verfahren und Tools der formalen Codeverfikation von Echtzeitsystemen analysiert. Echtzeitsysteme unterliegen der Forderung nach funktionaler und zeitlicher Korrektheit. Bei der formalen Verfikation stellen zur Zeit die Komplexität, die Menge der zu modellierenden Einflußgrößen und der verhältnismässig hohe Arbeitsaufwand die größten Hindernisse für einen praktischen Einsatz dar. Die betrachteten Verfahren und Tools- von denen keines für die fromale Codeverifikation von Echtzeitsystemen in relevanter Größenordnung geeignet ist - werden anhand eines Bewertungsschemas auf ihre Brauchbarkeit hin überprüft. Die maßgeblichen Bewertungskriterien sind die Skalierbarkeit, Integrierbarkeit, Plattforminformationen, Exaktheit, Akzeptanz sowie die Wirtschaftlichkeit der Verfahren und Tools.