Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen
Dieses Buch stellt eine Methodik zum systematischen Entwurf korrekter Mikroprogramme vor. Behandelt werden sämtliche Phasen der Firmwareentwicklung: das Erstellen einer formalen Beschreibung der Anforderungen, Techniken zur hierarchischen Organisation des Entwurfs, die Mikroprogrammierung in einer g...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | German |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
1987, 1987
|
| Edition: | 1st ed. 1987 |
| Series: | Informatik-Fachberichte
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 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.2 Die S*-Familie höherer Mikroprogrammiersprachen
- 3.3 Hierarchischer Entwurf von Rechnerarchitekturen
- 4 Verifikation mikroprogrammierter Rechnerarchitekturen
- 4.1 Die Generierung der axiomatischen Spezifikation einer Operation
- 4.2 Eine axiomatische Definition der S*-Familie
- 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