Seite 1 von 1

Nop-Shadows Analysis

Verfasst: 28. Feb 2012 17:38
von Fl4sh
Hallo!

Leider sitzen wir jetzt schon fast eine Stunde an der "Nop-Shadows Analysis" und haben keine Ahnung was da nun genau gemacht wird.
Leider fehlen in der Folie auch erläuternde Sätze. Stattdessen blinken farbige Punkte auf und jeder Erklärungsversuch den wir entwickeln läuft irgendwann ins Leere.
Wäre jemand so nett uns das Verfahren "Schritt für Schritt" zu erklären. Wir wissen, dass nun, in diesem 3. Schritt, die Reihenfolge der Aufrufe eine Rolle spielt und wohl eine Backward-Analysis durchgeführt wird. Aber wie wird genau vorgegangen? Wie ist die genaue definition von Hot und Cold?

Vielen, vielen Dank! Ich hoffe jemand erbarmt sich! :)

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 19:07
von tgp
Ok, ich versuchs mal - ist aber schon relativ spät für so grundsätzliche Fragen, gell? :wink:

NSA besteht aus drei Teilen:
  1. eine Vorwärtsanalyse
  2. eine Rückwärtsanalyse
  3. Kombination beider Analyse-Ergebnisse
In den Folien ist 1. und 2. vertauscht erklärt, ist aber egal, da die unabhängig voneinander sind. 1. ist halt einfacher, diese Reihenfolge erhöht eure Chancen, zumindest das bis zur Klausur zu verstehen :). Der 3. Teil ist nicht so explizit in den Folien getrennt, aber das seht ihr dann hoffentlich. Ich erstelle mal für jeden Schritt nacheinander einen eigenen Beitrag in diesem Thread.

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 19:14
von tgp
1. Die Vorwärtsanalyse (animierter Foliensatz, Folie 99)

Ausgangspunkt ist der endliche Automat und das zu untersuchende Programm, welches aus einer Liste von Events besteht (Methodenaufrufen).

Ihr startet vor dem ersten Event und schreibt dort den Startzustand des Automaten hin (grün, "connected"). Dann schaut ihr, in welchen Zustand der Automat wechselt, wenn ihr das Event "ausführt", also die Transition entlanggeht. In der Folie ist das "c.close()", was im Automaten von "connected"/grün zu "disconnected"/gelb führt. Diesen neuen Zustand schreibt ihr hinter das gerade abgearbeitete Event. Nun wieder schauen, wohin ihr von gelb mit reconnect kommt und das dahinter schreiben (grün) usw.

Die Vorwärtsanalyse ist abgeschlossen, wenn ihr das letzte Event (write) abgearbeitet habt und also den Zustand hingeschrieben habt.

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 19:27
von tgp
2. Die Rückwärtsanalyse (animierter Foliensatz, Folien 94-98)

Ausgangspunkt ist wieder der Automat + das Programm, das ihr aer diesmal eben rückwärts durchgeht. Ziel ist es bei diesem Teil, herauszufinden, ob das Programm in einen Fehlerzustand laufen kann (siehe animierter Foliensatz zur statischen Analyse, Folie 47: Rückwärtsanalysen ergeben Infos über die Zukunft).

Ihr startet hinter dem letzten Event und sortiert die Zustände des Automaten nach "Fehlerzustand" (=hot-Spalte) und "nicht Fehlerzustand" (=cold-Spalte). Interessanter ist natürlich ersteres, aber zum Verständnis ist es auch gut, die cold-Spalte zu führen. Im Beispielautomaten ist nur "error"/rot ein Fehlerzustand, alle anderen sind cold.

Nun schaut ihr, wie ihr in diesen Zustand gekommen sein könntet. Dazu arbeitet ihr das letzte Event "rückwärts" ab, d.h. ihr schaut nach Transitionen, die per "write" in den roten Zustand führen. Da gibts zwei, Eine von "disconnected"/gelb und eine von "error"/rot selbst. Somit ändert ihr in der Zeile direkt über "write" die hot-Zustände auf rot und gelb", der Rest (grün) ist kalt. Denn das heißt: Wenn der Automat an der Stelle im gelben oder roten Zustand ist, und das "c.write()" ausgeführt wird, landet ihr am Ende im Fehlerzustand.

So geht das bis zur Abarbeitung des ersten Events weiter: Bei gelb und rot gibt es keine Transitionen, die dorthin mit "reconnect" führen. Also ist davor alles kalt^^. Noch eins davor würdet ihr nach "close"-Transitionen suchen, die ins Nichts führen (hot ist ja leer), also gibt es davor auch keine hot-Zustände.

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 19:55
von Mr.B
Sehr nice, danke für diese ausführliche Beschreibung!

Kannst du nochmal was zum dritten Schritt(Kombination beider Analyse-Ergebnisse) sagen?

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 20:06
von tgp
3. Kombination beider Analyse-Ergebnisse (animierter Foliensatz, Folien 99-100)

Im letzen Teil benutzt ihr den Automatenablauf aus 1. und die Unterscheidung "könnte zum Fehlerzustand führen" / "kann nicht", um zu erkennen, an welchem Punkt im Ablauf eine Überwachung nicht nötig ist. Nicht nötig, weil "nix passieren kann", also ein Event nichts an der Wahrscheinlichkeit ändert, dass der Automat in den Fehlerzustand kommt. Das geht so:

