Verifizieren mit (X)Spin

Benutzeravatar
SM
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 10. Okt 2005 18:11
Wohnort: Darmstadt
Kontaktdaten:

Verifizieren mit (X)Spin

Beitrag von SM »

Hallo zusammen!

Also entweder hab ich was verpasst oder mein Gedächtnis ist ein Sieb, aber kann mir bitte irgendjemand genau erklären, wie ich mit xspin oder spin die Korrektheit eines Programmes beweise?

Versteht mich nicht falsch... ich war bei der "Einführung in Spin" (den Aufwand in Ehren, aber die dazugehörigen Folien sind im Nachhinein alles andere als eine Hilfe), in jeder Vorlesung und in jeder Übung und meine Gruppe hat sich bisher schon ausgiebig mit xspin beschäftigt - aber irgendwo will mir nicht 100%ig klar werden, wie ich vorzugehen habe.

Ok, den wechselseitigen Ausschluss zu zeigen, ist nicht weiter das Problem... aber bei der Verklemmungsfreiheit fängt es an... Reicht es, in jeden Prozess ein progress-Label zu packen und dann auf non-progress-cycles zu testen? Das dürfte doch eigentlich genügen, da das System ja nie zum Halt kommt, seh ich das richtig?

Und wie sieht es mit dem Verhungern aus? Bisher haben wir einen never-claim mit

Code: Alles auswählen

!((G F p1_in_critical_section) && (G F p2_in_critical_section))
verwendet. Dieser hält aber nur stand, wenn man Fairness vorraussetzt. Als Beispiel seien hier die Prozesse von Folie 22 genannt... setzt man nicht vorraus, dass irgendwann der zweite Prozess wirklich wieder mal zum Zug kommt, so kann sich theoretisch der erste Prozess beliebig oft wiederholen. (Eben dieser Cycle wird dann auch von xspin als entscheidender trace geliefert, der den never-claim erfüllt.) Es ist also nicht wirklich garantiert, dass der zweite Prozess jemals wieder zur Ausführung kommt.

Also gilt Fairness als vorrausgesetzt?

Ich kann mir nicht vorstellen, dass meine Gruppe die einzige ist, die sich solche Fragen stellt... also wäre ich über eine detaillierte Antwort bezüglich des Verifikationsablaufs dankbar.

MfG

SM
~ Per aspera ad astra. ~

j_roemer
Erstie
Erstie
Beiträge: 18
Registriert: 16. Nov 2005 16:31

Beitrag von j_roemer »

du bist nicht der einzige.
ich schliesse mich dem voll und ganz an!
Bitte um eine Antwort

MuldeR
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 131
Registriert: 18. Okt 2005 16:14
Wohnort: (d)armstadt
Kontaktdaten:

Re: Verifizieren mit (X)Spin

Beitrag von MuldeR »

SM hat geschrieben:Ich kann mir nicht vorstellen, dass meine Gruppe die einzige ist, die sich solche Fragen stellt... also wäre ich über eine detaillierte Antwort bezüglich des Verifikationsablaufs dankbar.

Mit freundlichen Grüßen

SM
Nein, deine Gruppe ist nicht die einzige! :?

Also, könnte es bitte jemand mal erklären, damit man auch die Aufgaben bearbeiten kann? Das "Tutorial" is ja wohl etwas sehr dürftig...


// EDIT

Vllt kommt man damit weiter:
http://www.spinroot.com/spin/Doc/SpinTutorial.pdf

snugans
Erstie
Erstie
Beiträge: 17
Registriert: 7. Nov 2004 15:58

Beitrag von snugans »

Wie teste ich denn genau mein never-claim?

Ich habe mit LTL den never claim erstellt, und dann die verification ausgeführt, im report steht jetzt 0 Errors etc, aber woran erkenn ich ob mein never stimmt oder nicht etc !?

bagotios
Mausschubser
Mausschubser
Beiträge: 72
Registriert: 1. Dez 2004 15:54

Beitrag von bagotios »

