An Integration of Z and Timed CSP for Specifying Real-Time Embedded Systems

dc.contributor.advisorJähnichen, Stefanen
dc.contributor.authorSühl, Carstenen
dc.contributor.grantorTechnische Universität Berlin, Fakultät IV - Elektrotechnik und Informatiken
dc.date.accepted2002-12-17
dc.date.accessioned2015-11-20T15:13:03Z
dc.date.available2003-01-31T12:00:00Z
dc.date.issued2003-01-31
dc.date.submitted2003-01-31
dc.description.abstractSoftware ü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.de
dc.identifier.uriurn:nbn:de:kobv:83-opus-4816
dc.identifier.urihttp://depositonce.tu-berlin.de/handle/11303/876
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-579
dc.languageEnglishen
dc.language.isoenen
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subject.ddc004 Datenverarbeitung; Informatiken
dc.subject.otherIntegration formaler Technikende
dc.subject.othereingebettete Systemede
dc.subject.otherEchtzeitde
dc.subject.otherZde
dc.subject.otherTimed-CSPde
dc.subject.otherIntegrating formal techniquesen
dc.subject.otherembedded systemsen
dc.subject.otherreal-timeen
dc.subject.otherZen
dc.subject.othertimed CSPen
dc.titleAn Integration of Z and Timed CSP for Specifying Real-Time Embedded Systemsen
dc.title.translatedEine Integration von Z und Timed-CSP zur Spezifikation eingebetteter Echtzeitsystemede
dc.typeDoctoral Thesisen
dc.type.versionpublishedVersionen
tub.accessrights.dnbfree*
tub.affiliationFak. 4 Elektrotechnik und Informatikde
tub.affiliation.facultyFak. 4 Elektrotechnik und Informatikde
tub.identifier.opus3481
tub.identifier.opus4486
tub.publisher.universityorinstitutionTechnische Universität Berlinen
Files
Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
Dokument_36.pdf
Size:
2.04 MB
Format:
Adobe Portable Document Format
Description:
Collections