An Integration of Z and Timed CSP
for Specifying Real-Time Embedded Systems
vorgelegt von
Diplom-Informatiker
Carsten S¨
uhl
aus Berlin
Von der Fakult¨
at IV - Elektrotechnik und Informatik
der Technischen Universit¨
at Berlin
zur Erlangung des akademischen Grades
Doktor der Ingenieurwissenschaften
- Dr.-Ing. -
genehmigte Dissertation
Promotionsausschuss:
Vorsitzender: Prof. Dr.-Ing. Martin Buss
Berichter: Prof. Dr.-Ing. Stefan J¨
ahnichen
Berichterin: Prof. Dr. rer. nat. Maritta Heisel
Tag der wissenschaftlichen Aussprache: 17. Dezember 2002
Berlin 2002
D 83
Zusammenfassung
Fortschritte in der Entwicklung der Hardwaretechnologie haben zu einem Vordringen von
Software in neue Anwendungsbereiche und zu ihrem Einsatz zur L¨
osung immer komplexe-
rer Probleme gef¨
uhrt. Dies trifft insbesondere auf den Bereich eingebetteter Systeme zu.
Viele eingebettete Systeme, vor allem im Bereich der Prozesskontrolle, sind sicherheitskri-
tisch, d.h. sie stellen eine potentielle Gefahr f¨
ur das Eigentum oder sogar das Leben von
Menschen dar. Weil von solchen Systemen ein hoher Grad an Zuverl¨
assigkeit verlangt wird,
besitzt die Verwendung formaler Techniken in diesem Anwendungsbereich im Vergleich
zu nicht sicherheitskritischen Systemen, bei denen ihr ad¨
aquater Einsatz lediglich zu einer
allgemeinen Qualit¨
atsverbesserung f¨
uhrt, ein noch gr¨
oßeres Potential. Trotz dieser Vorz¨
uge
besitzen die etablierten formalen Spezifikationssprachen verschiedene Restriktionen, welche
ihre N¨
utzlichkeit f¨
ur die Entwicklung eingebetteter Systeme einschr¨
anken. Unter anderem
diese Erkenntnis hat dazu gef¨
uhrt, dass sich das Forschungsgebiet der ”Integration formaler
Methoden“ in j¨
ungster Zeit wachsenden Interesses erfreut.
Die vorliegende Arbeit hat eine solche Integration von zwei formalen Techniken, der mo-
dellbasierten Notation Z und der Echtzeitprozessalgebra Timed-CSP, zum Gegenstand. Z
ist eine verbreitete Notation zur Spezifikation datenbezogener Eigenschaften transformatio-
neller Systeme, jedoch nicht zur Modellierung von Verhaltensaspekten geeignet. Timed-CSP
hingegen, eine Erweiterung der Prozessalgebra CSP um Echtzeit, erm¨
oglicht die Definition
von Verhalten inklusive Echtzeitaspekten, unterst¨
utzt allerdings nicht die Modellierung von
Datentypen. Ziel dieser Arbeit ist die Ausnutzung der St¨
arken der beiden komplement¨
aren
Formalismen im Rahmen eines Integrationsformalismus’, der als RT-Z bezeichnet wird. RT-
Z unterst¨
utzt den Entwicklungsprozess in verschiedenen Phasen — von der Anforderungs-
spezifikation ¨
uber den Architektur- bis zum Detailentwurf — und erlaubt eine koh¨
arente,
formale Spezifikation aller relevanten Aspekte eines eingebetteten Echtzeitsystems.
Im Folgenden seien die vier wesentlichen Charakteristika von RT-Z skizziert.
Zur Ausnutzung der oben genannten Vorz¨
uge formaler Techniken ist RT-Z vollst¨
andig for-
mal fundiert, was die Syntax, die Semantik und den Verfeinerungsbegriff, der die Grundlage
des Prozesses der schrittweisen Entwicklung von Spezifikationen bildet, einschließt.
Die meisten eingebetteten Systeme bestehen aus einer Vielzahl stark interdependenter Kom-
ponenten. Um diese inh¨
arente Komplexit¨
at bew¨
altigen zu k¨
onnen, stellt RT-Z eigene, formal
fundierte Strukturierungskonzepte bereit. Dies ist notwendig, weil beide Basisformalismen
nicht ¨
uber ad¨
aquate Strukturierungsmechanismen verf¨
ugen.
Weiterhin unterst¨
utzt RT-Z sowohl die Anforderungs- als auch die Entwurfsphasen. RT-Z
verf¨
ugt zu diesem Zweck ¨
uber Sprachkonstrukte auf verschiedenen Abstraktionsebenen:
abstrakte Konstrukte zur Spezifikation von Anforderungen, ohne dabei gleichzeitig Imple-
mentierungsdetails festzulegen, und konkrete Konstrukte zur Festlegung solcher Implemen-
tierungsdetails im Entwurf.
Schließlich ist eine herausragende Zielsetzung bei der Integration etablierter Techniken die
Wiederverwendbarkeit ihrer Infrastruktur, z.B. Werkzeuge. RT-Z ist als ”konservierende In-
tegration“ konzipiert und stellt einen optimalen Kompromiss zwischen oben genannter Wie-
derverwendbarkeit und der Koh¨
arenz der Teile einer Spezifikation dar.
Die Eignung von RT-Z — im Vergleich zu anderen Formalismen — f¨
ur den anvisierten An-
wendungsbereich folgt aus dem Zusammenwirken der Gesamtheit dieser Eigenschaften.
I
II
Acknowledgements
First of all, I would like to thank my advisers. Stefan J¨
ahnichen, who employed me as a PhD
student at GMD FIRST, gave me the freedom to develop my own research interests and to
choose my PhD topic. Also, the opportunity to work in interesting projects allowed me to
gain insight into current research issues. Maritta Heisel, who introduced me to research, sup-
ported my work from the beginning and provided me with important advice and feedback
for developing this thesis.
I am also grateful to my colleagues from the software engineering groups at Fraunhofer
FIRST (formerly GMD FIRST) and the Technical University of Berlin for their interest and
support. Matthias Anlauff, Jochen Burghardt, Steffen Helke, Stephan Herrmann, Florian
Kamm¨
uller, Jeff Sanders, Thomas Santen, Dirk Seifert, Graeme Smith and Kirsten Winter
helped me obtain an understanding of formal methods and software engineering in general.
They allowed me to benefit from their expertise and experience.
Thomas Santen deserves special thanks for relieving me in the QUASAR project during the
final stage of my dissertation as far as possible, allowing me to finish the work presented in
this thesis.
I am particularly grateful to Graeme Smith for reading the long chapter dealing with the
semantics of RT-Z and for giving me important advice how to make the definition of the
semantics conforming to my informal description of RT-Z.
Many thanks to Jochen Burghardt, who assisted me in improving the overview of timed CSP.
Discussions with Jan Brederecke helped me improve my understanding of and clear some
misconceptions concerning CSP-OZ.
Last, but not least, Wolfgang Grieskamp’s tool ZETA was extremely useful for typesetting
and checking the formal definitions.
III
Loading more pages...