Đang chuẩn bị liên kết để tải về tài liệu:
Digitale Hardware/ Software-Systeme- P14

Digitale Hardware/ Software-Systeme- P14:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf | 384 7 Software-Verifikation Abb. 7.7. ADDGfüra Programm 1 und b Programm 2 aus Beispiel 7.1.10 Beispiel 7.1.13. Für Programm 1 aus Beispiel 7.1.10 ergibt sich die Ausgabe-zu-Eingabe-Abbildung für die Variablen c und b unter ausschließlicher Berücksichtigung des rechten Pfades im ADDG in Abb. 7.7a zu M c b Mc tmp3 o Mtmp3 tmp2 O Mtmp2 b d1 d I d1 3 k A d2 k 2 A 128 k 256 A k Z Aquivalenzpriifung Zur Aquivalenzpriifung von zwei C-Programmen muss gezeigt werden dass beide Programme die selben Ausgaben für die selben Eingaben erzeugen. Unter der Annahme dass beide Programme die selben Eingabe- und Ausgabevariablen besitzen kann die Prüfung in zwei Schritten durchgeführt werden. Dazu müssen die folgenden zwei Bedingungen auf ihre Gültigkeit überprüft werden 1. Die Menge der Ausgabe-zu-Eingabe-Abbildungen ist die selbe für beide Programme. 7.1 Formale Äquivalenzprüfung eingebetteter Software 385 2. Die Berechnungen der beiden Programme sind identisch. Zusammen garantieren diese beiden Bedingungen dass die Ausgaben beider Programme durch die selben Berechnungen auf den selben Eingabedaten entstehen. Da die ADDGs der beiden Programme Abstraktionen der Berechnungen der Programme darstellen kann die Aquivalenzprüfung auch mit Hilfe der ADDGs erfolgen. Dabei werden die ADDGs der beiden Programme synchron von den Ausgabevariablen hin zu den Eingabevariablen traversiert. Die gesamte Aquivalenzprufung von zwei C-Programmen ist nochmals in Abb. 7.8 zu sehen. Abb. 7.8. Äquivalenzprüfung zweier C-Programme mittels ÄDDGs 395 Zunächst wird die Traversierung der ADDGs für Programme gezeigt die lediglich ein Propagieren von Ausdrücken und Schleifentransformationen zur Optimierung verwendet haben. Die synchrone Traversierung der ADDGs beginnt an korrespondierenden Knoten der ADDGs welche die selben Ausgabevariablen reprasen-tieren. Die Abhangigkeitsabbildung wird für beide Knoten mit der Identitatsfunktion initialisiert. Anschließend werden die beiden ADDGs synchron von den .