Making Object-Z Perfect : Verifaktion von Object-Z Spezifikationen unter Verwendung von Perfect Developer

Abstract

Gerade in sicherheitskritischen Anwendungen ist die Korrektheit von Software ein maßgeblicher Faktor. Neben dem Ansatz mit statischen und dynamischen Testmethoden Fehler zu finden, kann eine formale Verifikation Fehler in der Software ausschließen. Die so durchgeführte Überprüfung bildet einen wichtigen Bestandteil festzustellen, ob Spezifikationen in sich schlüssig und korrekt sind. Eine der meist verwendeten Spezifikationssprachen ist die Z Notation. Mit ihrer objekt-orientierten Erweiterung Object-Z können auch komplexe Systeme in modularer Weise formal beschrieben werden. Die Toolunterstützung für die Verifikation oder gar eine Generierung von Programmcode beschränkt sich bislang primär auf Typüberprüfungen. Perfect Developer wurde mit dem Ziel erstellt, formale Spezifikationen automatisiert zu verifizieren, sowie Implementierungen zu validieren und daraus Code zu generieren. Die Arbeit verknüpft beide Technologien miteinander, indem Object-Z Spezifikationen automatisch nach Perfect überführt werden. Mit dieser Arbeit wird gezeigt, dass eine automatische Übersetzung der Object-Z Sprachkonstrukte in semantisch gleichwertige Konstrukte in Perfect möglich ist. Nach einer detaillierten Analyse von Syntax und Semantik der beiden Sprachen werden Regeln entwickelt, mit Hilfe derer die Sprachkonstrukte der Quell- in die Zielsprache übersetzt werden können. Bei der Ausführung ist es notwendig, die Originalspezifikation in mehreren Durchläufen zu analysieren, um alle für die Transformation relevanten semantischen Informationen in strukturierter Weise zugänglich zu machen. Anhand eines Fallbeispiels evaluieren wir die Umsetzung der Regeln. Da das entwickelte Tool auf GitHub öffentlich zur Verfügung steht, können nun gleichzeitig die Vorteile der übersichtlichen Object-Z Notation und die automatisierten Verifikationsmechanismen von Perfect genutzt werden.

Especially in security-critical applications, the correctness of software is a major factor. In addition to static and dynamic test approaches to find errors in a software or system, formal verification methods target on proving the correctness of software. It constitutes an important component of determining whether a specification is coherent and sound and is satisfied by an implementation. One of the most widely used specification languages is the Z notation. With its object-oriented extension Object-Z, it offers a possibility to formalize even complex systems in a modular manner. However, the tool support for the verification of specifications or even the generation of program code remains limited to type checking. Perfect Developer with its specification language Perfect was created with the idea of automatically verifying formal specifications, validating implementations against them and generating code. The idea of this work is to link these two technologies and to automatically convert a given Object-Z specification automatically into a Perfect specification making thus the functionalities of Perfect Developer available to the specifier. This work demonstrates that an automated translation of Object-Z language constructs into semantically equivalent constructs in Perfect is possible. After a detailed analysis of the relevant parts of the syntax and semantics of the two languages, we develop rules with the help of which the individual language constructs of the source language can be translated into the target language. It is necessary to analyze the internal representation of the original specification in several passes to obtain all the semantic information relevant to the transformation in a structured manner. With the help of a case study, we evaluate the implementation of the rules. The developed tool is available on GitHub.