Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme

Front Cover
Springer-Verlag, Sep 24, 2010 - Computers - 431 pages
0 Reviews
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Kapitel 1 Einleitung
1
Kapitel 2 Logische Architektur
19
Kapitel 3 Formale Grundlagen
29
Kapitel 4 Grundlagen eigenschaftsorientierter Architekturbeschreibung
76
Kapitel 5 Anschauliche Darstellung eigenschaftsorientierter Architekturspezifikation
163
Kapitel 6 Eigenschaftsorientierte Architekturmuster
191
Kapitel 7 Fallstudie
232
Kapitel 8 Zusammenfassung und Ausblick
271
Anhang A Ströme und temporale Logik in IsabelleHOL
285
Anhang B Glossar
383
Literaturverzeichnis
389
Sachverzeichnis
423
Copyright

Other editions - View all

Common terms and phrases

Abbildung Abschnitt Abstraktionsebenen ACC-Komponente ACC-Switch-Operation-eq-Activate Aggregationsfunktion aktuellen äquivalent Architekturmuster Ausführungszyklus Ausgabe Ausgabeport AUTOFOCUS beispielsweise Berechnung Beweisziel bool boolesche booleschen Operatoren BPDL CCL-Ausdruck CCL-PDL-Ausdrucks consts Darstellung Datentyp definieren definiert Definition deklarativen Disjunktion eigenschaftsorientierten Eingabe Eingabeport eingebetteter Systeme Elemente exists ext-out f-Exec-Comp trans-fun xs f-Exec-Comp-Stream trans-fun xs forall formale Semantik Funktion funktionalen Anforderungen funktionaler Eigenschaften gezeiteten gilt graphische i-Exec-Comp-Stream trans-fun input i-Exec-Comp-Stream-Acc-Output k output-fun Implikation inext Initialzustand Instanziierung int-exec internen Intervalle iprev Isabelle/HOL Konjunktion last-message Leerlaufzustand lemma length xs localState output-fun trans-fun Mehrtaktsemantik Menge mithilfe mode-eq-Inactive natürlicher Zahlen nichtleere Nachricht nomsg Notationen output-fun trans-fun input output-fun trans-fun localState Parameter PDL-Notationen PDL1 Ports Quantor Schnittstelle Semantik sowie spezifiziert State-Idle localState output-fun Strom Strukturelemente struktureller und funktionaler Syntax Syntaxbaum Systemausschnitt Tabelle Taktfaktor Teilkomponenten temporale Logik temporale Operatoren temporallogische temporallogische Notationen TPTL trans-fun xs True Tupel Variablen Verfeinerung Verhaltensspezifikation verwendet Zeitintervall Zeitpunkt Zustandsübergangsdiagramme

About the author (2010)

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

Bibliographic information