English

Safety-critical electronic systems are becoming increasingly complex and simultaneously ubiquitous. As in other engineering disciplines, computer science needs to offer viable approaches to the correct design of such systems. Especially important within this design process is the phase of initial specification, since its results have impact on all subsequent stages of development. The most extensive and reliable analysis of system specifications is offered by using formal methods that allow us to obtain mathematical proofs of system correctness by applying automatic verification techniques. In the area of formal system specification there is, however, not one single general-purpose notation, that would be equally well suited for all system aspects. Instead, integrated formal methods are investigated, which combine different specification languages, exploiting their individual strengths, while still maintaining a common semantic foundation for subsequent verification. One such notation is the high-level specification language CSP-OZ-DC, combining the process algebra Communicating Sequential Processes (CSP) for expressing behavioural aspects, the state-based notation Object-Z (OZ) for expressing data aspects, and the real-time logic Duration Calculus (DC) for expressing real-time aspects of systems. The main obstacle for successful application of automatic verification, however, is the problem of state space explosion, i.e., the exponential blow-up in the number of system states to be analysed. Many techniques have been proposed to tackle this problem, one of them being the method of slicing that has its origins in the area of program analysis where it is used to compute those parts of a program that are relevant with respect to a specific analysis task. Within this thesis, we develop a slicing approach for integrated formal specifications that is custom-tailored to the rich syntactical structure of CSP-OZ-DC specifications and that is applicable in the context of their verification with respect to real-time requirements. The slicing approach essentially consists of three steps: First, the specification is analysed with respect to dependences between its syntactical elements with several new types of dependence being defined such as synchronisation and timing dependence. Second, these dependences as a whole are used to identify those specification parts that are relevant for the given verification property. Third, the specification slice is computed, i.e., a reduced version of the full specification that does not contain any elements without influence on the verification property. A correctness proof shows that verification can be carried out on the slice instead of the full original specification without changing the verification result. The proof is based on a notion of projection between a specification and its slice. The existence of such a projection relation is shown to be guaranteed by the slicing approach. The particular logic used to express verification properties is then shown to be stuttering-invariant, i.e., provided that the projection relation exists, it cannot distinguish between the slice and the original specification such that the verification result will in both cases always be the same. Furthermore, we present tool support that has been implemented for developing, slicing, and verifying CSP-OZ-DC specifications along with several case studies and experimental results for evaluating the effectiveness of the slicing approach.

Deutsch

Sicherheitskritische elektronische Systeme werden immer komplexer und gleichzeitig immer allgegenwärtiger. Wie andere Ingenieurwissenschaften muss auch die Informatik gangbare Herangehensweisen anbieten, um den korrekten Entwurf solcher Systeme zu gewährleisten. Besonders wichtig innerhalb des Entwurfsprozesses ist die Phase der initialen Spezifikation, da ihre Ergebnisse Auswirkungen auf alle nachfolgenden Entwicklungsschritte haben. Die umfassendste und zuverlässigste Analyse von Systemspezifikationen kann durch die Verwendung formaler Methoden erreicht werden, die es durch den Einsatz automatischer Verifikationstechniken ermöglichen, einen mathematischen Beweis der Systemkorrektheit zu erhalten. Im Bereich der formalen Spezifikation gibt es jedoch keine einzelne universell einsetzbare Notation, die gleichermaßen geeignet für alle Aspekte von Systemen wäre. Stattdessen werden integrierte formale Methoden erforscht, die unterschiedliche Spezifikationssprachen kombinieren, um ihre individuellen Stärken auszunutzen und gleichzeitig eine gemeinsame semantische Basis für die anschließende Verifikation aufrechtzuerhalten. Eine solche Notation ist die Spezifikationssprache CSP-OZ-DC, in der die Prozessalgebra Communicating Sequential Processes (CSP) zur Beschreibung von Verhaltensaspekten, die zustandsbasierte Notation Object-Z (OZ) zur Beschreibung von Datenaspekten und die Realzeit-Logik Duration Calculus (DC) zur Beschreibung von Realzeitaspekten von Systemen vereinigt sind. Das hauptsächliche Hindernis für die erfolgreiche Anwendung automatischer Verifikationsmethoden ist jedoch das Problem der Explosion des Zustandsraums, also der exponentiellen Vergrößerung der Anzahl der zu analysierenden Systemzustände. Zahlreiche Techniken zur Bewältigung dieses Problems wurden bereits vorgeschlagen, unter ihnen die des Slicing, das seinen Ursprung im Gebiet der Programmanalyse hat, wo es zur Berechnung derjenigen Programmteile verwendet wird, die im Hinblick auf eine bestimmte Fragestellung relevant sind. In der vorliegenden Dissertation wird eine Herangehensweise zum Slicing integrierter formaler Spezifikationen entwickelt, die maßgeschneidert für die reichhaltige syntaktische Struktur von CSPOZ-DC-Spezifikationen ist, und die gleichzeitig im Rahmen ihrer Verifikation bezüglich Realzeitanforderungen einsetzbar ist. Der Slicing-Ansatz besteht im Wesentlichen aus drei Schritten: Erstens wird die Spezifikation im Hinblick auf verschiedene Typen von Abhängigkeiten zwischen ihren syntaktischen Elementen analysiert, wobei mehrere neue Abhängigkeitstypen wie Synchronisations- und Zeitabhängigkeit definiert werden. Zweitens wird die Gesamtheit dieser Abhängigkeiten genutzt, um diejenigen Teile der Spezifikation zu identifizieren, die relevant für die gegebene Verifikationseigenschaft sind. Drittens wird der Slice der Spezifikation berechnet, also eine reduzierte Version der vollen Spezifikation, in der alle Elemente ohne Einfluss auf die Verifikationseigenschaft entfernt sind. Ein Korrektheitsbeweis zeigt, dass anstelle der ursprünglichen Spezifikation nun der Slice für eine Verifikation verwendet werden kann, ohne das Verifikationsergebnis zu verändern. Der Beweis basiert auf dem Begriff der Projektion zwischen einer Spezifikation und ihrem Slice. Es wird gezeigt, dass der entwickelte Slicing-Ansatz die Existenz einer solchen Projektionsbeziehung garantiert. Darauf aufbauend wird gezeigt, dass die jeweilige Logik zur Beschreibung von Verifikationseigenschaften stotter-invariant ist, das heißt, unter der Voraussetzung der Existenz einer Projektionsrelation kann sie nicht zwischen Slice und ursprünglicher Spezifikation unterscheiden, sodass das Verifikationsergebnis in beiden Fällen das gleiche sein wird. Schließlich wird die Werkzeugunterstützung vorgestellt, die zur Entwicklung, zum Slicing und zur Verifikation von CSP-OZ-DC-Spezifikationen implementiert wurde, ergänzt durch mehrere Fallstudien und experimentelle Ergebnisse zur Evaluierung der Effektivität des Slicing-Ansatzes.