Specification and verification of mobile real-time systems

Abstract

In dieser Arbeit wird eine formale Methode, die Logik Shape Calculus, zur Beschreibung und Verifikation von Systemen vorgestellt, deren Beschreibung sowohl Aussagen über den zeitlichen Ablauf als auch die räumliche Konfiguration der Komponenten erfordert. Es wird gezeigt, dass die Logik im Allgemeinen unentscheidbar ist. Es werden zwei entscheidbare Teilklassen angeben. Eine Teilklasse wird durch Einschränkung auf endliche diskrete Räume gewonnen. Die zweite Teilklasse durch syntaktische Einschränkung der Formelklasse. Für die erste Teilklasse existiert ein automatisches Verifikationswerkzeug. Die Anwendung dieses Werkzeugs wird anhand eines Fallbeispiels demonstriert, das mit Methoden, die nur die zeitlichen Aspekte betrachten nicht untersucht werden kann.