Trachtenherz Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme

1. Auflage 2010
ISBN: 978-3-8348-9703-9
Verlag: Vieweg & Teubner
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Deutsch, 431 Seiten, eBook

David Trachtenherz entwickelt einen Lösungsansatz zur eigenschaftsorientierten Beschreibung der logischen Architektur eingebetteter Systeme, der eine präzise deklarative Spezifikation funktionaler Eigenschaften mit wählbarem Grad der Abstraktion für unterschiedliche Entwicklungsphasen und -ebenen ermöglicht.

Dr. David Trachtenherz promovierte bei Prof. Dr. Dr. h. c. Manfred Broy am Institut für Informatik der Technischen Universität München.

Zielgruppe

Research

Autoren/Hrsg.

Trachtenherz, David

Inhaltsverzeichnis

1;Geleitwort;6
2;Danksagung;7
3;Kurzfassung;8
4;Abstract;10
5;Inhaltsverzeichnis;12
6;Abbildungsverzeichnis;14
7;Tabellenverzeichnis;16
8;Kapitel 1 Einleitung;18
8.1;1.1 Motivation;18
8.2;1.2 Zielsetzung und Ergebnisse;21
8.3;1.3 Gliederung der Arbeit;23
8.4;1.4 Verwandte Arbeiten;24
9;Kapitel 2 Logische Architektur;36
9.1;2.1 Begriffsdefinitionen;36
9.2;2.2 Anforderungen an Architekturbeschreibungsmittel;39
9.3;2.3 Entwurfsentscheidungen auf Grundlage der Anforderungsanalyse;40
10;Kapitel 3 Formale Grundlagen;45
10.1;3.1 Nachrichtenstrombasierte Spezifikation;45
10.1.1;3.1.1 Grundbegriffe;45
10.1.2;3.1.2 Ströme;50
10.1.3;3.1.3 Stromverarbeitenden Funktionen;56
10.2;3.2 Temporale Logik;57
10.2.1;3.2.1 Zeitbegriff und Zeitdomäne;58
10.2.2;3.2.2 Grundbegriffe linearer Temporallogik;64
10.3;3.3 Grundlagen des Arbeitens mit Isabelle/HOL;67
10.3.1;3.3.1 Grundlagen;67
10.3.2;3.3.2 Notation;71
10.3.3;3.3.3 Beweistaktiken;74
10.3.4;3.3.4 Weitere Hilfsmittel;86
11;Kapitel 4 Grundlagen eigenschaftsorientierter Architekturbeschreibung;92
11.1;4.1 ADL – Strukturbeschreibung und operationale Verhaltensbeschreibung;92
11.1.1;4.1.1 Modellierungstechnik;92
11.1.2;4.1.2 Formale Semantik;98
11.2;4.2 PDL – Deklarative Beschreibung funktionaler Eigenschaften;129
11.2.1;4.2.1 Basis-PDL;130
11.2.2;4.2.2 Beziehung zwischen Basis-PDL und Mehrtaktsemantik;149
11.3;4.3 ADL+PDL – Integration struktureller und dynamischer Beschreibungsmittel;157
11.3.1;4.3.1 CCL-Notation für strukturelle Eigenschaften;157
11.3.2;4.3.2 Integration funktionaler Notationen in CCL;162
12;Kapitel 5 Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation;177
12.1;5.1 Integrierte Darstellung struktureller und funktionaler Spezifikation;178
12.2;5.2 Tabellarische Spezifikation funktionaler Eigenschaften;182
12.3;5.3 Graphische Veranschaulichung funktionaler Eigenschaften;190
13;Kapitel 6 Eigenschaftsorientierte Architekturmuster;205
13.1;6.1 Spezifikation und Anwendung;205
13.2;6.2 Komposition;219
13.3;6.3 Abstraktionsebenen;232
14;Kapitel 7 Fallstudie;246
14.1;7.1 Schnittstelle und informale Spezifikation;246
14.2;7.2 Formale funktionale Spezifikation;251
14.3;7.3 Strukturelle und funktionale Verfeinerung;266
15;Kapitel 8 Zusammenfassung und Ausblick;283
15.1;8.1 Zusammenfassung;283
15.2;8.2 Zukünftige Arbeiten;288
16;Anhang A Ströme und temporale Logik in Isabelle/HOL;297
16.1;A.1 Ströme von Nachrichten;301
16.1.1;A.1.1 Expansion von Strömen;301
16.1.2;A.1.2 Kompression von Strömen;303
16.1.3;A.1.3 Stromverarbeitung;310
16.2;A.2 Temporale Logik auf Intervallen;333
16.2.1;A.2.1 Schnittoperatoren auf Intervallen/Mengen;333
16.2.2;A.2.2 Induktion über beliebige natürliche Intervalle/Mengen;334
16.2.3;A.2.3 Intervalle für temporale Logik;337
16.2.4;A.2.4 Arithmetische Operatoren auf Intervallen;341
16.2.5;A.2.5 Temporallogische Operatoren auf Intervallen natürlicher Zahlen;351
16.2.6;A.2.6 Nachrichtenströme und temporale Operatoren auf Intervallen;356
16.2.7;A.2.7 Temporale Operatoren und Stromverarbeitung durch beschleunigte Komponenten;363
16.3;A.3 Fallstudie;377
16.3.1;A.3.1 LTL – Definition und Validierung;377
16.3.2;A.3.2 Benutzerdefinierte PDL – Definition und Validierung;379
16.3.3;A.3.3 Funktionale Eigenschaften der ACC-Komponente;382
17;Anhang B Glossar;395
17.1;B.1 Abkürzungen;395
17.2;B.2 Mathematische und logische Ausdrücke;397
17.3;B.3 Ströme;399
18;Literaturverzeichnis;401
19;Sachverzeichnis;435

