Qualitätssicherung von Software (SWQS)

Prof. Dr. Holger Schlingloff

Humboldt-Universität zu Berlinund

Fraunhofer FOKUS

4.6.2013: Software Model Checking

Folie 2H. Schlingloff, Software-Qualitätssicherung

Fragen zur Wiederholung

• Was versteht man unter temporaler Logik?

• Wozu wird sie verwendet?

• Was bedeutet (p U q)

• Wie formuliert man “Auf jeden Regen folgt einmal Sonnenschein”?

• Unterschied LTL-CTL?

• Wie funktioniert Modellprüfung für temporale Logik?

Folie 3H. Schlingloff, Software-Qualitätssicherung

Software Model Checking

• Modellprüfung verifiziert eine temporale Formel in einem Modell woher kommt die Formel? woher das Modell?

• Technologische Fortschritte direkte Verifikation von Source Code möglich? nur Standardeigenschaften?

• Viele (Forschungs-)Tools verfügbar BANDERA, BLAST, CBMC, dSPIN, JPF, MAGIC, SLAM, SPIN 4,

Verisoft XT, CMC, ZING, etc.

• Beispiel Java Path Finder (Nasa) analysiert direkt den Java Byte Code spezialisiert auf Parallelitätsfehler (“race conditions”)

Folie 4H. Schlingloff, Software-Qualitätssicherung

Beispiel JPF

public class MyRaceCondition {

private static class Target { int i = 0; public void incr() { i++; } } private static class RaceCar extends Thread { Target finish; public void run() { for (int k = 0; k<5; k++) finish.incr(); } }

public static void main(String[] args) throws InterruptedException { Target line = new Target(); RaceCar racer1 = new RaceCar(); racer1.finish = line; RaceCar racer2 = new RaceCar(); racer2.finish = line;

racer1.start(); racer2.start(); //racer1.join(); //racer2.join();

System.out.println("i: " + line.i + ", div: " + 20/(line.i - 2)); }}

Folie 5H. Schlingloff, Software-Qualitätssicherung

Ergebnis

====================================================== error #1gov.nasa.jpf.jvm.NoUncaughtExceptionsPropertyjava.lang.ArithmeticException: division by zeroat MyRaceCondition.main(MyRaceCondition.java:22)====================================================== snapshot #1thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0} call stack:at MyRaceCondition.main(MyRaceCondition.java:22)

thread MyRaceCondition$RaceCar:{id:1,name:Thread-1,status:RUNNING,priority:5,lockCount:0,suspendCount:0} call stack:at MyRaceCondition$Target.incr(MyRaceCondition.java:6)at MyRaceCondition$RaceCar.run(MyRaceCondition.java:13)

thread MyRaceCondition$RaceCar:{id:2,name:Thread-2,status:RUNNING,priority:5,lockCount:0,suspendCount:0} call stack:====================================================== resultserror #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: division by zero a...“====================================================== statisticselapsed time: 00:00:02states: new=2419, visited=2029, backtracked=4439, end=383search: maxDepth=37, constraints hit=0choice generators: thread=2418 (signal=0, lock=1, shared ref=2028), data=0heap: new=10554, released=13688, max live=380, gc-cycles=4446instructions: 146638max memory: 15MBloaded code: classes=87, methods=1318

Folie 6H. Schlingloff, Software-Qualitätssicherung

Wie funktioniert das?

•Anweisung i++ ist nicht elementar! d.h., i kann jeden Wert zwischen 2 und 10

haben

• JPF sucht alle Interleavings ab

•Explizite Repräsentation des Zustandsraumes

•Depth-first-search

•Eigenschaften: LTL, Assertions

•Auswertung der Formeln während des Aufbaus des Zustandsgraphen

Folie 7H. Schlingloff, Software-Qualitätssicherung

JPF Architektur

Aus: W. Visser, P. Mehlitz, Model Checking Programs with Java PathFinderhttps://wiki.engr.illinois.edu/download/attachments/.../jpf-tutorial.ppt

Folie 8H. Schlingloff, Software-Qualitätssicherung

Programmzustände

