Sie sind hier
E-Book

Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme

AutorDavid Trachtenherz
VerlagVieweg+Teubner (GWV)
Erscheinungsjahr2010
Seitenanzahl431 Seiten
ISBN9783834897039
FormatPDF
KopierschutzDRM
GerätePC/MAC/eReader/Tablet
Preis64,99 EUR
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.

Kaufen Sie hier:

Horizontale Tabs

Leseprobe
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.
Inhaltsverzeichnis
Geleitwort6
Danksagung7
Kurzfassung8
Abstract10
Inhaltsverzeichnis12
Abbildungsverzeichnis14
Tabellenverzeichnis16
Kapitel 1 Einleitung18
1.1 Motivation18
1.2 Zielsetzung und Ergebnisse21
1.3 Gliederung der Arbeit23
1.4 Verwandte Arbeiten24
Kapitel 2 Logische Architektur36
2.1 Begriffsdefinitionen36
2.2 Anforderungen an Architekturbeschreibungsmittel39
2.3 Entwurfsentscheidungen auf Grundlage der Anforderungsanalyse40
Kapitel 3 Formale Grundlagen45
3.1 Nachrichtenstrombasierte Spezifikation45
3.1.1 Grundbegriffe45
3.1.2 Ströme50
3.1.3 Stromverarbeitenden Funktionen56
3.2 Temporale Logik57
3.2.1 Zeitbegriff und Zeitdomäne58
3.2.2 Grundbegriffe linearer Temporallogik64
3.3 Grundlagen des Arbeitens mit Isabelle/HOL67
3.3.1 Grundlagen67
3.3.2 Notation71
3.3.3 Beweistaktiken74
3.3.4 Weitere Hilfsmittel86
Kapitel 4 Grundlagen eigenschaftsorientierter Architekturbeschreibung92
4.1 ADL – Strukturbeschreibung und operationale Verhaltensbeschreibung92
4.1.1 Modellierungstechnik92
4.1.2 Formale Semantik98
4.2 PDL – Deklarative Beschreibung funktionaler Eigenschaften129
4.2.1 Basis-PDL130
4.2.2 Beziehung zwischen Basis-PDL und Mehrtaktsemantik149
4.3 ADL+PDL – Integration struktureller und dynamischer Beschreibungsmittel157
4.3.1 CCL-Notation für strukturelle Eigenschaften157
4.3.2 Integration funktionaler Notationen in CCL162
Kapitel 5 Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation177
5.1 Integrierte Darstellung struktureller und funktionaler Spezifikation178
5.2 Tabellarische Spezifikation funktionaler Eigenschaften182
5.3 Graphische Veranschaulichung funktionaler Eigenschaften190
Kapitel 6 Eigenschaftsorientierte Architekturmuster205
6.1 Spezifikation und Anwendung205
6.2 Komposition219
6.3 Abstraktionsebenen232
Kapitel 7 Fallstudie246
7.1 Schnittstelle und informale Spezifikation246
7.2 Formale funktionale Spezifikation251
7.3 Strukturelle und funktionale Verfeinerung266
Kapitel 8 Zusammenfassung und Ausblick283
8.1 Zusammenfassung283
8.2 Zukünftige Arbeiten288
Anhang A Ströme und temporale Logik in Isabelle/HOL297
A.1 Ströme von Nachrichten301
A.1.1 Expansion von Strömen301
A.1.2 Kompression von Strömen303
A.1.3 Stromverarbeitung310
A.2 Temporale Logik auf Intervallen333
A.2.1 Schnittoperatoren auf Intervallen/Mengen333
A.2.2 Induktion über beliebige natürliche Intervalle/Mengen334
A.2.3 Intervalle für temporale Logik337
A.2.4 Arithmetische Operatoren auf Intervallen341
A.2.5 Temporallogische Operatoren auf Intervallen natürlicher Zahlen351
A.2.6 Nachrichtenströme und temporale Operatoren auf Intervallen356
A.2.7 Temporale Operatoren und Stromverarbeitung durch beschleunigte Komponenten363
A.3 Fallstudie377
A.3.1 LTL – Definition und Validierung377
A.3.2 Benutzerdefinierte PDL – Definition und Validierung379
A.3.3 Funktionale Eigenschaften der ACC-Komponente382
Anhang B Glossar395
B.1 Abkürzungen395
B.2 Mathematische und logische Ausdrücke397
B.3 Ströme399
Literaturverzeichnis401
Sachverzeichnis435

Weitere E-Books zum Thema: Sicherheit - IT Security

Sicherheit im Online-Banking

E-Book Sicherheit im Online-Banking
PIN/TAN und HBCI im magischen Dreieck aus Sicherheit, Kosten und einfacher Bedienbarkeit Format: PDF