Logische Architektur.- Formale Grundlagen.- Grundlagen eigenschaftsorientierter Architekturbeschreibung.- Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation.- Eigenschaftsorientierte Architekturmuster.- Fallstudie.- Zusammenfassung und Ausblick.

Leseproben

Kapitel 8 Zusammenfassung und Ausblick (S. 266-267)

In der vorliegenden Arbeit befassten wir uns mit Beschreibungsmitteln für die logische Architektur von Softwaresystemen mit besonderem Hinblick auf eingebettete Systeme im Automobilbereich. Nun wollen wir ein Fazit ziehen. In dem Abschnitt 8.1 werden die Ergebnisse der Arbeit zusammengefasst. In dem Abschnitt 8.2 geben wir einen Ausblick auf zukünftige Arbeiten zur Weiterentwicklung der erarbeiteten Ergebnisse.

8.1 Zusammenfassung

Der Schwerpunkt der Arbeit lag auf der Entwicklung von Konzepten und Mitteln zur eigenschaftsorientierten Beschreibung der logischen Architektur eingebetteter Systeme, die neben der strukturellen und operationalen Systemspezi?kation die formal fundierte Spezi?kation funktionaler Eigenschaften in frühen Systementwicklungsphasen (insbesondere Grob- und Feinentwurf) mit wählbarem Abstraktionsgrad und unabhängig von einer operationalen Verhaltensspezi?kation ermöglichen.

Diese formale Spezi?kation kann im weiteren Verlauf der Systementwicklung zum einen als präzise Schnittstellenbeschreibung der Systemkomponenten dienen, und zum anderen zur frühen formalen Veri?kation bestimmter Systemeigenschaften noch vor der operationalen Implementierung des Systems verwendet werden, und damit zur Qualitätssicherung bereits zu einem Zeitpunkt, zu dem konventionelle Qualitätssicherung durch Testverfahren noch nicht möglich ist.

Ein wichtiger Vorteil dieser beiden Aspekte gegenüber informalen oder semi-formalen Spezi?kationsmitteln ist, dass sie zwar eine grundsätzlich präzisere Vorgehensweise bei der Systementwicklung möglich machen, sie jedoch nicht fest vorschreiben, sondern vielmehr neue Wege eröffnen, die zusätzlich zur traditionellen Entwicklung verfügbar sind:

• Eine formale Spezi?kation funktionaler Eigenschaften kann zusätzlich zur konventionellen informalen Spezi?kation durch Texte/Diagramme verwendet werden. Die formale und informale Spezi?kation ergänzen in diesem Fall einander: während die formale Spezi?- kation die Missverständnisse und fehlende Präzision der informalen ausräumt, dient die informale als Kommentar zur formalen Spezi?kation, die ihr Verständnis erleichtert.

• Eine formale Spezi?kation kann zur Unterstützung der konventionellen Qualitätssicherungsverfahren verwendet werden, beispielsweise durch Generierung von Testfällen aus einer deklarativen funktionalen Spezi?kation.

• Eine formale Spezi?kation kann schließlich zur formalen Veri?kation ausgewählter Systemeigenschaften verwendet werden. Dabei können je nach Form der formalen Spezi?kation sowie Entwicklungsstand des Systems unterschiedliche Veri?kationsverfahren (beispielsweise Theorembeweisen, Modelchecking, SAT-Solving u. v. m.) eingesetzt werden.

Die oben aufgeführten Möglichkeiten, die durch eine formale Spezi?kation funktionaler Eigenschaften eröffnet werden, können je nach Anforderungen an das zu entwickelnde System und insbesondere an die zu erzielende Qualität unabhängig voneinander für das Gesamtsystem oder ausgewählte Teilsysteme sowie für ausgewählte Aspekte des Verhaltens angewendet werden, so dass die formale Spezi?kation ?exibel in verschiedenen Ausbaustufen mit Hinblick auf den Spezi?kations- sowie gegebenenfalls Veri?kationsaufwand und die angestrebte Systemqualität eingesetzt werden kann.

Über Autor(innen)

Dr. David Trachtenherz promovierte bei Prof. Dr. Dr. h. c. Manfred Broy am Institut für Informatik der Technischen Universität München.