• Produktbild: Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen
  • Produktbild: Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen
Band 146

Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen

Aus der Reihe Informatik-Fachberichte

54,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.09.1987

Abbildungen

VIII, mit Abbildung

Verlag

Springer Berlin

Seitenzahl

327

Maße (L/B/H)

24,4/17/1,9 cm

Gewicht

587 g

Auflage

1987

Sprache

Deutsch

ISBN

978-3-540-18320-4

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.09.1987

Abbildungen

VIII, mit Abbildung

Verlag

Springer Berlin

Seitenzahl

327

Maße (L/B/H)

24,4/17/1,9 cm

Gewicht

587 g

Auflage

1987

Sprache

Deutsch

ISBN

978-3-540-18320-4

Herstelleradresse

Springer-Verlag GmbH
Tiergartenstr. 17
69121 Heidelberg
DE

Email: GPSR Kontakt

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)

Weitere Artikel finden Sie in

  • Produktbild: Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen
  • Produktbild: Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen
  • 1 Einleitung.- 2 Grundbegriffe der Firmwareverifikation.- 2.1 Ebenen einer Rechnerarchitektur.- 2.2 Mikroprogrammierung.- 2.3 Mikroprogrammierte Rechnerarchitekturen.- 2.4 Grundlagen der axiomatischen Verifikation von Firmware.- 3 Entwurf mikroprogrammierter Rechnerarchitekturen.- 3.1 Formale Beschreibung von Rechnerarchitekturen.- 3.1.1 Grundkonzepte von AADL.- 3.1.2 Formale Beschreibung von Mikroarchitekturen.- 3.1.3 Spezifikation von Zielarchitekturen.- 3.2 Die S*-Familie höherer Mikroprogrammiersprachen.- 3.3 Hierarchischer Entwurf von Rechnerarchitekturen.- 3.3.1 Grundprinzipien des hierarchischen Entwurfs mikroprogrammierter Rechnerarchitekturen.- 3.3.2 Die Speicherabbildung.- 3.3.3 Modifikation der hierarchischen Entwurfsmethode.- 4 Verifikation mikroprogrammierter Rechnerarchitekturen.- 4.1 Die Generierung der axiomatischen Spezifikation einer Operation.- 4.1.1 Die schwächste ableitbare Vorbedingung einer Operation.- 4.1.2 Die axiomatische Spezifikation einer Operation.- 4.1.3 Die Einbindung der axiomatischen Spezifikation als Anforderung an die Implementierung.- 4.2 Eine axiomatische Definition der S*-Familie.- 4.2.1 Axiomatisierung von Mikrooperationen.- 4.2.2 Konfliktanalyse in Mikroarchitekturen und ihre Einbettung in Beweisregeln für die parallele Ausführung von Mikrooperationen.- 4.2.3 Axiomatisierung prozessorabhängiger Kontrollstrukturen von S*.- 4.2.4 Axiomatisierung prozessorunabhängiger Kontrollstrukturen und der Dokumentationsbefehle von S*.- Zusammenfassung.- Danksagung.- Fußnoten.- Al Anhang 1.- A1.1 Spezifikation der Makroarchitektur der NOVA 1200.- A1.2 Formale Beschreibung der Mikroarchitektur der MICRODATA 1600.- A1.3 Definition der Zwischenarchitektur.- A2 Anhang 2.- Die Syntax von S*.- A3 Anhang 3.- Konfliktanalyse zwischen dynamischen Speicherausdrücken.- A4 Anhang4 : Ein Beispielbeweis.- A4.1 Diskussion des Beweises.- A4.2 Schematische Darstellung des Beweises.- A4.3 Berechnung der schwächsten Vorbedingung.- A4.4 Einige Vereinfachungsregeln.- Stichwortverzeichnis.- Verzeichnis der Abbildungen.