Slicing integrated formal specifications for verification / Ingo Brückner [original]

Slicing Integrated Formal

Specifications for Verification

Dissertation

zur Erlangung des Grades eines

Doktors der Naturwissenschaften

der Fakult¨

at f¨

ur Elektrotechnik, Informatik und Mathematik

der Universit¨

at Paderborn

vorgelegt von

Dipl.-Inform. Ingo Br¨

uckner

Oldenburg, 11. M¨

arz 2008

Mitglieder der Promotionskommission:

•Prof. Dr. Heike Wehrheim (Vorsitzende, Gutachterin)

•Prof. Dr. Ernst-R¨

udiger Olderog (Gutachter)

•Prof. Dr. Stefan B¨

ottcher

•Prof. Dr. Wilhelm Sch¨

afer

•Dr. Theodor Lettmann

Eingereicht: 18. Dezember 2007

Tag der m¨

undlichen Pr¨

ufung: 11. M¨

arz 2008

Abstract

Safety-critical electronic systems are becoming increasingly complex and simulta-

neously 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 spec-

ifications 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 re-

spect 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.

Acorrectness 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.

Zusammenfassung

Sicherheitskritische elektronische Systeme werden immer komplexer und gleichzei-

tig immer allgegenw

artiger. Wie andere Ingenieurwissenschaften muss auch die

Informatik gangbare Herangehensweisen anbieten, um den korrekten Entwurf sol-

cher Systeme zu gew

ahrleisten. Besonders wichtig innerhalb des Entwurfsprozesses

ist die Phase der initialen Spezifikation, da ihre Ergebnisse Auswirkungen auf alle

nachfolgenden Entwicklungsschritte haben. Die umfassendste und zuverl

assigste

Analyse von Systemspezifikationen kann durch die Verwendung formaler Methoden

erreicht werden, die es durch den Einsatz automatischer Verifikationstechniken

erm¨

oglichen, einen mathematischen Beweis der Systemkorrektheit zu erhalten.

Im Bereich der formalen Spezifikation gibt es jedoch keine einzelne universell ein-

setzbare Notation, die gleichermaßen geeignet f

ur alle Aspekte von Systemen w

are.

Stattdessen werden integrierte formale Methoden erforscht, die unterschiedliche

Spezifikationssprachen kombinieren, um ihre individuellen St

arken auszunutzen

und gleichzeitig eine gemeinsame semantische Basis f

ur die anschließende Ve-

rifikation 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

achliche Hindernis f

ur die erfolgreiche Anwendung automatischer

Verifikationsmethoden ist jedoch das Problem der Explosion des Zustandsraums,

also der exponentiellen Vergr

oßerung der Anzahl der zu analysierenden System-

zust

ande. Zahlreiche Techniken zur Bew

altigung 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 inte-

grierter formaler Spezifikationen entwickelt, die maßgeschneidert f

ur die reichhal-

tige syntaktische Struktur von CSP-OZ-DC-Spezifikationen ist, und die gleichzeitig

im Rahmen ihrer Verifikation bez

uglich Realzeitanforderungen einsetzbar ist. Der

Slicing-Ansatz besteht im Wesentlichen aus drei Schritten: Erstens wird die Spezi-

fikation im Hinblick auf verschiedene Typen von Abh

angigkeiten zwischen ihren

syntaktischen Elementen analysiert, wobei mehrere neue Abh¨

angigkeitstypen wie

Synchronisations- und Zeitabh

angigkeit definiert werden. Zweitens wird die Ge-

samtheit dieser Abh

angigkeiten genutzt, um diejenigen Teile der Spezifikation zu

identifizieren, die relevant f

ur die gegebene Verifikationseigenschaft sind. Drittens

wird der Slice der Spezifikation berechnet, also eine reduzierte Version der vollen

Loading more pages...