Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme

Cover......Page 1
Eigenschaftsorientierte
Beschreibung der
logischen Architektur
eingebetteter Systeme......Page 4
ISBN 9783834810298......Page 5
Geleitwort......Page 7
Danksagung......Page 8
Kurzfassung......Page 10
Abstract......Page 12
Inhaltsverzeichnis......Page 14
Abbildungsverzeichnis......Page 16
Tabellenverzeichnis......Page 18
1.1 Motivation......Page 21
1.2 Zielsetzung und Ergebnisse......Page 24
1.3 Gliederung der Arbeit......Page 26
1.4 Verwandte Arbeiten......Page 27
2.1 Begriffsdefinitionen......Page 39
2.2 Anforderungen an Architekturbeschreibungsmittel......Page 42
2.3 Entwurfsentscheidungen auf Grundlage der Anforderungsanalyse
......Page 43
3.1.1 Grundbegriffe......Page 49
3.1.2 Ströme......Page 54
3.1.3 Stromverarbeitenden Funktionen......Page 60
3.2 Temporale Logik......Page 61
3.2.1 Zeitbegriff und Zeitdomäne......Page 62
3.2.2 Grundbegriffe linearer Temporallogik......Page 68
3.3.1 Grundlagen......Page 71
3.3.2 Notation......Page 75
3.3.3 Beweistaktiken......Page 78
3.3.4 Weitere Hilfsmittel......Page 90
4.1.1 Modellierungstechnik......Page 97
4.1.2 Formale Semantik......Page 103
4.2 PDL – Deklarative Beschreibung funktionaler Eigenschaften
......Page 134
4.2.1 Basis-PDL......Page 135
4.2.2 Beziehung zwischen Basis-PDL und Mehrtaktsemantik......Page 154
4.3.1 CCL-Notation für strukturelle Eigenschaften......Page 162
4.3.2 Integration funktionaler Notationen in CCL......Page 167
Kapitel 5 Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation
......Page 183
5.1 Integrierte Darstellung struktureller und funktionaler Spezifikation
......Page 184
5.2 Tabellarische Spezifikation funktionaler Eigenschaften......Page 188
5.3 Graphische Veranschaulichung funktionaler Eigenschaften
......Page 196
6.1 Spezifikation und Anwendung......Page 211
6.2 Komposition......Page 225
6.3 Abstraktionsebenen......Page 238
7.1 Schnittstelle und informale Spezifikation......Page 253
7.2 Formale funktionale Spezifikation......Page 258
7.3 Strukturelle und funktionale Verfeinerung......Page 273
8.1 Zusammenfassung......Page 291
8.2 Zukünftige Arbeiten......Page 296
Anhang A Ströme und temporale Logik in Isabelle/HOL
......Page 305
A.1.1 Expansion von Strömen......Page 309
A.1.2 Kompression von Strömen......Page 311
A.1.3 Stromverarbeitung......Page 318
A.2.1 Schnittoperatoren auf Intervallen/Mengen......Page 341
A.2.2 Induktion über beliebige natürliche Intervalle/Mengen......Page 342
A.2.3 Intervalle für temporale Logik......Page 345
A.2.4 Arithmetische Operatoren auf Intervallen......Page 349
A.2.5 Temporallogische Operatoren auf Intervallen natürlicher Zahlen......Page 359
A.2.6 Nachrichtenströme und temporale Operatoren auf Intervallen......Page 364
A.2.7 Temporale Operatoren und Stromverarbeitung durch beschleunigte Komponenten
......Page 371
A.3.1 LTL – Definition und Validierung......Page 385
A.3.2 Benutzerdefinierte PDL – Definition und Validierung......Page 387
A.3.3 Funktionale Eigenschaften der ACC-Komponente......Page 390
B.1 Abkürzungen......Page 403
B.2 Mathematische und logische Ausdrücke......Page 405
B.3 Ströme......Page 407
Literaturverzeichnis......Page 409
Sachverzeichnis......Page 443