• Der Zustand des Programms besteht aus Information über jeden Thread im Java Programm

- für jede aufgerufene Methode ein Keller den statischen Variablen in allen Klassen

- Fields und Locks für jede Klasse den dynamischen Variablen aller Objekte

- Fields und Locks für jedes Objekt

• Gemeinsame Anteile des Zustandsraumes Aufteilen auf eine Menge separat gespeicherter Komponenten fields, locks, frames

• Statt einer Menge von Zustandskomponentenwerten wird nur der Index eines Eintrags gespeichert jeder Zustand ist ein Integer-Array

• effiziente Repräsentation von Mengen von Integer-Arrays

Folie 9H. Schlingloff, Software-Qualitätssicherung

Zustandsraumexplosion

•n boolesche Variablen 2n Zustände

•Maßnahmen: Symmetrie-Reduktionen

- Äquivalente Zustände werden nur einmal durchsucht

Partial-order-Reduktionen- verschiedene Interleavings, die zum selben

Ergebnis führen, werden nur einmal durchsucht

Abstraktion- gewisse Anteile des Zustands werden

weggelassen

Folie 10H. Schlingloff, Software-Qualitätssicherung

Symmetrie-Reduktionen

• Idee: Äquivalente Zustände nur einmal durchsuchen

• “Äquivalent”: Im Sinne des erwarteten Fehlverhaltens Speicherverwaltung, Reihenfolge der erzeugten

Objekte, usw.

• Die Reihenfolge, in der Klassen geladen werden, spielt für JPF keine Rolle “Kanonische Ordnung” der Klassen im Speicher

• Verwaltung dynamisch erzeugter Objekte? Speichern der Art und Anzahl von “new” Aufrufen

Folie 11H. Schlingloff, Software-Qualitätssicherung

Partial-Order Reduktion

• Parallele Ausführung von Threads führt zu vielen verschiedenen Interleavings oft beeinflusst die Reihenfolge das Gesamtergebnis nicht dann ist es ausreichend, nur eine statt aller Möglichkeiten zu

untersuchen Bsp.: {x=0, y=0} x++ || y++ {x=1, y=1}

x=0, y=0

x=1, y=0

x=0, y=1

x=1, y=1

x++

x++

y++

y++

Folie 12H. Schlingloff, Software-Qualitätssicherung

class S1 { int x;}class FirstTask extends Thread { public void run() { S1 s1; int x = 1; s1 = new S1(); x = 3;}}

class Main { public static void main(String[] args) { FirstTask task1 = new FirstTask(); SecondTask task2 = new SecondTask(); task1.start(); task2.start();}}

class S2 { int y;}class SecondTask extends Thread { public void run() { S2 s2; int x = 1; s2 = new S2(); x = 3;}}

state space search generates 258 stateswith symmetry reduction: 105 stateswith partial order reduction: 68 stateswith symmetry reduction + partial order reduction : 38 states

Bsp. aus:W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda. "Model Checking Programs." Automated Software Engineering Journal Volume 10, Number 2, April 2003 www.cs.ucsb.edu/~bultan/courses/267/.../l12.ppt

Folie 13H. Schlingloff, Software-Qualitätssicherung

Abstraktion

• Techniken aus der abstrakten Interpretation von Programmen (nächstes Kapitel): Slicing Partielle Evaluation

• Slicing versucht, “irrelevante” Programmteile wegzulassen “irrelevant” in Bezug auf ein bestimmtes Kriterium Z.B. Erreichbarkeit einer bestimmten Anweisung bestimmte Variablen könnten dazu nicht beitragen Abhängigkeitsanalyse

Folie 14H. Schlingloff, Software-Qualitätssicherung

Weitere Abstraktionstechniken

• manuelle Einschränkungen des Zustandsraumes 32-Bit-Integer zu 8-Bit Größe von Arrays einschränken dynamische Objekterzeugung vermeiden

• Zusätzliche Annahmen im Programmtext Verify.beginAtomic()... Verify.endAtomic() Verify.assertTrue(... );

• Ersetzung durch “abstrakte Bereiche” z.B. Int durch {<0, =0, >0}