Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-579
Main Title: An Integration of Z and Timed CSP for Specifying Real-Time Embedded Systems
Translated Title: Eine Integration von Z und Timed-CSP zur Spezifikation eingebetteter Echtzeitsysteme
Author(s): Sühl, Carsten
Advisor(s): Jähnichen, Stefan
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Software übernimmt in eingebetteten Systemen zunehmend komplexere Funktionen, die bislang z.B. durch mechanische oder elektrische Komponenten realisiert wurden. Für die Entwicklung solcher Komponenten existieren etablierte Techniken, die auf umfangreichen, in Jahrzehnten gewonnenen Erfahrungen basieren. Der Ersatz konventioneller Komponenten durch Software in eingebetteten Systemen führt zu neuen softwaretechnischen Problemstellungen. Viele eingebettete Systeme, vor allem im Bereich der Prozesskontrolle, sind sicherheitskritisch, d.h. sie stellen eine potentielle Gefahr für das Eigentum oder sogar das Leben von Menschen dar. Weil von solchen Systemen ein hoher Grad an Zuverlässigkeit verlangt wird, besitzt die Verwendung formaler Techniken in diesem Anwendungsbereich im Vergleich zu nicht sicherheitskritischen Systemen, bei denen ihr adäquater Einsatz lediglich zu einer allgemeinen Qualitätsverbesserung führt, ein noch größeres Potential. Trotz dieser Vorzüge besitzen die etablierten formalen Spezifikationssprachen verschiedene Restriktionen, welche ihre Nützlichkeit für die Entwicklung eingebetteter Systeme einschränken. Unter anderem diese Erkenntnis hat dazu geführt, dass sich das Forschungsgebiet der "Integration formaler Methoden" in jüngster Zeit wachsenden Interesses erfreut. Die vorliegende Arbeit hat eine solche Integration von zwei formalen Techniken, der modellbasierten Notation Z und der Echtzeitprozessalgebra Timed-CSP, zum Gegenstand. Z ist eine verbreitete Notation zur Spezifikation datenbezogener Eigenschaften transformationeller Systeme, jedoch nicht zur Modellierung von Verhaltensaspekten geeignet. Timed-CSP hingegen, eine Erweiterung der Prozessalgebra CSP um Echtzeit, ermöglicht die Definition von Verhalten inklusive Echtzeitaspekten, unterstützt allerdings nicht die Modellierung von Datentypen. Ziel dieser Arbeit ist die Ausnutzung der Stärken der beiden komplementären Formalismen im Rahmen eines Integrationsformalismus', der als RT-Z bezeichnet wird. RT-Z unterstützt den Entwicklungsprozess in verschiedenen Phasen - von der Anforderungsspezifikation über den Architektur- bis zum Detailentwurf - und erlaubt eine kohärente, 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üge formaler Techniken ist RT-Z vollständig formal 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 Komponenten. Um diese inhärente Komplexität bewältigen zu können, stellt RT-Z eigene, formal fundierte Strukturierungskonzepte bereit. Dies ist notwendig, weil beide Basisformalismen nicht über adäquate Strukturierungsmechanismen verfügen. Weiterhin unterstützt RT-Z sowohl die Anforderungs- als auch die Entwurfsphasen. RT-Z verfügt zu diesem Zweck über Sprachkonstrukte auf verschiedenen Abstraktionsebenen: abstrakte Konstrukte zur Spezifikation von Anforderungen, ohne dabei gleichzeitig Implementierungsdetails festzulegen, und konkrete Konstrukte zur Festlegung solcher Implementierungsdetails 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 Integration" konzipiert und stellt einen optimalen Kompromiss zwischen oben genannter Wiederverwendbarkeit und der Kohärenz der Teile einer Spezifikation dar. Die Eignung von RT-Z - im Vergleich zu anderen Formalismen - für den anvisierten Anwendungsbereich folgt aus dem Zusammenwirken der Gesamtheit dieser Eigenschaften.
URI: urn:nbn:de:kobv:83-opus-4816
http://depositonce.tu-berlin.de/handle/11303/876
http://dx.doi.org/10.14279/depositonce-579
Exam Date: 17-Dec-2002
Issue Date: 31-Jan-2003
Date Available: 31-Jan-2003
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Integration formaler Techniken
eingebettete Systeme
Echtzeit
Z
Timed-CSP
Integrating formal techniques
embedded systems
real-time
Z
timed CSP
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_36.pdf2.09 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.