Ihr startet beim ersten Event und betrachtet den Zustand des Automaten vor und nach der Ausführung, in den Folien ist das grün und gelb, wie bei 1. festgestellt. Nun schaut ihr beim Analyseergebnis aus 2., in die Zeile direkt nach der Ausführung des Events. In den Folien ist das die zweite Zeile mit rot, gelb und grün als cold-Zustände (die erste Zeile wird nicht gebraucht).

Ihr seht, dass beide Zustände (grün und gelb) cold sind, also in derselben Äquivalenzklasse. Das bedeutet, dass es egal ist, ob "c.close()" ausgeführt wird oder nicht, in jedem Fall seit ihr auf der cold-Seite. Also ist die Überwachung der Zeile unnötig und kann gestrichen werden.

Anders beim nächsten Event: Da gehts laut 1. von gelb nach grün, nach 2. ist aber gelb dann hot-Zustand und grün cold-Zustand. Also sind die Zustände nicht äquivalent, und die Überwachung muss bleiben. Beim dritten Event ist es dann einfach, weil der Automat an sich schon im gleichen Zustand (grün) bleibt, und grün=cold ist nunmal äquivalent zu grün=cold :D.


Sonstiges:

In dem Foliensatz steht noch was von erster und zweiter Iteration. Das und noch ein anderes Detail hat Eric leider erst bei der Übungsbesprechung ordentlich erklärt: Sobald man einen shadow entfernt hat (=die Überwachung gestrichen), muss man 1. und 2. wiederholen, da sich da der Ausgangspunkt, genauer das Programm / die Liste der Events verändert hat. Im Clara-Foliensatz sieht das so aus, als ob man die zweite Iteration erst startet, wenn man alles gestrichen hat, was nicht von hot nach cold oder umgekehrt führt.


Die zweite Sache war im Clara-Foliensatz gar nicht erwähnt, braucht man aber bei der Übung: Die Rückwärtsanalyse muss man in einer Iteration ggf. mehrmals durchführen. Das ist im animierten RefaFlex-Foliensatz auf der Folie 96 gezeigt: Auf der rechten Seite gibt es zwei Backwards-Spalten (und es werden nur die interessanten Zustände, also die von "hot" gezeigt).

Das liegt daran, dass im Programm zweimal das Event "write" auftaucht. Es kann ja sein, dass man schon mit dem ersten in den Fehlerzustand kommt. "Zum Glück" gibt es aber nur write-Transitionen, die in den Fehlerzustand führen, weshalb man das Programm nur auf dieses Event abgrasen muss, das aber eben zweimal auftaucht.

Das zu 2. gesagte muss also nicht nur hinter dem letzten Event losgehen (Stelle "//(6)"), sondern auch hinter dem "c.write("all fine")" / "//(4)". Dort gehts wieder mit dem Fehlerzustand los, der hot ist (Ich empfehle übrigens, eine Rückwärtsanalyse nach der anderen zu machen, sonst kommt man durcheinander). Wieder müsst ihr schauen, welche Transitionen in "error" münden, die mit "write" beschriftet sind (welche von rot und gelb). Dann schaut ihr, welche reconnect-Transitionen in rot oder gelb enden - gibt keine, also gibt es bei "//(2)" auch keine hot-Zustände.

Jetzt muss noch geklärt werden, wie ihr die Infos aus den zwei (oder ggf. mehr...) Rückwärtsanalysen bei 3. verwenden könnt. Hier gilt einfach, dass die Zustände bei beiden Analysen jeweils im gleichen Zustand sein müssen. Also am Beispiel des ersten "close"-Events: Aus 1. wisst ihr, dass der Automat von grün nach gelb geht. In der linken ("längeren") Rückwärtsanalyse sind bei "//(2)" beide hot, also äquivalent. Bei der rechten Analyse sind sie cold (Erinnerung: die sind eigentlich uninteressant, also ausgeblendet), also auch äquivalent. Deshalb kann die Überwachung des close entfernt werden.

Jetzt müsste eigentlich, wie oben geschrieben, 1. und 2. neu berechnet werden, aber fürs Verständnis noch der andere Fall, der auf der Folie 97 gezeigt ist: Beim reconnect gehts von gelb nach grün, die längere Analyse sieht beide danach als hot an, bei der kürzeren ist gelb=hot und grün=cold. Also kann beim reconnect die Überwachung nicht entfernt werden.


Jetzt alles klar?

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 20:06
von tgp
Mr.B hat geschrieben:Sehr nice, danke für diese ausführliche Beschreibung!

Kannst du nochmal was zum dritten Schritt(Kombination beider Analyse-Ergebnisse) sagen?
Ja, der hat zusammen mit "Sonstiges" etwas zum Tippen gebraucht ;).

Re: Nop-Shadows Analysis

Verfasst: 28. Feb 2012 20:14
von Fl4sh
Vielen, vielen Dank! :)

Du hast uns sehr geholfen! :) Wir hätten echt nicht gedacht, dass sich jemand so viel Mühe gibt! :) Danke! :)