Jähnichen, StefanSühl, Carsten2015-11-202003-01-312003-01-312003-01-31urn:nbn:de:kobv:83-opus-4816https://depositonce.tu-berlin.de/handle/11303/876http://dx.doi.org/10.14279/depositonce-579Software ü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.en004 Datenverarbeitung; InformatikIntegration formaler Technikeneingebettete SystemeEchtzeitZTimed-CSPIntegrating formal techniquesembedded systemsreal-timeZtimed CSPDoctoral Thesis