tailieunhanh - Digitale Hardware/ Software-Systeme- P25

Digitale Hardware/ Software-Systeme- P25: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. | 474 8 Systemverifikation Die Übergangsmarkierungsfunktion LR R 2Vr gibt an für welchen Zustandsübergang welches Ereignis v e VR gilt. Dies ist gleichbedeutend mit Das Ereignis LR s s gilt beim Zustandsubergang s s wobei Lr s s v A v veLR s s ve Vr Lr s s Daneben kann jede SE-LTL-Formel p über Vs und VR auch als LTL-Formel pLTL über VS U VR interpretiert werden. Dabei sind p und pLTL syntaktisch identisch unterscheiden sich aber semantisch. Da jede LTS mit Definition als Buchi-Automat interpretiert werden kann kann wie im Fall der LTL-Modellprüfung der Produktautomat aus einer LTS und einem Buchi-Automaten gebildet werden. Sei B Sb RB LB AB ein Buchi-Automat mit Anfangszustanden Sb q und M S R Ls LR eine attributierte temporale Struktur mit Anfangszustanden So. Der Buchi-Automat verwendet die atomaren Aussagen VB Vs Mp M0B Sp Rp Lp Ap ist definiert durch Sp s sB e S x Sb Ls s 3VR LB sB dies beschreibt die Formel LB sB in der alle Variablen v e VR existentiell quantifiziert wurden s sb s1 sB e Rp genau dann wenn 3v e Vr s - s1 A sb s B e Rb A Ls s ALr s s Lb sb und s sB e Ap genau dann wenn sB e AB. Die Anfangszustande ergebenen sich aus den Paaren der Anfangszustande beider Automaten. Da SE-LTL-Formeln syntaktisch identisch mit LTL-Formeln sind lassen sich SE-LTL-Formeln als Buchi-Automaten modellieren. Somit kann nun die SE-LTL-Modellprüfung wie die LTL-Modellprüfung als Test auf eine leere Sprache des Produktautomaten umformuliert werden. Theorem . Fur eine LTS M und eine SE-LTL-Formel p gilt M p T M0B-pLTL 0 Die Sprache des Produktautomaten ist definiert wie in Abschnitt beschrieben. Abstraktion Neben der oben beschriebenen Abbildung von SystemC-Modellen auf parallele Kompositionen von LTS lassen sich weitere Abstraktionen durchführen welche die Verifikationszeit verkürzen können. Hardware Software-Partitionierung Durch Hardware Software-Partitionierung kann die Modellkomplexitat deutlich reduziert werden. Hierzu werden die