Suchen und Finden
Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme
von: David Trachtenherz
Vieweg+Teubner (GWV), 2010
ISBN: 9783834897039 , 431 Seiten
Format: PDF, OL
Kopierschutz: Wasserzeichen
Preis: 64,99 EUR
Mehr zum Inhalt
Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme
Geleitwort
6
Danksagung
7
Kurzfassung
8
Abstract
10
Inhaltsverzeichnis
12
Abbildungsverzeichnis
14
Tabellenverzeichnis
16
Kapitel 1 Einleitung
18
1.1 Motivation
18
1.2 Zielsetzung und Ergebnisse
21
1.3 Gliederung der Arbeit
23
1.4 Verwandte Arbeiten
24
Kapitel 2 Logische Architektur
36
2.1 Begriffsdefinitionen
36
2.2 Anforderungen an Architekturbeschreibungsmittel
39
2.3 Entwurfsentscheidungen auf Grundlage der Anforderungsanalyse
40
Kapitel 3 Formale Grundlagen
45
3.1 Nachrichtenstrombasierte Spezifikation
45
3.1.1 Grundbegriffe
45
3.1.2 Ströme
50
3.1.3 Stromverarbeitenden Funktionen
56
3.2 Temporale Logik
57
3.2.1 Zeitbegriff und Zeitdomäne
58
3.2.2 Grundbegriffe linearer Temporallogik
64
3.3 Grundlagen des Arbeitens mit Isabelle/HOL
67
3.3.1 Grundlagen
67
3.3.2 Notation
71
3.3.3 Beweistaktiken
74
3.3.4 Weitere Hilfsmittel
86
Kapitel 4 Grundlagen eigenschaftsorientierter Architekturbeschreibung
92
4.1 ADL – Strukturbeschreibung und operationale Verhaltensbeschreibung
92
4.1.1 Modellierungstechnik
92
4.1.2 Formale Semantik
98
4.2 PDL – Deklarative Beschreibung funktionaler Eigenschaften
129
4.2.1 Basis-PDL
130
4.2.2 Beziehung zwischen Basis-PDL und Mehrtaktsemantik
149
4.3 ADL+PDL – Integration struktureller und dynamischer Beschreibungsmittel
157
4.3.1 CCL-Notation für strukturelle Eigenschaften
157
4.3.2 Integration funktionaler Notationen in CCL
162
Kapitel 5 Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation
177
5.1 Integrierte Darstellung struktureller und funktionaler Spezifikation
178
5.2 Tabellarische Spezifikation funktionaler Eigenschaften
182
5.3 Graphische Veranschaulichung funktionaler Eigenschaften
190
Kapitel 6 Eigenschaftsorientierte Architekturmuster
205
6.1 Spezifikation und Anwendung
205
6.2 Komposition
219
6.3 Abstraktionsebenen
232
Kapitel 7 Fallstudie
246
7.1 Schnittstelle und informale Spezifikation
246
7.2 Formale funktionale Spezifikation
251
7.3 Strukturelle und funktionale Verfeinerung
266
Kapitel 8 Zusammenfassung und Ausblick
283
8.1 Zusammenfassung
283
8.2 Zukünftige Arbeiten
288
Anhang A Ströme und temporale Logik in Isabelle/HOL
297
A.1 Ströme von Nachrichten
301
A.1.1 Expansion von Strömen
301
A.1.2 Kompression von Strömen
303
A.1.3 Stromverarbeitung
310
A.2 Temporale Logik auf Intervallen
333
A.2.1 Schnittoperatoren auf Intervallen/Mengen
333
A.2.2 Induktion über beliebige natürliche Intervalle/Mengen
334
A.2.3 Intervalle für temporale Logik
337
A.2.4 Arithmetische Operatoren auf Intervallen
341
A.2.5 Temporallogische Operatoren auf Intervallen natürlicher Zahlen
351
A.2.6 Nachrichtenströme und temporale Operatoren auf Intervallen
356
A.2.7 Temporale Operatoren und Stromverarbeitung durch beschleunigte Komponenten
363
A.3 Fallstudie
377
A.3.1 LTL – Definition und Validierung
377
A.3.2 Benutzerdefinierte PDL – Definition und Validierung
379
A.3.3 Funktionale Eigenschaften der ACC-Komponente
382
Anhang B Glossar
395
B.1 Abkürzungen
395
B.2 Mathematische und logische Ausdrücke
397
B.3 Ströme
399
Literaturverzeichnis
401
Sachverzeichnis
435
Alle Preise verstehen sich inklusive der gesetzlichen MwSt.