TAILIEUCHUNG - Digitale Hardware/ Software-Systeme- P17

Digitale Hardware/ Software-Systeme- P17: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 | 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

Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.