Manuel Gesell

• Embedded systems, ranging from very simple systems up to complex controllers, may nowadays have quite challenging real-time requirements. Many embedded systems are reactive systems that have to respond to environmental events and have to guarantee certain real-time constrain. Their execution is usually divided into reaction steps, where in each step, the system reads inputs from the environment and reacts to these by computing corresponding outputs. The synchronous Model of Computation (MoC) has proven to be well-suited for the development of reactive real-time embedded systems whose paradigm directly reflects the reactive nature of the systems it describes. Another advantage is the availability of formal verification by model checking as a result of the deterministic execution based on a formal semantics. Nevertheless, the increasing complexity of embedded systems requires to compensate the natural disadvantages of model checking that suffers from the well-known state-space explosion problem. It is therefore natural to try to integrate other verification methods with the already established techniques. Hence, improvements to encounter these problems are required, e.g., appropriate decomposition techniques, which encounter the disadvantages of the model checking approach naturally. But defining decomposition techniques for synchronous language is a difficult task, as a result of the inherent parallelism emerging from the synchronous broadcast communication. Inspired by the progress in the field of desynchronization of synchronous systems by representing them in other MoCs, this work will investigate the possibility of adapting and use methods and tools designed for other MoC for the verification of systems represented in the synchronous MoC. Therefore, this work introduces the interactive verification of synchronous systems based on the basic foundation of formal verification for sequential programs – the Hoare calculus. Due to the different models of computation several problems have to be solved. In particular due to the large amount of concurrency, several parts of the program are active at the same point of time. In contrast to sequential programs, a decomposition in the Hoare-logic style that is in some sense a symbolic execution from one control flow location to another one requires the consideration of several flows here. Therefore, different approaches for the interactive verification of synchronous systems are presented. Additionally, the representation of synchronous systems by other MoCs and the influence of the representation on the verification task by differently embedding synchronous system in a single verification tool are elaborated. The feasibility is shown by integration of the presented approach with the established model checking methods by implementing the AIFProver on top of the Averest system.
• Eingebette Systeme reichen von sehr einfachen Systemen zu sehr komplexen Steuerungen, und haben meist extreme Echtzeit- und Planungsanforderungen. Viele Eingebettete Systeme sind reaktive Systeme, die auf Ereignisse der Umgebung reagieren müssen und dabei bestimmte zeitliche Vorgaben erfüllen müssen. Die Ausführung solcher Systeme wird normalerweise in Reaktionsschritte unterteilt, wobei in jedem Schritt das System seine Eingaben liest und auf diese mit den entsprechenden Ausgaben reagiert. Das synchrone Berechnungsmodel (MoC) ist geeignet solche Systeme zu modellieren, da es dem Paradigma der perfekten Synchronie folgt, welches die Natur der reaktiven Systeme wiederspiegelt. Ein weiterer Vorteil ist das Vorhandensein von formalen Verifikationsmethoden, wie Modelprüfung. Die Anwendbarkeit dieser Methoden basiert auf der deterministischen Ausführung solcher Systeme, aufgrund der formalen Semantik. Durch die steigende Komplexität von Eingebetteten Systemen muss der natürliche Nachteil der Modellprüfung, die Zustandsraumexplosion, ausgeglichen werden um akzeptable Laufzeiten des Verifikationsverfahren sicher zu stellen. Dafür werden meist bestehende Techniken wiederverwendet. Vor allem Methoden, die den Zustandsraum durch z.B. Zerlegung verkleinern und damit dem Nachteil der Modellprüfung entgegenwirken sind wichtig. Die Definition solcher Dekompositionstechniken ist für synchrone Sprachen, durch deren Parallelität nicht einfach. Inspiriert durch die Erfolge im Gebiet der Desynchronisation von synchronen Systemen, welche diese in asynchrone Systeme transformieren, wird diese Arbeit die Möglichkeit untersuchen, ob ähnliche Techniken auch für die Verifikation verwendet werden können. Dabei werden Techniken betrachtet, die ein anderes Berechnungsmodell zu Grunde legen und eine mögliche Verwendung für die Verifikation synchroner Systeme untersucht. Dabei wird der Schwerpunkt auf die interaktive Verifikation synchroner Systeme, basierend auf dem Hoare- Kalkül, einer grundlegenden Verifikationstechnik sequentieller Programme gelegt. Durch die verschiedenen zugrundeliegenden Berechnungsmodelle muss eine vielzahl an Problemen gelöst werden. Besonders problematisch ist die Möglichkeit, dass verschiedene Programmteile zum gleichen Zeitpunkt aktiv sein und sich gegenseitig beeinflussen können. Im Gegensatz zum sequentiellen Fall, bei dem man einzelne Anweisungen betrachtet, bedeutet eine Dekomposition synchroner Programme, dass man eine symbolische Ausführung von mehreren parallelen Programteilen betrachten muss. Zum Lösen dieses Problems werden verschiedene Ansätze gezeigt. Außerdem wird gezeigt wie ein synchrones System durch andere Berechnungsmodelle zum Zwecke der Verifikation dargestellt werden kann und welchen Einfluß dies auf dessen Verifikation hat. Die Realisierbarkeit der vorgestellten Ansätze wird durch die Integration mit den vorhandenen Modellprüfungsmethoden durch die Implementierung eines Prototyps gezeigt.