Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

18
Fachbereich Informatik/Mathematik 100. Fachbereichsseminar Fehlersuche und Test von Fehlersuche und Test von Software Software 1. Fehler und Fehlersuche in Programmen … 2. „Klassisches“ Testen (Jamus, JUnit) 3. Testen reaktiver und verteilter Systeme (EPKfix, SaxTeste 7. Februar 2005 Hartmut Fritzsche

description

Fachbereich Informatik/Mathematik 100. Fachbereichsseminar. Fehler und Fehlersuche in Programmen … „Klassisches“ Testen(Jamus, JUnit) Testen reaktiver und verteilter Systeme (EPKfix, SaxTester). Fehlersuche und Test von Software. 7. Februar 2005 Hartmut Fritzsche. - PowerPoint PPT Presentation

Transcript of Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

Page 1: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

Fachbereich Informatik/Mathematik100. Fachbereichsseminar

Fehlersuche und Test von SoftwareFehlersuche und Test von Software

1. Fehler und Fehlersuche in Programmen …

2. „Klassisches“ Testen (Jamus, JUnit)

3. Testen reaktiver und verteilter Systeme (EPKfix, SaxTester)

7. Februar 2005Hartmut Fritzsche

Page 2: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

2

1. Fehler und Fehlersuche in Programmen …

„Fehler“ - Abstraktionen:

Globale Sicht: Ein Fehler ist jede Abweichung der tatsächlichen Ausprägung einer Qualitätseigenschaft von der vorgesehenen Sollausprägung.

Korrektheit eines Programms:

Ein Fehler ist jede Abweichung der Implikation von der Spezifikation (IEEE/ANSI-Standard).

Strukturelle Softwaretests:

Ein Fehler ist ein strukturelles Merkmal des Programmtextes, das

ein fehlerhaftes Verhalten des Programms verursacht.

Sprich: „Ein Programmfehler kann eine Programmausnahme (Exception) verursachen“.

„Durch Testen kann man die Anwesenheit von Fehlern zeigen, nicht aber deren Abwesenheit“ E.W. Dijkstra

Page 3: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

3

Fehler aus der „Praxis“:

der Fehler, den ich zuletzt gesucht habe …

(Shell-Interpreter, LV BS, 3. Februar 2005)

der Fehler, an dem ich am längsten gesucht habe …

(im Garbage Collection, System TULISP, 1985)

ein wirklich komplizierter Fall …

(D. Knuth, „Man or Boy“, 1964)

Page 4: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

4

#include <sys/types.h>#include <sys/wait.h>#include <stdio.h>

int main(void) {

char buf[80]; pid_t pid; int status;

printf("%% "); while(fgets(buf,80, stdin) != NULL) {

buf[strlen(buf) - 1] = 0;if ( (pid = fork()) < 0) printf("fork error");else if (pid == 0) { execlp(buf, buf, (char *) 0); printf("command not executable: %s\n ",buf); exit(127);}if ((pid = waitpid(pid, &status, 0)) < 0) printf("waitpid error");printf("%% ");

} exit(0); /* exit(4) */}

ein simpler Shell-Interpreter:das Klammerpaar ( ) wurde vergessen

• fork() erzeugt Sohnprozess, in dem wird eingegebenes Kommando ausgeführt.

• im Vaterprozess ist (fälschlicherweise) der Wert pid = 0 , da der Vergleichswert zugewiesen wird. Auch hier wird das eingelesene Kommando ausgeführt, waitpid wird nie erreicht.

Page 5: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

5

hartmut@linux:~/BSII> ./a.out% dateSam Feb 5 18:11:01 CET 2005Sam Feb 5 18:11:01 CET 2005hartmut@linux:~/BSII> echo $?0hartmut@linux:~/BSII>

hartmut@linux:~/BSII> ./a.out% dateSam Feb 5 18:11:57 CET 2005% ps PID TTY TIME CMD 2372 pts/1 00:00:00 bash 2665 pts/1 00:00:00 a.out 2667 pts/1 00:00:00 ps% hartmut@linux:~/BSII>

Analyse: • Fehler ohne Testwerkzeug ermittelt

• keine Spezifikation vorhanden

• manuelle Pfadanalyse (Parallelität)

Page 6: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

6

TULISPGarbage Collection:

mark + sweep• typenreine Seiten – hier: pair • automatisch ausgelöstes GC

Wirkung des Fehlers:

In Listen tauchen falsche Elemente auf:

1 falsch verkettetes Element auf ca. 15000 richtig verkettete(keine Exception !)

Analyse:

• Es kann kein Testfall konstruiert werden, um den Fehler zu reproduzieren!• keine Spezifikation vorhanden• kein Testwerkzeug verfügbar• Fehlersuche mit Debugger

Page 7: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

7

1 Zelle „pair“ → 1 Halbwort (4 Hex)1 Page → 1020 Halbworte≈ 15 Seiten → 15300 Zellen

81E 1

Page 8: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

8

begin real procedure A(k,x1,x2,x3,x4,x5); value k; integer k; begin real procedure B;

begin k := k - 1; B := A := A(k,B,x1,x2,x3,x4) end; if k <= 0 then A := x4 + x5 else B

end; outreal(A(10,1,-1,-1,1,0))end;

„Man or Boy“ ?oder: Wen interessiert noch die Parametervermittlung „call-by-name“?

(Testprogramm für Algol-60-Compiler von D. Knuth, 1964)

Prozedur B ist lokal zu A

B wird an A übergebenk via call-by-value

Prozeduraufrufe

Page 9: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

9

Ergebnisse bis k=23: >> ManOrBoyEnv 1 0 -2 0 1 0 1 -1-10-30-67-138-291-642-1446-3250-7244-16065-35601-78985-175416-389695-865609-1922362

Scheme (Ein LISP-Dialekt mit lexikaler Bindung):

(define A (lambda(k x1 x2 x3 x4 x5)(letrec ((B (lambda()

(set! K (- k 1))(A k B x1 x2 x3 x4))))

(if (<= k 0)(+ (x4)(x5))(B)))))

Aufruf:

(A 10 (lambda() 1)(lambda() -1)(lambda() -1) (lambda() 1)(lambda() 0))

Referenz: H. Fritzsche, I.O. Kerner / Informatik-Spektrum 20/3 1997

Page 10: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

10

2. „Klassisches“ Testen (Jamus, JUnit)

SyntaxbaumQuellprogramm

(verschiedeneQuellsprachen)

Zielprogramm

(verschiedeneObjektsprachen)

Der Syntaxbaum ist die Referenz-Struktur eines Programms (nicht das Quellprogramm!)

Page 11: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

11

2. „Klassisches“ Testen (Jamus, JUnit)

SyntaxbaumQuellprogramm

(verschiedeneQuellsprachen)

Zielprogramm

(verschiedeneObjektsprachen)

Testrahmen(Testcases)

Test-Runner

SteuerflussgraphVisualisierung

Page 12: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

12

SystemeSysteme

Reaktive SystemeReaktive Systeme

„offen“, reagieren auf ständig eintreffende Eingangsdaten,

das Bewegen durch einenZustandsraum erfolgtereignisgetrieben

( Hardware oder Software, Klimaanlage, BS, EPK, … )

Transformative SystemeTransformative Systeme

„prozedural“, berechnen Ausgangsdaten, Eingangsdaten stehen zum Zeitpunkt der Aktivierung des Systems bereit

3. Testen reaktiver und verteilter Systeme …

Page 13: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

13

BMBF Verbundprojekt EPK-fix,1995 -98„Testassistenzsystem“ TASSI

FormaleSpezifikation

Anforderungs-analyse

Generierung

Page 14: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

14

TASSI• automatische und interaktive Testung • Testmonitor mit GUI

• parametrisierte Teststrategien

• Capture – Replay – Funktion

• Browswn in Fehlerklassifikationen

• Automatisches Prüfen Formalisierter Design-Richtlinien

Testen ist ein Verfahren mit Stichprobencharakter!

→ Testendekriterium

Page 15: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

15

Nutzung von Beweistechniken (z.B. SLD-/FWD-Resolution)

Verifikation:

Ziel eines Beweisvorganges ist es, nachzuweisen, dass die Softwareeine gegebene formale Spezifikation erfüllt (partielle bzw. totale Korrektheit).

A if B and C and …A :- B, C, … .

Wir drehen die Zielfunktion um:

Beim Testen reaktiver Systeme ist es das Ziel, in erreichten Systemzuständen durch Beweise Fehler gegenüber formal spezifizierten Sachverhalten aufzudecken.

„Es ist ein Fehler“ if B and C and … .

Beispiel: Formale Überprüfung von Design-Richtlinien

Es ist ein Fehler, wenn ein Objekt mit einer Hintergrundfarbetransitiv ein Element mit einer identischen Fontfarbe enthält

Page 16: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

16

Beispiel: SaxTester (2003)

Testen verteilter (Web-) Anwendungen mit GUIsKommunikation mittels XML-RPC

Capure – Replay – Funktionalität

Automatisches/manuelles Erstellen und Abspielen von Python-Skripts

Testung von Browser-Inhalten (MS IE) über das Component Object Model (COM-Schnittstelle)

(Diplomarbeit D. Linke, HTWD 2004, Medieninformatik)

Technologies & Application Development

Page 17: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

17

Symbolic Model Checking

Aussagen über erreichte oder zu erwartende Zustände eines Systems werden mit (temporal-) logischen Formeln beschrieben (z.B. Computational Tree Logic).

Ein Model-Checker prüft Formeln gegenüber dem Modell.

AX f : In jedem unmittelbaren Nachfolgezustand des aktuellenZustands ist f erfüllt.

AG f : Entlang jedes Pfades wird f in jedem Zustand erfüllt.

Beispiel: Klimaanlage

AG((Running & AboveDesiredTemp) → (AC | AX(AC)))AG((Running & BelowDesiredTemp) → (HEAT | AX(HEAT)))

Page 18: Fachbereich Informatik/Mathematik 100. Fachbereichsseminar

18

Resümee

• Praktisch werden kaum formale Spezifikationen (z.B. Klassen-Invarianten) unabhängig vom Programmtext verwendet.

• Entwicklungswerkzeuge (z.B. Together ControlCenter) verbinden Spezifikationen mit Generierung (Syntaxbaum!) und Reverse Engineering.

• Testwerkzeuge entlasten bisher den Programmierer nicht davon, Testfälle zu beschreiben, und werden es auch künftig nur begrenzt tun. Testfallbeschreibungen sind Spezifikationen!

• Testen reaktiver, verteilter Systeme wird praktisch noch zu wenig unterstützt. Ansätze existieren für einzelne Programmiermodelle (z.B. COM)