Abstract | Modelchecking ist ein Verfahren, um Eingenschaften eines Systems zu verifizieren, indem der Zustandsraum des Systems vollständig untersucht wird. Für viele reale Systeme, insbesondere für Softwaresysteme, wird dieser Zustandraum sehr groß. Dies macht die Analyse des Zustandsraums schnell zu aufwendig, selbst dann, wenn symbolische Darstellungen verwendet werden, um Systeme und Zustandsmengen zu repräsentieren.
Um solche Systeme dennoch analysieren zu können, kann vom konkreten System abstrahiert werden, indem jeweils mehrere, konkrete Zustände zu einem abstrakten Zustand zusammengefasst werden. Eine Transition zwischen zwei abstrakten Zuständen ist üblicherweise dann möglich, wenn eine entsprechende konkrete Transition existiert.
Predicate-Abstraction ist eine Technik um Abstraktionen zu beschreiben und zu berechnen. Um die Abstraktion zu beschreiben wird eine Menge von Prädikaten über die Zustandsvariablen eines konkreten Systems verwendet. Ein abstrakter Zustand legt dann für jedes Prädikat fest, ob die zugehörigen, konkreten Zustände das Prädikate erfüllen oder nicht erfüllen müssen. Ein Prädikat teilt den Zustandsraum in eine Menge von konkreten Zuständen, die das Prädikat erfüllen, und in eine Menge von Zuständen, die das Prädikat nicht erfüllen. Die Schnittmengen für alle Prädikate entsprechen dann den abstrakten Zuständen.
Um die abstrakten Transitionen zu bestimmen, wird mit Hilfe eines Theorembeweisers überprüft, ob aus den Prädikaten des einen, abstrakten Zustandes und der Transitionsrelation des Systems folgt, dass ein konkreter Zustand des anderen, abstrakten Zustandes durch eine konkrete Transition erreichbar ist.
Auf den so erzeugten, abstrakten Systemen wird dann Modelchecking durchgeführt. Schlägt die Verifikation der gewünschten Eigenschaft fehl, wird ein Ablauf im abstrakten System bestimmt, der die Eigenschaft verletzt. Dann wird zunächst überprüft, ob ein entsprechender Ablauf auch im konkreten System existiert. Ist dies nicht der Fall, muss die Abstraktion verbessert werden. Dies wird üblicherweise erreicht, indem abstrakte Zustände so aufgeteilt werden, dass der abstrakte Ablauf nicht mehr existiert.
Solche Abstraktionen zeigen mehr Verhalten, als das konkrete System, d.h. es sind mehr Abläufe möglich, als im konkreten System tatsächlich auftreten. Aus diesem Grund eignen sich solche Abstraktionen nicht, um die Existenz von Abläufen zu verifizieren, es ist lediglich möglich zu überprüfen, dass alle Abläufe bestimmte Eigenschaften erfüllen. Außerdem kann die Verifikation einer Eigenschaft fehlschlagen, obwohl sie das konkrete System erfüllt. Daher ist es notwendig zu überprüfen, ob ein unzulässiger, abstrakter Ablauf auch tatsächlich einem konkreten Ablauf entspricht. Um Ausagen über die Exisitenz von Abläufen machen zu können, muss man so abstrahieren, dass höchstens weniger Abläufe möglich sind. Man kann jedoch nicht so abstrahieren, dass beide Fälle abgedeckt sind.
Drei-wertige, abstrakte System unterscheiden zwischen abstrakten ?-Transitionen, für die es lediglich mindestens eine konkrete Transition gibt, und !-Transitionen, für die es für jeden konkreten Anfangszustand eine entsprechende Transition gibt. Auf diesen Systemen ist es möglich, gleichzeitig Eigenschaften von allen Abläufen und die Existenz von Abläufen zu verifizieren. Wenn eine Eigenschaft für das abstrakte System nicht gilt, ist es zudem sicher, dass sie auch für das konkrete System nicht gilt. Schlägt die Verifikation fehl, so kann das auf ?-Transitionen des abstrakten Systems zurückgeführt werden und die Abstraktion muss so angepasst werden, dass diese ?-Transitionen entfallen.
Im Rahmen dieser Arbeit wurde Predicate-Abstraction so angepasst, dass solche drei-wertigen Systeme zur Abstraktion verwendet werden können. Außerdem wurde symbolisches Modelchecking auf drei-wertige Systeme übertragen und um ein Verfahren ergänzt, dass die ?-Transitionen findet, die dazu führen, dass die Verifikation einer Eigenschaft fehl schlägt. Um diese ?-Transitionen aus dem abstrakten System zu entfernen, wurde ein Abstraction-Refinement-Verfahren entwickelt, das entsprechend neue Prädikate generiert.
Diese Verfahren wurden zudem prototypisch implementiert. Dazu wurden die Theorembeweiser Yices und Z3 verwendet und eine einfache Modellierungssprache entworfen.
|