Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme - David Trachtenherz

Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme (eBook)

eBook Download: PDF
2010 | 2010
XVIII, 431 Seiten
Vieweg & Teubner (Verlag)
978-3-8348-9703-9 (ISBN)
Systemvoraussetzungen
64,99 inkl. MwSt
  • Download sofort lieferbar
  • Zahlungsarten anzeigen
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.

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

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

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.

Erscheint lt. Verlag 24.9.2010
Zusatzinfo XVIII, 431 S. 65 Abb.
Verlagsort Wiesbaden
Sprache deutsch
Themenwelt Informatik Netzwerke Sicherheit / Firewall
Informatik Software Entwicklung Software Architektur
Schlagworte Eigenschaftsorientierte Architekturmuster • Formale Spezifikation • Informatik • Logische Architektur • Modellbasierte Entwicklung • Softwarearchitektur • Softwarearchitektur und Systementwurf • Verifikation
ISBN-10 3-8348-9703-5 / 3834897035
ISBN-13 978-3-8348-9703-9 / 9783834897039
Haben Sie eine Frage zum Produkt?
PDFPDF (Wasserzeichen)
Größe: 3,4 MB

DRM: Digitales Wasserzeichen
Dieses eBook enthält ein digitales Wasser­zeichen und ist damit für Sie persona­lisiert. Bei einer missbräuch­lichen Weiter­gabe des eBooks an Dritte ist eine Rück­ver­folgung an die Quelle möglich.

Dateiformat: PDF (Portable Document Format)
Mit einem festen Seiten­layout eignet sich die PDF besonders für Fach­bücher mit Spalten, Tabellen und Abbild­ungen. Eine PDF kann auf fast allen Geräten ange­zeigt werden, ist aber für kleine Displays (Smart­phone, eReader) nur einge­schränkt geeignet.

Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen dafür einen PDF-Viewer - z.B. den Adobe Reader oder Adobe Digital Editions.
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen dafür einen PDF-Viewer - z.B. die kostenlose Adobe Digital Editions-App.

Zusätzliches Feature: Online Lesen
Dieses eBook können Sie zusätzlich zum Download auch online im Webbrowser lesen.

Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.

Mehr entdecken
aus dem Bereich
Das Praxishandbuch zu Krisenmanagement und Krisenkommunikation

von Holger Kaschner

eBook Download (2024)
Springer Fachmedien Wiesbaden (Verlag)
34,99
Methodische Kombination von IT-Strategie und IT-Reifegradmodell

von Markus Mangiapane; Roman P. Büchler

eBook Download (2024)
Springer Vieweg (Verlag)
42,99