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

Digitale Hardware/ Software-Systeme- P4: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 | 2.4 Formale Spezifikation funktionaler Anforderungen 81 Andererseits gibt es CTL-Formeln die sich nicht in LTL formulieren lassen. Ein Beispiel hierfür ist AG EF p. Diese Formel besagt dass auf allen Pfaden von jedem Zustand aus ein Pfad existiert auf dem irgendwann p gilt. Dies lasst sich nicht in LTL ausdrücken. Schließlich gibt es Formeln die sich weder in LTL noch in CTL ausdrücken lassen. Ein solches Beispiel kann aus den beiden vorherigen Beispielen konstruiert werden AFG p V AGEF p Eine temporale Aussagenlogik die sowohl LTL-Formeln CTL-Formeln als auch deren Kombination ausdrücken kann ist CTL . Der Zusammenhang zwischen LTL CTL und CTL ist in Abb. 2.19 zu sehen. Abb. 2.19. Zusammenhang zwischen LTL CTL und CTL 457 CTL lasst sich formal definieren siehe auch 272 Definition 2.4.9 Syntax von CTL . Sei V die Menge aussagenlogischer Variablen atomare Formeln . Jede Zustandsformel ist eine zulässige CTL -Formel die Pfadformeln enthalten kann. Dabei sind Zustandsformeln und Pfadformeln wie folgt definiert Zustandsformeln - Falls p e V dann ist p eine Zustandsformel. - Falls p und y Zustandsformeln sind so sind -p und p V y ebenfalls Zustandsformeln. - Falls p eine Pfadformel ist dann ist E p eine Zustandsformel. Pfadformeln - Falls p eine Zustandsformel ist dann ist p ebenfalls eine Pfadformel. - Falls p und y Pfadformeln sind dann sind ebenfalls -p p V y X p und p U y Pfadformeln. Die Syntax von CTL besteht also aus zwei Formelklassen Zustandsformeln und Pfadformeln. Zustandsformeln können in einem Zustand der temporalen Struktur gültig sein. Die Gültigkeit von Pfadformeln hangt von einem Pfad in einer temporalen Struktur ab. Der Zusammenhang zwischen Zustands- und Pfadformeln ist in Abb. 2.20 dargestellt. Definition 2.4.10 Semantik von CTL . Sei p eine Zustandsformel. Dann besagt M s p dass p im Zustand s der temporalen Struktur M gilt. Sei y eine Pfadformel. 82 2 Spezifikation digitaler Systeme Abb. 2.20. Zustands- und Pfadformeln in CTL 272 Dann besagt M s y