Digitale Hardware/ Software-Systeme- P11: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. | 192 5 Eigenschaftsprüfung Monitor-Konstruktion für PSL-Zusicherungen Im Folgenden wird die Konstruktion von Monitoren für PSL-Zusicherungen für eine Teilmenge der Foundation Language von PSL beschrieben siehe Abschnitt . Die PSL-FL wird hierbei derart eingeschränkt dass die Negation von sequentiell erweiterten regularen Ausdrücken engl. sequential extended regulär expressions SEREs nicht zulassig ist. Die resultierende Sprache wird mit PSL-FL- bezeichnet. Definition PSL-FL- . Alle aussagenlogischen Formeln sind PSL-FL--Formeln. Sei r eine SERE und p1 und p2 zwei PSL-FL- -Formeln dann sind auch die folgenden Ausdrücke PSL-FL--Formeln r P1 V P2 P1 A P2 X P1 P1 U P2 P1 R P2 Man muss beachten dass der Ausschluss der Negation keinen Einfluss auf die Expressivitat von LTL-Formeln hat die keine SEREs verwenden. Die abkürzenden Schreibweisen F p1 und G p1 lassen sich aus obiger Definition ableiten und sind ebenfalls PSL-FL--Formeln. Die Übersetzung einer PSL-FL--Formel in einen Monitor erfolgt indem mittels der sog. Tableau-Technik zunachst ein nichtdeterministischer endlicher Automat konstruiert und dieser anschließend in einen deterministischen endlichen Automaten übersetzt wird. Mittels der Tableau-Technik wird die Erfüllbarkeit einer LTL-Formel in einen aussagenlogischen Teil und eine Verpflichtung engl. obligation für den nachsten Zustand des Modells zerlegt. Beide Teile werden anschließend disjunktiv verknüpft. . Gegeben ist die LTL-Formel p1 U p2. Um diese zu erfüllen muss entweder p2 im aktuellen Zustand gelten oder es gilt p1 und im nachsten Zustand gilt verpflichtend P1 U P2. Ersteres hebt die Verpflichtung auf da hierdurch bereits die LTL-Formel im momentanen Zustand erfüllt ist. Letzteres verlangt dass nachdem p1 im momentanen Zustand gilt die ursprüngliche LTL-Formel im nachsten Zustand erfüllt ist. Überdeckung von PSL-FL--Formeln Die disjunktive Verknüpfung beider Teile einer zerlegten LTL-Formel wird als Überdeckung der LTL-Formel .