snugans hat geschrieben:Wie teste ich denn genau mein never-claim?

Ich habe mit LTL den never claim erstellt, und dann die verification ausgeführt, im report steht jetzt 0 Errors etc, aber woran erkenn ich ob mein never stimmt oder nicht etc !?
Du musst mit den flags -a -f testen ansonsten kann es sein das du nicht alle Fehler im Programm findest. Und ob dein never-claim stimmt, nunja bau einfach einen Fehler ein den du mit deinem claim finden willst. Findest du einen Fehler stimmt dein never-claim, findest du ihn nicht mußt du wohl einen neuen claim die ausdenken.

Andreas Schlosser
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 21. Okt 2005 10:35

Re: Verifizieren mit (X)Spin

Beitrag von Andreas Schlosser »

SM hat geschrieben: Ok, den wechselseitigen Ausschluss zu zeigen, ist nicht weiter das Problem... aber bei der Verklemmungsfreiheit fängt es an... Reicht es, in jeden Prozess ein progress-Label zu packen und dann auf non-progress-cycles zu testen? Das dürfte doch eigentlich genügen, da das System ja nie zum Halt kommt, seh ich das richtig?
Siehe hierzu meine Antwort im Thread "Spin und Wächterfunktion".
SM hat geschrieben: Und wie sieht es mit dem Verhungern aus? Bisher haben wir einen never-claim mit

Code: Alles auswählen

!((G F p1_in_critical_section) && (G F p2_in_critical_section))
verwendet. Dieser hält aber nur stand, wenn man Fairness vorraussetzt. Es ist also nicht wirklich garantiert, dass der zweite Prozess jemals wieder zur Ausführung kommt. Also gilt Fairness als vorrausgesetzt?
Offenbar hast Du durch Deine Verifikationsversuche rausgefunden, dass das Verfahren nur bei fairer Ausführung wirklich funktioniert. Dann muss Fairness eben vorausgesetzt werden um die Korrektheit zu zeigen. Jetzt kannst Du Dir noch überlegen, ob das sinnvoll/realistisch ist, oder ob das Verfahren evtl. doch nicht so toll ist.

Andreas Schlosser
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 21. Okt 2005 10:35

Re: Verifizieren mit (X)Spin

Beitrag von Andreas Schlosser »

MuldeR hat geschrieben: Also, könnte es bitte jemand mal erklären, damit man auch die Aufgaben bearbeiten kann? Das "Tutorial" is ja wohl etwas sehr dürftig...
Vllt kommt man damit weiter:
http://www.spinroot.com/spin/Doc/SpinTutorial.pdf
Worauf im "Tutorial" ja auf der letzten Folie hingewiesen wurde...

Andreas Schlosser
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 21. Okt 2005 10:35

Beitrag von Andreas Schlosser »

bagotios hat geschrieben:
snugans hat geschrieben:Wie teste ich denn genau mein never-claim?

Ich habe mit LTL den never claim erstellt, und dann die verification ausgeführt, im report steht jetzt 0 Errors etc, aber woran erkenn ich ob mein never stimmt oder nicht etc !?
Du musst mit den flags -a -f testen ansonsten kann es sein das du nicht alle Fehler im Programm findest. Und ob dein never-claim stimmt, nunja bau einfach einen Fehler ein den du mit deinem claim finden willst. Findest du einen Fehler stimmt dein never-claim, findest du ihn nicht mußt du wohl einen neuen claim die ausdenken.
Was getestet wurde sieht man ja in der Auflistung nach der Ausführung von ./pan - da steht in den einzelnen Zeilen ein '+' oder ein '-'.

Wenn ein Fehler gefunden wird, ist die eine Möglichkeit sicherlich ein anderes claim zu nehmen. Eine andere (durchaus nicht seltene) Lösung besteht aber auch darin, sich sein Modell nochmal genau anzuschauen. Evtl. ist ja auch in der Modellierung noch ein kleiner Fehler drin.

Antworten

Zurück zu „Archiv“