Lab 2 - Task 6

hstr
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Lab 2 - Task 6

Beitrag von hstr »

Hallo,
wir haben ein Problem beim Überprüfen der Bedingungen.
Beim Ausführen der pan.exe erhalten wir jedes mal (egal bei welcher Bedingung) "unreached in proctype ...".
Selbst durch umformulieren der Bedingungen haben wir noch das gleiche Problem.
In der Vorlesung gab es auch kein Beispiel für den Umgang mit Implikationen bei temporaler Logik.

VG

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Lab 2 - Task 6

Beitrag von yourmaninamsterdam »

Implikationen in temporaler Logik funktionieren im Grunde genauso wie in Aussagenlogik. Du forderst die Konklusion, aber nur wenn die Prämisse wahr ist. Ist die Prämisse jedoch falsch, dann ist es egal, ob die Konklusion erfüllt ist oder nicht. Eine LTL-Formel fordert das zunächst mal für den aktuellen Zeitpunkt, es sei denn, du verpasst ihr ein '[]'. Beispiele dafür gab es übrigens in der 3. Übung.

"Unreached in proctype ..." spricht vermutlich von unerreichten Zuständen? Das passiert, wenn du Code hast, der unerreichbar ist, etwa wenn vorher eine Endlosschleife steht oder ein Prozess immer blockiert. Das kann, muss aber nicht zwingend ein Problem sein.

Melkman
Neuling
Neuling
Beiträge: 2
Registriert: 13. Okt 2010 22:43

Re: Lab 2 - Task 6

Beitrag von Melkman »

Darf Bob auch mit dem Intruder eine Kommunikation anfangen, weil sonst ist ja die Abfrage auf knows_nonceB eig sinnlos. Er kann ja nicht die nonce von Bob wissen, wenn Bob an Alice schreibt, da der Intruder ja den data teil nicht lesen kann, da es nicht mit seinen Schlüssel verschlüsselt wurde.

Zudem hab ich noch eine Frage zu dem Counterexample, was ist das?? War in dieser Vorlesung nicht da, kann mir jemand dies vielleicht erklären? Wäre sehr nett, danke :)

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Lab 2 - Task 6

Beitrag von yourmaninamsterdam »

Modellier doch bitte einfach das, was in der Aufgabenstellung gefragt ist. Im Übrigen sollte man hier nicht zu viel "Vorwissen" mitmodellieren, denn es geht ja gerade darum, Angriffe aufzudecken, die man sonst eventuell nicht bemerkt hätte. Wenn du jetzt Dinge sagst wie "das ist sinnlos", "er kann ja nicht" und so weiter, dann ist ja alles super und wird auch dann nicht eintreten, wenn dein Modell es erlaubt. Aber das sehen wir dann, denn nur weil du das jetzt grad sagst, glaube ich dir das zumindest nicht.

Counterexample ist einfach Englisch für Gegenbeispiel. In dem Fall also ein Trail (bzw. die Beschreibung des Programmablaufs), bei dem das Protokoll nicht wie gewünscht terminiert.

T.R.
Erstie
Erstie
Beiträge: 11
Registriert: 2. Mai 2011 08:09

Re: Lab 2 - Task 6

Beitrag von T.R. »

Ich verstehe bei den Hinweisen nicht, wann wir für die ltl Formeln Abkürzungen einführen sollen. Sind Ausdrücke der Art !a || b && c bereits komplex? Wo schreibe ich die Abkürzungen auf - vielleicht mittels Makro #define?

Edit: Ich schätze, das mit den Einschränkungen beim Formulieren von Formeln, bezieht sich auf die verschieden Arten ltl Formeln einzubetten. :idea:
Zuletzt geändert von T.R. am 9. Dez 2012 19:29, insgesamt 2-mal geändert.

T.R.
Erstie
Erstie
Beiträge: 11
Registriert: 2. Mai 2011 08:09

Re: Lab 2 - Task 6

Beitrag von T.R. »

*doppelpost*

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Lab 2 - Task 6

Beitrag von yourmaninamsterdam »

Das, was du schätzt, ist völlig korrekt. Verwendet bitte nur Möglichkeit (3). Abkürzungen für Teilformeln mit #define können trotzdem sinnvoll sein, weil man dann Teilformeln sprechende Namen geben kann.

Antworten

Zurück zu „Archiv“