Konstruktion und Überprüfung von Beweisen auf Abstrakten Zustandsmaschinen

Abstrakte Zustandsmaschinen (ASMs) werden häufig für die Formalisierung und Verifikation der Semantik von Software oder Hardware verwendet.
Es fehlt jedoch an Werkzeugen, die diesen Prozess bei iterativ entwickelten Spezifikationen unterstützen. Mit iterativer Entwicklung bezeichne ich das Hinzufügen von Erweiterungen in jeder Iteration ohne Refactoring. Das Ziel ist ein Werkzeug zu schaffen, das die Verifikation von iterativ entwickelten Spezifikationen unterstützt. Der Ansatz besteht darin, ASM-Spezifikationen in die Sprache eines bestehenden Proof-Checkers zu übersetzen und Beweise weitesgehend automatisch zu konstruieren und mit dem Proof-Checker zu überprüfen. Außerdem sollen Beweise von iterativ entwickelten Spezifikationen auch iterativ entwickelt sein.

Construction and checking of proofs on Abstract State Machines

Abstract State Machines (ASMs) are widely used in the formalization and verification of the semantics of software or hardware. However, tools for assisting this process for evolving specifications are still lacking. With evolving we denote adding extensions without refactoring. We want to create a tool assisting in the verification of evolving specifications. Our approach is to translate ASM specifications into the language of an existing proof checker, construct the proofs as far as possible automatically, and check the proofs with the proof checker. Further, we want proofs of evolvable specifications also to be evolvable.