tailieunhanh - Digitale Hardware/ Software-Systeme- Part 12

Digitale Hardware/ Software-Systeme- P12: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. | 212 5 Eigenschaftsprüfung Mengen an Zuständen in denen p bzw. q gilt. Die Funktion COMPUTE_EU 0 berechnet die Zustände welche die TCTL-Formel E p U o q erfüllen. Das sind diejenigen Zustände von denen aus ein Pfad s existiert der einen Zustand in Sq erreicht und der auf dem Pfad nur Zustande aus Sp enthalt. Zusatzlich muss die Latenz A dieses Pfades A s 0 sein. Somit kann die Funktion COMPUTE_EU 0 wie folgt definiert werden COMPUTE_EU 0 M Sp Sq Sn 0 DO Sr Sn Sa s e S 3s e Sn s s1 e R Sn Sq U Sp n Sa UNTIL Sn Sr RETURN Sn Die Funktion COMPUTE_EG 0 berechnet die Zustande welche die TCTL-Formel EG 0 p erfüllen. Das sind diejenigen Zustande die einen Pfad s besitzen der lediglich Zustande aus Sp beinhaltet und bei dem alle Zustandsübergange die Zeit 8 0 haben. Mit anderen Worten Es wird die Verfolgung eines Pfades abgebrochen sobald ein Zustandsübergang mit 8 0 auftritt. COMPUTE_EG 0 M Sp Sn S DO Sr Sn Sa s e S 3s e Sn 8 0 s1 e R Sn Sp n Sa UNTIL Sn Sr RETURN SN Mit Hilfe der Funktionen COMPUTE_EU 0 und COMPUTE_EG 0 lassen sich nun allgemeinere Zeitaspekte überprüfen. Diese lassen sich durch die Formeln E p UM q und EG 1u p formulieren. Dabei beschreiben 1 u Zeitintervalle innerhalb derer die Latenz liegen muss. Im Folgenden wird lediglich die Funktion COMPUTE_EU ljü naher betrachtet welche diejenigen Zustande s e S ermittelt die Prafix eines Pfades s sind der lediglich mit p markierte Zustande enthalt und dessen letzter Zustand mit q markiert ist. Für die Latenz dieses Pfades s gilt 1 A s u. Die maximale Verzogerungszeit eines Zustandsübergangs sei dabei 8max. COMPUTE_EU ljü M Sp Sq 1 u w u -1 1 i 0 IF w 0 V u 0 RETURN F Prüfung nichtfunktionaler Eigenschaften 213 FOR j 1 j min w Smax j j 1 SA COMPUTE_EU o M S s e S Hs e S s s Si j COMPUTE_EU o M Sp Sq n Sa FOR j w 1 j 8 j j 1 Si j 0 SI 8max 1 0 SN COMPUTE_EU o M Sp Sq Sr Sn FOR i 1 i u i i 1 FOR j 1 j 8 j j 1 Sa s e S Hs e Sr s - i s1 Si j Si j 1 U COMPUTE_EU o Sp Sq nSa SR Si 1 IF i w Sr Sr U Sn RETURN Sr .