Die Suche ergab 681 Treffer

von yourmaninamsterdam
9. Dez 2012 20:35
Forum: Archiv
Thema: Lab 2 - Task 6
Antworten: 6
Zugriffe: 582

Re: Lab 2 - Task 6

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.
von yourmaninamsterdam
9. Dez 2012 18:50
Forum: Archiv
Thema: Lab2 Task 5
Antworten: 12
Zugriffe: 1039

Re: Lab2 Task 5

Es ist wichtig, dass ihr euch auf das Modellieren konzentriert. Den Angriff soll dann der Verifier finden.
von yourmaninamsterdam
9. Dez 2012 18:43
Forum: Archiv
Thema: Alice sendet nicht
Antworten: 2
Zugriffe: 331

Re: Alice sendet nicht

Habt ihr denn jemanden, der auf dem Channel empfängt?
von yourmaninamsterdam
8. Dez 2012 21:59
Forum: Archiv
Thema: Lab 2 - Task 6
Antworten: 6
Zugriffe: 582

Re: Lab 2 - Task 6

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 j...
von yourmaninamsterdam
8. Dez 2012 21:54
Forum: Archiv
Thema: Lab2 Task 5
Antworten: 12
Zugriffe: 1039

Re: Lab2 Task 5

Nein, er darf nicht vergleichen. Er sieht doch aber an der Nachricht, welchen Protokollschritt er gerade abgefangen hat. Daraus lässt sich (ganz ohne Vergleiche) schlussfolgern, was eine Nonce ist und welche.
von yourmaninamsterdam
8. Dez 2012 17:11
Forum: Archiv
Thema: Lab2 Task 5
Antworten: 12
Zugriffe: 1039

Re: Lab2 Task 5

Der Intruder kennt aber den Protokollablauf. Daraus geht hervor, welche Information er abgefangen hat (sollte er den Inhalt der Nachricht lesen können).
von yourmaninamsterdam
2. Dez 2012 12:40
Forum: Archiv
Thema: Lab 2 - Task 6
Antworten: 6
Zugriffe: 582

Re: Lab 2 - Task 6

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 aktuel...
von yourmaninamsterdam
1. Dez 2012 01:09
Forum: Archiv
Thema: hash conflicts
Antworten: 1
Zugriffe: 177

Re: hash conflicts

Meines Wissens kannst du diese Ausgabe einfach ignorieren, zumal dort "resolved" dahinter steht. Im Handbuch [1] gibt einen Hinweis darauf, was es damit auf sich hat: Es treten Hash-Konflikte auf, die dadurch aufgelöst werden, dass eine verlinkte Liste durchsucht wird. Für das Ergebnis macht das ans...
von yourmaninamsterdam
1. Dez 2012 01:05
Forum: Archiv
Thema: Bewertung Lab 1
Antworten: 1
Zugriffe: 212

Re: Bewertung Lab 1

Es dauert eine ziemlich lange Weile, die Programmierübungen zu korrigieren. Es ist bisher noch eine Reihe von Labs unbewertet. Euer Lab ist eins davon. Solltet ihr das Lab nicht bestehen, beginnt eure Nachfrist ab dem Moment, an dem ein Tutor euch ein Feedback gibt und in Moodle eine vorläufige Bewe...
von yourmaninamsterdam
22. Nov 2012 01:19
Forum: Archiv
Thema: Fragen zu Lab1
Antworten: 29
Zugriffe: 1442

Re: Fragen zu Lab1

Ich persönlich bin auch ein Fan von anderen Aufgaben, aber man muss es mit der Komplexität auch nicht gleich zu Beginn übertreiben, oder? Benutz doch einfach dein Wissen aus der Vorlesung und die Modellierungselemente aus der zweiten Übung, um ein kompaktes und übersichtliches Modell für den Sachver...
von yourmaninamsterdam
22. Nov 2012 00:36
Forum: Archiv
Thema: Fragen zu Lab1
Antworten: 29
Zugriffe: 1442

Re: Fragen zu Lab1

In meinem Fall ist es gewissermaßen auch so. Zwar kann es zwischen der Auswertung des Guards und des Asserts zu Interleaving kommen, die Variable x ist aber lokal, sodass es zu keiner Änderung kommen sollte. Aber das ist im Grunde auch egal, denn ich überprüfe da einfach keine sonderlich entscheiden...
von yourmaninamsterdam
21. Nov 2012 21:44
Forum: Archiv
Thema: Fragen zu Lab1
Antworten: 29
Zugriffe: 1442

Re: Fragen zu Lab1

Was ist eigentlich, wenn sich die Korrektheit schon aus den IF-Statements ergibt? Die Frage deutet darauf hin, dass du den Zweck der Übung nicht verstanden hast. Als Faustregel kann man sagen, dass sich nie Korrektheit aus if-Statements ergibt. Wenn in deinem Programm natürlich Dinge stehen wie byt...
von yourmaninamsterdam
21. Nov 2012 17:16
Forum: Archiv
Thema: Fragen zu Lab1
Antworten: 29
Zugriffe: 1442

Re: Fragen zu Lab1

Das heißt dann aber wieder, dass man den Philosophen vorschreiben muss wie sie handeln sollen, um den Deadlock von vornherein zu vermeiden. In den vorherigen Post wurde jedoch gesagt das wir den Philosophen nicht vorschreiben sollen wie sie zu handeln haben, oder seh ich das jetzt falsch? Wenn du d...
von yourmaninamsterdam
21. Nov 2012 12:11
Forum: Archiv
Thema: Verifikation Server-Drucker
Antworten: 8
Zugriffe: 489

Re: Verifikation Server-Drucker

null hat geschrieben:Er kommt nicht in den atomic-Block rein, weil das guad blockt und geht daher weiter.
Er geht nicht weiter, sondern blockiert, bis 'printerStatus == free' wahr wird.
von yourmaninamsterdam
20. Nov 2012 21:01
Forum: Archiv
Thema: Fragen zu Lab1
Antworten: 29
Zugriffe: 1442

Re: Fragen zu Lab1

Noch zu den Asserts: Lasst bitte auch nur die asserts drin, die ihr für die Verifikation braucht und nicht "alle, die euch so eingefallen sind". Ich nehme an, es reicht, wenn das Programm mit N = 5 funktioniert. Aber da kann euch Nathan eher was zu sagen.

Zur erweiterten Suche