tailieunhanh - Digitale Hardware/ Software-Systeme- P8

Digitale Hardware/ Software-Systeme- P8: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 | 202 5 Eigenschaftsprüfung Definition Beschränkte Semantik von LTL-Formeln mit Schleife . Sei M eine temporale Struktur mit Anfangszustand s0. Sei ferner k e Z 0 und s eine k-Schleife. Dann ist eine LTL-Formel p gültig entlang des Pfades s s0 s1 . mit Schranke k geschrieben M s k p genau dann wenn M s p. Handelt es sich bei s hingegen nicht um eine k-Schleife muss die Semantik approximiert werden. Betrachtet wird die LTL-Formel F p. Diese Formel ist nur gültig entlang des Pfades s wenn ein i e Z 0 existiert so dass s p. Mit anderen Worten Es muss ein Suffix von s existieren so dass der Anfangszustand dieses Suffixes p erfüllt. Wird der Präfix der Lange k 1 betrachtet so besitzt der Zustand sk allerdings keinen Nachfolgezustand so dass sich die Semantik nicht rekursiv über Suffixe definieren lasst. Um dies zu umgehen wird der Parameter i zur Definition der Semantik hinzugenommen und dafür k als Symbol verwendet. Dabei beschreibt i die momentane Position in der Sequenz und k die verwendete Schranke. Definition Beschränkte Semantik von LTL-Formeln ohne Schleife . Sei M eine temporale Struktur mit Anfangszustand s0. Sei ferner k e Z 0 und s ein Pfad der keine k-Schleife ist. Dann ist eine LTL-Formel p gültig entlang des Pfades s s0 s1 . mit Schranke k geschrieben M s k p genau dann wenn M s 0 p wobei M s k p o p e L si falls p e V M s k -p o p e L si falls p e V M s k p V y o M s k p oder M s k y m sr k p A y o M s k p und M s k y M s k X p o i k und M s k 1 p M s k G p o gilt niemals M s k p U y o Ji j k M s k yAVi n j M s k p M s k p R y o Ji j k M s k pAVi n j M s k y Falls s keine k-Schleife ist so ist G p ungültig in der beschrankten Semantik da nicht sichergestellt werden kann dass p in sk 1 weiterhin gilt. Aus dem selben Grund muss aus der Definition des R-Operators der Fall ausgeschlossen werden bei dem y immer erfüllt ist aber p niemals. Diese Beschränkungen heben auch die Dualitat der Operatoren G und F -F p G -p sowie U und R - p U y -p R -y auf.