Das Buch unterzieht den aktuellen Stand der Sicherungsverfahren im Online-Banking einer kritischen Analyse. Neben den verschiedenen PIN/TAN-Verfahren und HBCI werden im Ausblick auch andere Systeme…

Hacking für Manager

E-Book Hacking für Manager
Was Manager über IT-Sicherheit wissen müssen. Die Tricks der Hacker. Format: PDF

Die Technik, die uns heute überschwemmt, lässt uns gar keine Chance mehr, alles so abzusichern, dass wir auch wirklich sicher sind. Lernen Sie die Waffen Ihrer Gegner und Ihre eigenen…

Sicherheitsforschung

E-Book Sicherheitsforschung
Chancen und Perspektiven - acatech DISKUTIERT  Format: PDF

Wissenschaft und Technik dienen dazu, das Grundbedürfnis nach Sicherheit zu befriedigen. Weil aber der Sicherheitsbegriff nicht einheitlich verwendet wird, sind Modelle und Lösungskonzepte zur…

Datenschutz von A-Z

E-Book Datenschutz von A-Z
Schnell und kompakt informiert zum Datenschutz Format: PDF

In diesem kompakten Taschenlexikon können Sie die wichtigsten Fragen zum Datenschutz einfach nachschlagen. Alle Begriffe werden umfassend und verständlich erklärt: Von Auftragsdatenverarbeitung über…

Sicherheitsforschung

E-Book Sicherheitsforschung
Chancen und Perspektiven - acatech DISKUTIERT  Format: PDF

Wissenschaft und Technik dienen dazu, das Grundbedürfnis nach Sicherheit zu befriedigen. Weil aber der Sicherheitsbegriff nicht einheitlich verwendet wird, sind Modelle und Lösungskonzepte zur…

Sicherheitsforschung

E-Book Sicherheitsforschung
Chancen und Perspektiven - acatech DISKUTIERT  Format: PDF

Wissenschaft und Technik dienen dazu, das Grundbedürfnis nach Sicherheit zu befriedigen. Weil aber der Sicherheitsbegriff nicht einheitlich verwendet wird, sind Modelle und Lösungskonzepte zur…

Mobile Anwendungen in Unternehmen

E-Book Mobile Anwendungen in Unternehmen
Konzepte und betriebliche Einsatzszenarien Format: PDF

Das Buch vermittelt umfassende Kenntnisse über den Einsatz von mobilen Anwendungen in Unternehmen. Die Autoren stellen sowohl Grundlagen als auch Konzepte dar, um betriebliche Einsatzszenarien zu…

ExPDT

E-Book ExPDT
Vergleichbarkeit von Richtlinien für Selbstregulierung und Selbstdatenschutz Format: PDF

Dr. Martin Kähmer promovierte bei Prof. Dr. Günter Müller am Institut für Informatik und Gesellschaft der Albert-Ludwigs-Universität Freiburg.

Webserver Security

E-Book Webserver Security
Format: PDF

Studienarbeit aus dem Jahr 2011 im Fachbereich Informatik - IT-Security, Universität Augsburg, Veranstaltung: Internetsicherheit, Sprache: Deutsch, Abstract: In der vorliegenden Arbeit werden zu…

Weitere Zeitschriften

Augenblick mal

Augenblick mal

Die Zeitschrift mit den guten Nachrichten "Augenblick mal" ist eine Zeitschrift, die in aktuellen Berichten, Interviews und Reportagen die biblische Botschaft und den christlichen Glauben ...

Berufsstart Bewerbung

Berufsstart Bewerbung

»Berufsstart Bewerbung« erscheint jährlich zum Wintersemester im November mit einer Auflage von 50.000 Exemplaren und ermöglicht Unternehmen sich bei Studenten und Absolventen mit einer ...

Burgen und Schlösser

Burgen und Schlösser

aktuelle Berichte zum Thema Burgen, Schlösser, Wehrbauten, Forschungsergebnisse zur Bau- und Kunstgeschichte, Denkmalpflege und Denkmalschutz Seit ihrer Gründung 1899 gibt die Deutsche ...

dima

dima

Bau und Einsatz von Werkzeugmaschinen für spangebende und spanlose sowie abtragende und umformende Fertigungsverfahren. dima - die maschine - bietet als Fachzeitschrift die Kommunikationsplattform ...

e-commerce magazin

e-commerce magazin

PFLICHTLEKTÜRE – Seit zwei Jahrzehnten begleitet das e-commerce magazin das sich ständig ändernde Geschäftsfeld des Online- handels. Um den Durchblick zu behalten, teilen hier renommierte ...

Euphorion

Euphorion

EUPHORION wurde 1894 gegründet und widmet sich als „Zeitschrift für Literaturgeschichte“ dem gesamten Fachgebiet der deutschen Philologie. Mindestens ein Heft pro Jahrgang ist für die ...