tailieunhanh - Digitale Hardware/ Software-Systeme- P21

Digitale Hardware/ Software-Systeme- P21: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. | 394 7 Software-Verifikation Falls eine Ursache und eine Wirkung stets den selben Wert besitzen so besteht zwischen Ursache und Wirkung eine Identität siehe Abb. . Falls Ursache und Wirkung jedoch stets invertierte Werte zueinander besitzen so ist deren Relation eine Negation Abb. . Eine Disjunktion Konjunktion liegt vor wenn eine Wirkung eintritt sofern eine alle der verbundenen Ursachen eintreten Abb. und d . Eine exklusive Beziehung zwischen zwei Ursachen besteht wenn die Anwesenheit einer Ursache die Anwesenheit der anderen Ursache ausschließt Abb. . Die O-Abhangigkeit engl. one and only one ist gegeben wenn immer exakt eine Ursache erfüllt ist Abb. . Abbildung zeigt eine inklusive Beziehung zwischen Ursachen. Dies bedeutet dass mindestens immer eine Ursache erfüllt ist. Die R- und M-Abhangigkeit engl. requires und masks dargestellt in Abb. und i liegen vor falls die Anwesenheit einer Ursache die Anwesenheit der anderen Ursache voraussetzt bzw. die Anwesenheit der Ursache durch die Anwesenheit der anderen Ursache maskiert wird. Das folgende Beispiel stammt aus 305 . Beispiel . Betrachtet wird ein Programm das Zeichen von einer Tastatur solange einliest wie große Vokale und große Konsonanten eingegeben werden oder ein Zahler kleiner ist als der Maximalwert vom Typ int. Der Zahler wird beim Lesen eines großen Vokals oder Konsonanten inkrementiert. Er zahlt somit die gelesenen Zeichen. Im Falle dass das gelesene Zeichen ein großer Vokal ist wird ein zweiter Zahler für die Vokale ebenfalls inkrementiert. Ist das gelesene Zeichen weder ein großer Vokal noch ein großer Konsonant so wird das Programm beendet. Das Programm sieht wie folgt aus 1 Programm 2 char c 3 int count 0 4 int voc_count 0 5 std cin c 6 while c A c Z 7 count MAX_INT 8 count 9 if c A c E c I 10 c O c U 11 voc_count 12 std cin c 13 Die Ursachen in diesem Programm lauten u1 das gelesene Zeichen ist ein großer Konsonant u2 das gelesene Zeichen ist ein .