Formal methods for real-time requirements engineering

Abstract

Timed model checking turned out to be a very successful technique for the verification of real-time systems. In general, however, large-scale systems require more than a mere real-time perspective: They utilise, for example, Abstract Data Types and Fairness Aspects. VSE-II (Verification Support Environment) is a general tool which supports the design and the verification process of such large-scale systems. The basic machinery within VSE-II is theorem proving rather than model checking and one of its underlying formalisms is close to TLA (Temporal Logic of Actions), i.e. it is based on linear discrete time. In this thesis we develop a technique to perform an exact discretisation of dense real-time aspects, i.e. a discretisation that is not just an approximation but rather mirrors dense behaviour exactly. This discretisation is achieved without an explicit or implicit introduction of rational numbers. With the help of the exact discretisation we define an embedding of Hybrid Automata into VSE-II such that model checking strategies for Hybrid Automata can be used in VSE-II. Vice versa, the embedding allows the model checking strategies to benefit from the proof work done in VSE-II. This thesis introduces a general methodology for formal requirements analysis, namely observer models, that deals with particular perspectives on a system rather than with particular aspects of it. This way, different specialised approaches can be integrated and used to describe the overall system requirements. One such view, for example, is a real-time which uses a new discretisation technique.

In der Verifikation von Realzeit-Systemen haben sich Model-Checking Verfahren bewährt. Im Allgemeinen kann man jedoch sagen, dass große industrielle Anwendungen nicht nur die Realzeit Dimension aufweisen. Sie bestehen vielmehr aus einer Vielzahl weiterer Dimensionen (Sichten) wie eine Informationsflusssicht oder eine Security-Sicht. Zur Spezifikation dieser Sichten werden beispielsweise Abstrakte Datentypen oder auch Fairness Aspekte verwendet. VSE-II (Verification Support Environment) ist ein Werkzeug, welches den formalen Entwicklungsprozess vom Design bis hin zur Verifikation solcher Anwendungen unterstützt. Der Kern des VSE-IIWerkzeugs ist ein interaktives Beweissystem, das auf einem Sequenzenkalkül basiert, der neben der Logik erster Stufe und Dynamischer Logik auch die Temporale Logik der Aktionen (TLA) beinhaltet. TLA beruht auf einem Zeitmodell, welches linear und diskret ist. In dieser Arbeit beschreiben wir eine Technik, die eine exakte Diskretisierung von dichten Realzeitaspekten erlaubt, so dass das VSE-II System diese Aspekte mit den vorhandenen Verfahren und Regeln behandeln kann. Die Diskretisierung ist so definiert, dass sie nicht nur eine Approximation ist, sondern sie spiegelt vielmehr das dichte Verhalten exakt wider. Dies wird ohne die explizite oder implizite Einführung von rationalen Zahlen erreicht. Mit Hilfe der exakten Diskretisierung wird eine Einbettung von Hybriden Automaten in VSE-II definiert, die es ermöglicht Teilbeweise, die von Modelcheckingverfahren für Hybride Automaten gefunden wurden, ohne weiteren Beweis in VSE-II zu verwenden und umgekehrt. Weiterhin wird eine Methodologie zur formalen Anforderungsanalyse eingeführt, die verschiedene Sichten auf ein System und nicht nur verschiedene Aspekte eines Systems behandelt. Diese Methodologie, genannt Observer Models, ermöglicht die Integration unterschiedlicher spezieller Werkzeuge bzw. Verfahren zur Beschreibung der einzelnen Sichten und somit zur Beschreibung der gesamten Systemanforderungen. Eine solche Sicht stellt beispielsweise eine Realzeit-Sicht dar, welche auf der oben erwähnten Einbettung beruht.