 |
| | | | | Beschreibung | | Die Voraussetzung für die  Programm-Verifikation ist eine Spezifikation der Vor- und Nachbedingungen (pre- und post conditions) des Programms bzw. von Teilen davon. Solche Bedingungen stellen logische Aussagen dar, die bei jedem möglichen Programmdurchlauf an den betreffenden Stellen den Wahrheitswert "True" liefern müssen. Aus den Vor- und Nachbedingungen und dem vorliegenden Quellcode lassen sich mithilfe eines Verifikationswerkzeugs sog. Verifikationsbedingungen (verification conditions) ableiten, von deren Erfüllung die Korrektheit des Programms abhängt.
Die Verifikation lässt sich aus Aufwandsgründen zumeist nicht "flächendeckend" auf mittlere bis große Programme anwenden, dennoch kann die Sicherheit eines Programms beträchtlich erhöht werden, wenn Kernalgorithmen formal verifiziert werden. Hierbei können Verifikationssysteme wertvolle Hilfestellung bei der Herstellung zuverlässiger Software liefern.
Liggesmeyer führt in [ Lig02 ] an, dass formale Verifikationswerkzeuge von professionellen Werkzeuganbietern kaum zur Verfügung gestellt werden. Die Mehrzahl der formalen Verifikationswerkzeuge stammt aus dem universitären Bereich, wodurch die Nutzung für die praktische Software-Entwicklung eingeschränkt ist. Auf der anderen Seite gibt es Anwendungsbereiche, in denen bestimmte Verifikationstechniken eine gewisse Bedeutung besitzen. Hierbei kann die Entwicklung eingebetteter Software im sicherheitskritischen Umfeld als Beispiel genannt werden.
In der jüngeren Vergangenheit verzeichnen vor allem die automatenbasierten Techniken und die darauf basierenden formalen Verifikationsverfahren eine starke Bedeutungszunahme. An erster Stelle ist das Symbolic Model Checking zu nennen, welches dazu dient, Eigenschaften von Zustandsautomaten nachzuweisen. Derartige Verfahren sind vor allem dort von Bedeutung, wo Zustandsautomaten ein wichtiges Beschreibungsmittel sind (z.B. in der Automatisierungs- und Steuerungstechnik).
In der praktischen Anwendung gestattet es Symbolic Model Checking, extrem große Zustandsräume in die Untersuchung einzubeziehen. Die Zustandsräume werden dabei in der Regel effizient dargestellt. Als Darstellungsmittel für Zustandsautomaten haben sich Ordered Binary Decision Diagrams (OBDDs) etabliert. Die Eigenschaften, die von den Zustandsautomaten gefordert werden, werden in der Regel in temporaler Logik angegeben. Üblich ist dabei die Formulierung von Sicherheits- und Lebendigkeitseigenschaften. Sicherheit äußert sich in der Nichterreichbarkeit gefährlicher (unsicherer) Zustände. Lebendigkeit bedeutet, dass ein bestimmter Zustand immer wieder erreicht wird. Der Nachweis der Eigenschaften erfordert die Durchsuchung des kompletten Zustandsraumes. Die setzt bei großen Zustandsräumen effiziente Algorithmen voraus, die in modernen Werkzeugen realisiert sind. | |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | Programm-Verifikation | | | | | | Literaturhinweise | | | | | | | | | | Glossar | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
