Programmierung und Softwaretechnik (PST) — PST - Veri zieren, … · 2016. 1. 27. ·...

Softwaretechnik

Verifizieren, Validieren, Testen

Prof. Dr. Matthias Holzl

Joschka Rinke

27. Januar 2016

Uberblick

Wie kann man hohe Software-Qualitat erreichen?

I Inspektionen

I Formale Verifikation

I Testen

Einfuhrung in Verifikation, Validierung und Testen

Software-Qualitat

I Hohe Qualitat von Software sicherzustellen ist eines dergrundlegenden Probleme der Softwaretechnik

I Welche Techniken helfen ein zuverlassiges, effektives undeffizientes Produkt herzustellen?

I Gutes PersonalI Gute Management-Praktiken und EntwicklungsprozesseI Gute Architektur und gutes DesignI Verifikation, Validierung und Testen

(Testen ist Teil von Verifikation und Validierung)

Verifikation und Validierung (V&V)

I Verifikation:”Are we developing the product right?“

I Entspricht die Software ihrer Spezifikation(ihren funktionalen und nichtfunktionalen Requirements)?

I Validierung:”Are we developing the right product?“

I Entspricht die Software den Kundenanforderungen?I Allgemeiner als Verifikation

Verifikation und Validierung (V&V)

Verifikations und Validierungstechniken

I Statisch: Das Programm wird nicht ausgefuhrtI Code-Inspektionen und -ReviewsI Formale Methoden

I Dynamisch: Das Programm wird ausgefuhrt undTerminierungszustand oder Ergebnisse werden uberpruft

I TestsI Fuzzing (automatisches Testen)

Statische Verifikation und Validierung I

Code-Inspektionen und Reviews

Code-Inspektionen und Reviews

I Der Programmcode wird von einem oder mehrerenProgrammierern, die nicht der ursprungliche Autor sind,manuell uberpruft

I Konnen mehr oder weniger formal durchgefuhrt werdenI Toolunterstutzung

I ChecklistenI Code-NavigationI Versionskontrolle

I Moderne Code-Hosting-Plattformen bietenProjektmanagement Tools, die Unterstutzung furCode-Inspektionen und Reviews integrieren(z.B. Issues, Pull-Requests)

Beispiel: Projektmanagement in GitLab

Beispiel: Projektmanagement in GitLab

I Milestones legen Ziele fur ein Projekt fest

I Issue Tracker dienen dazu, identifizierte Bugs, Probleme undVerbesserungsvorschlage (

”Issues“) zu verwalten

I Merge Requests sind Anderungsvorschlage fur Software, dietypischerweise ein Issue beseitigen

Milestones

I Konkrete Kriterien fur das Erreichen des Milestones

I Typischerweise: Ziel-Datum

I Oft: Zusammenfassung von Issues und Merge Requests

I In Scrum Projekten oft Sprintziele

I https://gitlab.com/gitlab-org/gitlab-ce/milestones

I https://gitlab.com/gitlab-org/gitlab-ce/milestones/19

https://gitlab.com/gitlab-org/gitlab-ce/milestones

https://gitlab.com/gitlab-org/gitlab-ce/milestones/19

Liste aller Milestones

Milestone

Issues

I Issue: ein konkretes Problem bzw. ein Verbesserungsvorschlagfur Software

I Angabe des Problems / der gewunschten Verbesserung

I Typischerweise: Wie kann das Problem reproduziert werden?

I Oft: Wer ist verantwortlich

I Oft: Klassifikation nach verschiedenen Kriterien (z.B.Bug/Feature Request oder Critical/Normal/Low Priority)

I Issues werden geschlossen, wenn sie nicht mehr aktuell sind

I https://gitlab.com/gitlab-org/gitlab-ce/issues

I https://gitlab.com/gitlab-org/gitlab-ce/issues/10982

I https://gitlab.com/gitlab-org/gitlab-ce/issues/10242

https://gitlab.com/gitlab-org/gitlab-ce/issues

https://gitlab.com/gitlab-org/gitlab-ce/issues/10982

https://gitlab.com/gitlab-org/gitlab-ce/issues/10242

Liste aller Issues

Issue 1

Issue 2

Versionskontrolle und Merge Requests

I Verteilte Versionskontrollsysteme (wie z.B. Git) ermoglichenes, dass jeder Entwickler sein eigenes Repository hat

I Es ist moglich verschiedene Varianten der Software(”Branches“) in einem Repository zu haben, Z.B.I master: Stabile Version der SoftwareI devel: EntwicklungsversionI 1.0, 1.1, 2.0: Release-Versionen der Software

I Entwicklung von Features erfolgt of in Feature-Branches

I Nach Abschluss der Entwicklung wird der Feature-Branch inden master- bzw. devel-Brach integriert (

”gemerged“)

I Bei kleinen Projekten integriert oft jeder Entwickler seineAnderungen selber

I Bei großeren Projekten oder Open-Source Projekten werdenoft Merge-Requests verwendet

Branches

Merge Requests

Merge Request

Statische Verifikation und Validierung II

Verifikation mit formalen Methoden

Formale Methoden und Verifikation

I Formales Modell des Systems dient als SpezifikationI Mathematische Analyse des Modells

I Ubersetzung in detailliertere, semantisch aquivalenteReprasentation

I Formaler Beweis, dass das System gewisse Eigenschaften erfullt

I Anwendung in verschiedenen Phasen der EntwicklungI Analyse der Spezifikation auf InkonsistenzenI Verifikation, dass der Programmcode konsistent mit seiner

Spezifikation ist

I Programmentwicklung typischerweise durch Transformation


I Verschiedene Techniken mit unterschiedlicherAusdrucksmachtigkeit, unterschiedlichemAutomatisierungsgrad

I Grundidee:I Modell/Programm in geeignetem FormalismusI Aussagen uber das Modell/Programm, typischerweise in einer

LogikI Model Checker, Theorembeweiser, etc. der beim Beweis, dass

die Aussage fur das Programm gilt, hilft (oder ihnvollautomatisch durchfuhrt)

I Je ausdrucksmachtiger die zugrunde liegende Logik undModellierungssprache sind, desto mehr manuellerBeweisaufwand ist in der Regel erforderlich


I Proponenten formaler Techniken fuhren hohereSystemsicherheit und -zuverlassigkeit als Grund fur ihrenEinsatz an

I Formale Techniken ermoglichen Garantien, die mit anderenMethoden nicht erreicht werden konnen

Aber:

I Die formale Spezifikation, die zum Einsatz dieser Methodenerforderlich ist, kann von den Benutzeranforderungenabweichen

I Der formale Beweis kann Fehler enthalten, falls er nichtvollstandig automatisiert ist (und selbst dann konnen dieTools fehlerhaft sein)

I In Spezifikation und Beweis konnen falsche Annahmen uberdie Verwendung des Systems gemacht werden

PVS: Analyse von Spezifikationen

PVS (Prototype Verification System) ist ein System mit demSpezifikationen auf Konsistenz bzw. gewunschteSystemeigenschaften uberpruft werden konnen.

PVS bestehe aus einer ausdrucksstarken Logik und eineminteraktiven Theorembeweiser. Das PVS-System ist Open Sourceund kann von der URL http://pvs.csl.sri.com/

heruntergeladen werden.

http://pvs.csl.sri.com/

PVS: Analyse von Spezifikationen

In PVS werden Axiome und zu beweisende Aussagen in einerTheorie zusammengefasst. Eine Theorie enthalt

I Deklarationen von Sorten (Typen)

I Deklarationen von Variablen und Konstanten

I Deklarationen und Definitionen von Funktionen

I Axiome

I Zu beweisende Aussagen

Beispiel

family: THEORY

BEGIN

person: TYPE+

betty, carol, joe: person

c, f, m, p, q, r, x, y, z: VAR person

father(p): person

mother(p): person

...

END family

Beispiel

parent(p, c): bool

is_male(p): bool

is_female(p): bool

all_names_are_different: AXIOM

betty /= carol & betty /= joe & carol /= joe

betty_is_parent_of_carol: AXIOM parent(betty, carol)

joe_is_father_of_carol: AXIOM father(carol) = joe

Beispiel

father_is_parent: AXIOM parent(father(c), c)

mother_is_parent: AXIOM parent(mother(c), c)

father_is_male: AXIOM

(exists c: f = father(c)) => is_male(f)

mother_is_female: AXIOM

(exists c: m = mother(c)) => is_female(m)

male_is_not_female: AXIOM

is_male(x) <=> not(is_female(x))

parent_is_either_father_or_mother: AXIOM

parent(p, c) <=> (p = father(c) OR p = mother(c))

father_is_not_mother: AXIOM

father(c) /= mother(c)

Beispiel

joe_is_male: PROPOSITION

is_male(joe)

betty_is_mother_of_carol: PROPOSITION

mother(carol) = betty

Beweis in PVS

Installing rewrite rule sets.singleton_rew (all instances)

joe_is_male :

|-------

{1} is_male(joe)

Rule? (lemma "joe_is_father_of_carol")

Applying joe_is_father_of_carol

this simplifies to:

joe_is_male :

{-1} father(carol) = joe

|-------

[1] is_male(joe)

Beweis in PVS

joe_is_male :

{-1} father(carol) = joe

|-------

[1] is_male(joe)

Rule? (lemma "father_is_male")

Applying father_is_male

this simplifies to:

joe_is_male :

{-1} FORALL (f: person):

(EXISTS c: f = father(c)) => is_male(f)

[-2] father(carol) = joe

|-------

[1] is_male(joe)

Beweis in PVS

joe_is_male :




|-------

[1] is_male(joe)

Rule? (inst?)

Found substitution:

f: person gets joe,

Using template: is_male(f)

Instantiating quantified variables,

this simplifies to:

Beweis in PVS

joe_is_male :




|-------

[1] is_male(joe)

Rule? (inst?)

...

joe_is_male :

{-1} (EXISTS c: joe = father(c)) => is_male(joe)


|-------

[1] is_male(joe)

Beweis in PVS

joe_is_male :

{-1} (EXISTS c: joe = father(c)) => is_male(joe)


|-------

[1] is_male(joe)

Rule? (split)

Splitting conjunctions,

this yields 2 subgoals:

Beweis in PVS

joe_is_male.1 :

{-1} is_male(joe)


|-------

[1] is_male(joe)

which is trivially true.

This completes the proof of joe_is_male.1.

Beweis in PVS

joe_is_male.2 :


|-------

{1} EXISTS c: joe = father(c)

[2] is_male(joe)

Rule? (inst?)

Found substitution:

c gets carol,

Using template: father(c)


this simplifies to:

Beweis in PVS

joe_is_male.2 :


|-------

{1} EXISTS c: joe = father(c)

[2] is_male(joe)

Rule? (inst?)

...

joe_is_male.2 :


|-------

{1} joe = father(carol)

[2] is_male(joe)

Beweis in PVS

joe_is_male.2 :


|-------

{1} joe = father(carol)

[2] is_male(joe)

Rule? (grind)

Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of joe_is_male.2.

Q.E.D.

Run time = 0.44 secs.

Real time = 104.163 secs.

NIL

*

Beweis in PVS

Installing rewrite rule sets.singleton_rew (all instances)

betty_is_mother_of_carol :

|-------

{1} mother(carol) = betty

Rule? (auto-rewrite-theory "family")

Rewriting relative to the theory: family,

this simplifies to:

Beweis in PVS


|-------

[1] mother(carol) = betty

Rule? (lemma "betty_is_parent_of_carol")

Applying betty_is_parent_of_carol

this simplifies to:


{-1} parent(betty, carol)

|-------


Beweis in PVS


{-1} parent(betty, carol)

|-------


Rule? (lemma "parent_is_either_father_or_mother")

Applying parent_is_either_father_or_mother

this simplifies to:


{-1} FORALL (c, p: person):


[-2] parent(betty, carol)

|-------


Beweis in PVS





|-------


Rule? (inst?)

Found substitution:

c: person gets carol,

p: person gets betty,

Using template: parent(p, c)


this simplifies to:

Beweis in PVS





|-------


Rule? (inst?) ...


{-1} parent(betty, carol) <=>

(betty = father(carol) OR betty = mother(carol))


|-------


Beweis in PVS


{-1} parent(betty, carol) <=>



|-------


Rule? (lemma "father_is_not_mother") ...


{-1} FORALL (c: person): father(c) /= mother(c)

[-2] parent(betty, carol) <=>



|-------


Beweis in PVS

{-1} FORALL (c: person): father(c) /= mother(c)




|-------


Rule? (inst?) ...

{-1} father(carol) /= mother(carol)




|-------


Beweis in PVS

{-1} father(carol) /= mother(carol)




|-------


Rule? (lemma "all_names_are_different") ...

{-1} betty /= carol & betty /= joe & carol /= joe

[-2] father(carol) /= mother(carol)




|-------


Beweis in PVS


{-1} betty /= carol & betty /= joe & carol /= joe

[-2] father(carol) /= mother(carol)




|-------


Rule? (grind)


Q.E.D.

PVS

Wie man schon an diesem kleinen Beispiel sieht, sind Spezifikationund Beweise mit PVS (und anderen formalen Methoden) relativaufwandig.

Man kann die manuelle Arbeit manchmal durch die Definitiongeeigneter Beweisstrategien reduzieren. Fur manche Theorienkonnen Beweise auch durch die in PVS eingebautenEntscheidungsprozeduren automatisiert werden.

Beispiel: Addierer

Beispiel: Addierer in PVS

FullAdder: THEORY

BEGIN

x, y, cin: VAR bool

FA(x, y, cin): [bool, bool] =

((x AND y) OR ((x XOR y) AND cin),

(x XOR y) XOR cin)

bool2nat(x): nat = IF x THEN 1 ELSE 0 ENDIF

FA_corr: THEOREM

LET (carry, sum) = FA(x, y, cin) IN

bool2nat(sum) + 2 * bool2nat(carry) =

bool2nat(x) + bool2nat(y) + bool2nat(cin)

END FullAdder

Beispiel: Addierer in PVS – Beweis

FA_corr :

|-------

1 FORALL (cin, x, y: bool):

LET (carry, sum) = FA(x, y, cin) IN


bool2nat(x) + bool2nat(y) + bool2nat(cin)

Rule? (skolem!)

Skolemizing,

this simplifies to:

FA_corr :

|-------

1 LET (carry, sum) = FA(x!1, y!1, cin!1) IN


bool2nat(x!1) + bool2nat(y!1) + bool2nat(cin!1)

Beispiel: Addirer in PVS – Beweis

. . .

Beispiel: Addierer in PVS – Beweis

FA_corr.2 :

|-------

1 (x!1 XOR y!1) XOR cin!1

2 0 +

2 *

IF (x!1 AND y!1) OR ((x!1 XOR y!1) AND cin!1) THEN 1 ELSE 0 ENDIF

=

IF x!1 THEN 1 ELSE 0 ENDIF + IF y!1 THEN 1 ELSE 0 ENDIF +

IF cin!1 THEN 1 ELSE 0 ENDIF

Rule? (grind)


This completes the proof of FA_corr.2.

Q.E.D.

ACL2: Verifikation von Programmen

ACL2 ist eine auf Lisp basierende, funktionaleProgrammiersprache, die es erlaubt, Programme mit einemautomatischen Theorembeweiser zu verifizieren.

ACL2: Beispiel

(defun insert (x xs)

(cond ((atom xs)

(list x))

((<= x (first xs))

(cons x xs))

(t

(cons (first xs) (insert x (rest xs))))))

(defun insertion-sort (xs)

(if (atom xs)

’()

(insert (first xs)

(insertion-sort (rest xs)))))

ACL2: Beispiel

(defun is-sorted-p (xs)

(if (or (endp xs) (endp (rest xs)))

t

(and (<= (first xs) (second xs))

(is-sorted-p (rest xs)))))

(defthm result-of-insertion-sort-is-sorted

(is-sorted-p (insertion-sort xs)))

ACL2: Beispiel

Haben wir durch den Beweis vonresult-of-insertion-sort-is-sorted gezeigt, dassinsertion-sort einen korrekten Sortieralgorithmusimplementiert?

ACL2: Beispiel


’())

Offensichtlich erfullt auch diese Implementierung das Theoremresult-of-insertion-sort-is-sorted. . .

ACL2: Beispiel

. . . und noch schlimmer: diese Implementierung


’(1 2 3))

Wir mussen also noch zeigen, dass das Ergebnis des Sortierens einePermutation der ursprunglichen Eingabeliste ist

ACL2: Beispiel

(defun in (x xs)

(cond ((atom xs) nil)

((equal x (first xs)) t)

(t (in x (rest xs)))))

(defun del (x xs)

(cond ((endp xs) ’())

((equal x (first xs)) (rest xs))

(t (cons (first xs)

(del x (rest xs))))))

(defun perm (xs ys)

(if (endp xs)

(endp ys)

(and (in (first xs) ys)

(perm (rest xs) (del (first xs) ys)))))

ACL2: Beispiel

(defthm insert-is-permutation-of-cons

(implies (perm xs ys)

(perm (insert x xs) (cons x ys))))

(defthm insertion-sort-is-permutation-of-input

(perm (insertion-sort xs) xs))

Testen

Ziele des Testens

I Zeigen, dass das Programm seine Anforderungen erfulltI Fur EntwicklerI Fur KundenI Standardsoftware: Mindestens ein Test pro FeatureI Individualsoftware: Mindestens ein Test pro Requirement/User

Story

I Finden von Fehlern bevor das System ausgeliefert wirdI SystemabsturzeI Unerwunschte Interaktionen mit anderen SystemenI Falsche Werte von BerechnungenI Zerstorung von DatenI Abweichungen des Systemverhaltens von der Spezifikation

Wer entwickelt Tests und fuhrt sie aus?

I Fruher war es ublich, dass Tests ausschließlich von einemspezialisierten Test-Team durchgefuhrt wurden

I Heutzutage ist es ublich, dass Programmierer Tests schreiben,die die Funktion der einzelnen Komponenten testen

I Je nach Art und Große des Projekts und nach verwendetemSoftwareprozess werden Tests fur großere Subsysteme oderdas ganze System auch vom Entwicklungsteam oder voneinem Test-Team entworfen und ausgefuhrt.

I Das zu testende System wird manchmal als SUT (Systemunder Test) bezeichnet

Konnen Tests Fehlerfreiheit sicherstellen?

Nein.

Durch Testen kann nicht sichergestellt werden, dass ein Systemkeine Fehler hat. Man kann nur sicherstellen, dass die getestetenSzenarien funktionieren.

”Testing can only show the presence of errors, not their absence“

(Dijkstra, 1972)

Bezeichnungen (nach ISO 9000/IEEE 610)

I Fehler: Abweichung des Ist vom Soll, wenn sie dievordefinierte Toleranzgrenze uberschreitet, d.h. zu großeAbweichung zwischen beobachten, ermittelten oderberechneten Zustanden oder Verhalten und festgelegten,korrekten Zustanden oder Vorgangen. Zusammengesetzt aus:

I Fehlhandlung (Error): Die Handlung, die zu einemFehlerzustand fuhrt

I Fehlerzustand (Defect): Defekt in einer Komponente odereinem System, der eine geforderte Funktion des Produktsbeeintrachtigen kann

I Fehlerwirkung (Failure): Die Manifestierung eines innerenFehlers bei der Ausfuhrung des Programms als in inkorrektesVerhalten oder Resultat bzw. als Versagen des Systems

Bemerkungen

I Eine Fehlhandlung fuhrt zu einem Fehlerzustand, der eineFehlerwirkung hervorruft. (Errors introduce defects thatultimately result in failures)

I Fehlerzustande konnen durch Anforderungen, Entwurf oderImplementierung entstehen

I Seltenes Auftreten von Fehlerwirkungen ist ein Maß fur dieZuverlassigkeit eines Systems

I Fehlerwirkungen konnen durch die Verletzung expliziter oderimpliziter Anforderungen entstehen

Klassifikation von Tests nach Zielen

I Validierungstesten (”validation testing“): versucht

sicherzustellen, dass das System seine intendierte Funktionkorrekt erfullt

I Defekttesten (”defect testing“): versucht Fehler (eigentlich

Fehlerzustande) zu findenI selten betrachtete Ausfuhrungspfade oder User CasesI Randbedingungen

I Die Ubergange zwischen den beiden Klassen sind fließend

Klassifikation von Tests nach relativer Große des SUT

I Unit Tests: Testen einzelner Methoden oder Klassen,typischerweise isoliert vom Rest des Systems

I Komponententests: Testen einzelner Komponenten inIsolation

I Integrations/Systemtests: Testen das komplette System.

Andere Bezeichnungen/Testarten

I Regressionstests: Tests, die bereits behobene Fehler testen.Sollen sicherstellen, dass diese Fehler nicht erneut ins Systemgelangen konnen.Regressionstests konnen Unit-, Komponenten- oderIntegrations/Systemtests sein

I Performanztests: Tests, die das Verhalten des Systems unterBelastung uberprufen (Lasttests, Stresstests, Spike-Tests, . . . )

I Benutzbarkeitstests (Usability Tests): Tests, dieuberprufen, wie gut Benutzer mit dem System zurechtkommen

Klassifikation von Tests nach Zeitpunkt

I Entwicklungstests: Das System wird wahrend derEntwicklungsphase getestet.Werden i.A. von den Entwicklern selber ausgefuhrt

I Release Tests: Eine vollstandige Version des Systems wirdgetestet bevor es an Kunden ubergeben wird.Werden oft von einem speziellen Test-Team ausgefuhrt

I Endbenutzertests: Benutzer oder potentielle Benutzer testendas System, oft in ihrer eigenen Systemumgebung.Akzeptanztests sind eine Form der Endbenutzertests

Teststrategien

I White-Box vs. Black-Box

I Top-down vs. Bottom-up

White-Box Tests

I Auch Glass-Box oder strukturelles Testen genanntI Tester haben Zugriff auf Design und Implementierung des

Systems und konnenI die Design-Dokumente lesenI den Code inspizieren

um potentielle Fehler zu finden

I Wenn Programmierer Tests fur ihren eigenen Code schreibenhandelt es sich immer um White-Box Tests

Black-Box Testing

I Tester konnen das Systemverhalten (z.B. Ausgaben) fur vonihnen gewahlte Eingaben uberprufen

I Tester haben keinen Zugriff auf Systeminterna

I (Klassisches) Fuzzing ist eine automatisierte Form desBlack-Box Testens

I Haben Tester Zugriff auf die Design-Dokumente aber nichtden Programmcode spricht man manchmal vomGray-Box-Testing

Einfuhrung in Unit Testing

Was sind Unit Tests?

I Tests vonI FunktionenI MethodenI KlassenI Einfachen Komponenten

I FeingranularI Methodenaufruf mit verschiedenen Parametern

I Keine Interaktion zwischen getesteter Einheit und Rest desSystems

I Isolierte TestfalleI Benotigte Subsysteme werden durch Simulationen ersetzt

(Mocks)

Grunde fur das Unit-Testen

I Fruhes Finden von Fehlern

I Einfachere Lokalisierung von FehlernI

”Sicherheitsnetz“ fur Programmierer

I Fungieren auch als RegressionstestsI Fehler werden (hoffentlich) gefunden, bevor sie das

Gesamtsystem beeinflussen

I Unterstutzen Wartbarkeit und Erweiterbarkeit von CodeI Erleichtern Refactoring, da viele dabei auftretende Fehler

durch Unit-Tests gefunden werdenI Stellen sicher, dass Erweiterungen die existierende

Funktionalitat nicht beeintrachtigen

I Dienen als zusatzliche DokumentationI Konnen aber Architekturdiagramme, etc. nicht ersetzen

Richtlinien fur Unit Tests

Unit Tests sollen

I automatisiert sein

I einzelne Programmelemente isoliert testen

I zu jedem Zeitpunkt erfolgreich ausfuhrbar sein

I nicht viel Zeit zur Ausfuhrung brauchen

I fur alle Systembestandteile geschrieben werden

I alle wichtigen Zustande jedes getesteten Elements abdecken

Spater: detailliertere Richtlinien - FIRST, Right-BICEP, CORRECT

Praktisches Testen

Terminologie

I Test oder Test CaseI Aktion, die auf dem getesteten Element ausgefuhrt wirdI Resultat (und evtl. Ausgabe) der Aktion bestimmen, ob das

getestete Element (in der getesteten Situation) korrekt arbeitetI Oft wird zusatzliche Information angegeben (Eindeutige ID,

Name, Beschreibung, . . . )

I TestsuiteI Zusammenfassung von Tests und/oder TestsuitesI Kann als Einheit ausgefuhrt werdenI Aggregiert die Ergebnisse der Testausfuhrung

I FixtureI Kontext, in dem ein Test stattfindet

I Zustand eines ObjektsI Umgebung des Testelements

I Enthalt oft Stubs/Mocks fur Teile des Systems, die nichtgetestet werden

Mogliche Ergebnisse von Tests

I Pass: Der Test wurde beendet und lieferte das gewunschteErgebnis

I Fail: Der Test wurde beendet und lieferte nicht dasgewunschte Ergebnis

I Error: Der Test lieferte kein Ergebnis, er wurde mit einerunerwarteten Exception beendet oder das Programm istabgesturzt

Erschopfendes Testen

Erschopfendes Testen (d.h., das Schreiben von Tests, die allemoglichen Eingaben eines Programms abdecken) ist nicht moglich.

Beispiel Passworteingabe:

I Angenommen Passworter mit maximal 20 Zeichen sindzulasig, 80 Eingabezeichen sind erlaubt (große und kleineBuchstaben, Sonderzeichen)

I Das ergibt

8020 = 115.292.150.460.684.697.600.000.000.000.000.000.000

mogliche Eingaben

I Bei 10ns fur einen Test wurde man ca. 1024 Jahre brauchenum alle Eingaben zu testen

Effektivitat und Effizienz von Unit Tests

Unit Tests sollen effektiv und effizient sein

I Effektiv: Die Tests sollen so viele Fehler wie moglich finden

I Effizient: Wir wollen die großte Anzahl an Fehlern mit dergeringsten Anzahl an moglichst einfachen Tests finden

Effizienz ist wichtig, da Tests selber Code sind, der gewartetwerden muss und Fehler enthalten kann.

Strategien zum Finden von Tests

I Analyse von Randwerten (Boundary Value Analysis, BVA)

I Partitionierung

I Zustandsbasiertes Testen

I Kontrollflussbasiertes Testen

I Richtlinien

I Kenntniss haufiger Fehler

Boundary Value Analysis

I Viele Fehler treten am”Rand“ des Definitionsbereichs von

Funktionen oder Prozeduren aufI Eine gute Strategie zum effizienten Testen ist es daher,

derartige Randwerte zu betrachtenI Der/die letzten gultigen WerteI Werte, die gerade außerhalb des Definitionsbereichs liegen

I Ist z.B. eine Funktion fur ganzzahlige Werte zwischen 0 und 5definiert, so kann sie mit Eingaben −1, 0, 5 und 6 getestenwerden

Boundary Value Analysis

Vorteil:

I Man konzentriert sich auf empirisch haufige Fehlerquellen

Schwierigkeiten:

I Bei vielen Bereichen ist nicht klar, was”Randwerte“ sind

(Allerdings lassen sich oft alternative Kriterien finden, z.B.Lange von Collection-Argumenten)

I Werte außerhalb des Definitionsbereichs konnen manchmal zuundefiniertem Verhalten fuhren

I Bei Funktionen mit vielen Parametern gibt es einekombinatorische Explosion von Randwerten.

Merkregel fur BVA: CORRECT

I Conformance: Entspricht der Wert einem erwarteten Format?

I Ordering: Sind die moglichen Werte geordnet oderungeordnet?

I Range: Hat der Wert einen minimalen und/oder maximalenWert?

I Reference: Hat der Code externe Referenzen, die nicht unterseiner Kontrolle sind?

I Exist: Existiert der Wert (ist er nicht null, in einervorgegebenen Menge enthalten, . . . )

I Cardinality: Sind genug Werte vorhanden? Sind zu viele Wertevorhanden?

I Time: Sind die Werte zum benotigten Zeitpunkt verfugbar? Inder erwarteten Reihenfolge?

Partitionierung

Argumente von Funktionen, Ein/Ausgabe des Programms undZustande von Klassen konnen oft in Aquivalenzklassen unterteiltwerden, so dass

I Das Verhalten fur Elemente aus der gleichen Aquivalenzklasseahnlich ist (z.B. den gleichen Kontrollflusspfad nimmt)

I Elemente aus unterschiedlichen Klassen verschiedeneVerhalten zeigen

I Beispiel: Die Argumente der sqrt-Funktion konnen unterteiltwerden in

I Positive Zahlen und 0I Negative Zahlen

Eine feinere Unterteilung ware zusatzlich in Quadratzahlenund Nicht-Quadratzahlen

Eine derartige Aquivalenzklasse heißt Partition oder Domane.

Partitionierung

Finde Partitionen fur das getestete Element und teste diefolgenden Elemente

I Einen Wert aus der”Mitte“ der Partition

I Einen Wert auf oder nahe jeder Partitionsgrenze

Haufig findet man Partitionen durch BVA.

Beispiel:

Um die Quadratwurzelfunktion zu testen, schreibe Tests fur

I sqrt(0.0)

I sqrt(2.0)

I sqrt(-2.0)

Zustandsbasiertes Testen

Hat man das Verhalten eines Objekts zurch ein Zustandsdiagrammangegeben, so kann man sich beim Testen an den Zustanden undTransitionen orientieren

I Ein zustandsbasierter Test wird durch eine Folge von Eventsbeschrieben, die die Zustandsmaschine steuern.

I Die erwarteten Resultate sindI die Zustande (falls beobachtbar) undI die Aktivitaten bzw. Ausgaben

die durch die Eingabeevents verursacht werdenI Es gibt verschiedene Methoden um

I fehlerhafte Aktivitaten bzw. AusgabenI falsche Zustandsubergange

zu finden

Zustandsbasiertes Testen

Wir besprechen zwei Testverfahren, die fur Zustandsmaschinengeeignet sind, bei denen die Zustande nicht direkt beobachtbarsind

I”Transitions-Touren“ (Transition Tours, TT) und

I unterscheidende Sequenzen (distinguishing Sequences, DS)

Transition Tour (TT)

I Beim Testen einer Transition Tour erzeug man eine Sequenzvon Events, die

I beginnend beim AnfangszustandI jede Transition mindestens einmal durchlauft undI wieder beim Anfangszustand ankommt

I Das geht nicht fur jede Zustandsmaschine

I Transition Tours sind leicht zu finden, falls sie existieren

I TT ergibt kurze Testfalle

I TT kann fehlerhafte Aktivitaten/Ausgaben erkennen, abernicht Fehler in den Zustandsubergangen

Distinguishing Sequence (DS)

I Eine Folge von Events ist eine unterscheidende Sequenz(distinguishing Sequence (DS), falls sie fur jeden Zustand eineunterschiedliche Folge von Aktivitaten/Ausgaben erzeugt

I Idee: Verwende DS um fehlerhafte Zustandsubergange zufinden:

I Fur jeden Zustand: fuhre die DS beginnend von diesemZustand aus

I Falls die Ausgabe von der erwarteten Ausgabe fur diesenZustand abweicht liegt ein Fehler im Zustandstransfer vor (fallsdie Aktivitaten/Ausgaben jeder Transition als korrekt uberpruftwurden)

I DS mussen systematisch ausprobiert werdenI Beginne mit Anfangszustand, fuhre DS ausI Fuhre vom Anfangszustand aus Transitionen aus, die in einen

anderen Zustand fuhren, fuhre DS fur diesen Zustand ausI So lange, bis die DS fur alle Zustande ausgefuhrt wurde

Distinguishing Sequence (DS)

I Kann fehlerhafte Zustandsubergange erkennen und denfehlerhaften Zustand lokalisieren

I Gut fur die Uberprufung von Protokollkonformanz

I Benotigt die Moglichkeit, die Zustandsmaschine in denStartzustand zuruckzuversetzen

I Existenz einer DS ist nicht garantiert (benotigt eine minimaleZustandsmaschine)

I Berechnung der DS ist aufwandig (exponentiell in der Großeder Zustandsmaschine)

Kontrollflussbasiertes Testen

I Der Kontrollfluss-Graph (CFG) eines Programms ist eingerichteter Graph, der die Kontrollstruktur eines Programmsreprasentiert

I Knoten sind Basic Blocks (lineare Folgen von Anweisungen)I Kanten reprasentieren mogliche Programmablaufe

I Fallunterscheidungen: Knoten mit mehreren Nachfolgern

I Schleifen im Programm fuhren zu Schleifen im CFG


if (x == 0) {

print "x == 0"

print "This is interesting."

} else {

print "x != 0"

print "The boring case."

}

print "Hello, world!"


Mit dem CFG kann man verschiedene Maße fur die

”Testabdeckung“ des Programms definieren

I Anweisungsuberdeckung (Statement Coverage): DerProzentsatz and Programmanweisungen (Knoten im CFG),der durch die Tests abgedeckt wird. Eine Test Suite hat 100%Anweisungsuberdeckung wenn jede Programmanweisungdurch mindestens einen Test abgedeckt wird

I Entscheidungsuberdeckung (Branch Coverage, DecisionCoverage): Der Prozentsatz an Kanten im CFG der von Testsabgedeckt wird. Eine Test Suite hat 100%Entscheidungsuberdeckung wenn jede mogliche Verzweigungim Programm von einem Test abgedeckt wird, d.h., wenn jedeKante im CFG von einem Test durchlaufen wird.

I 100% Entscheidungsuberdeckung impliziert 100%Anweisungsuberdeckung aber nicht umgekehrt

Richtlinien

I Reprasentieren projekt- oder domanenspezifisches Wissen

I Konnen erweitert werden wenn Defekte gefunden werden, dienicht von bisherigen Tests erfasst wurden

Beispiele fur Richtlinien

I Schreibe Unit Tests, die jede mogliche Fehlermeldung triggern

I Teste jede Funktion, die einen Buffer verwendet mit einerEingabe, die großer als die maximale Buffergroße ist

I Teste gecachte Funktionen mehrmals mit der gleichenEingabe und stelle sicher, dass sich die Ausgabe nicht andert

I Teste jede Funktion mit Eingaben, die außerhalb des gultigenDefinitionsbereichs liegen

I Teste jede Funktion, die eine Collection als Eingabeparameterhat mit der leeren Collection und mit einelementigenCollections

I Verwende Collections verschiedener Große in Tests

I Stelle sicher, dass auf Elemente von Anfang, Mitte und Endeeiner Collection zugegriffen wird (falls moglich)

Einige”Haufige Fehler“

I Falsche Boole’sche BedingungenI Betrachte Partitionen, die durch Bedingungen generiert werdenI Betrachte die Randwerte von Bedingungen

I Nichtterminierende BerechnungenI Vergessene/unvollstandige Basisfalle in rekursiven Funktionen

(z.B. Test auf = 0 statt <= 0)I Unvorhergesehenes Inkrement/Dekrement des Zahlers in for

oder while-Schleifen

I Falsche Vorbedingungen fur CodeI Schreibe Assertions im Code, die Vorbedingungen uberprufenI Schreibe Tests, die diese Assertions triggern

I Falsche InvariantenI Schreibe Funktionen, die Invarianten testen, sofern diese auf

nicht-zugreifbarem Zustand beruhenI Schreibe Tests, die diese Funktionen verwenden


I Nullpointer, nicht-initialisierter SpeicherI Im allgemeinen schwer durch Tests zu finden; verwende Tools

wie Valgrind und schalte Compilerwarnungen ein, fallsverfugbar

I Versuche Partitionen zu finden, die Werte uninitialisiert lassen

I Ungewohnliche BereicheI Leere oder einelementige CollectionsI Sehr kleine Werte (z.B. 1.0e-300)I Sehr große Werte oder Collections

I Off-by-One, Zaunpfahl-Fehler (Fencepost Errors)I Teste, dass Schleifen nicht zu oft oder zu selten durchlaufen

werdenI Verwende for-in falls moglich


I Falsche OperatorprazedenzI Uberprufe, dass Formeln auch die erwartete Bedeutung habenI Versuche Partitionen zu finden, die das sicherstellen

I Ungeeignete AlgorithmenI Schlechte LaufzeiteigenschaftenI Uber-/Unterlauf fur bestimmte Eingaben

I Ungeeignete Reprasentation von DatenI Gleitkommazahlen fur GeldbetrageI Darstellung von Werten, die nur aus Ziffern bestehen konnen

(z.B. Bankleitzahlen, Kontonummern) durch int-Werte(fuhrende Nullen, Lange der Reprasentation)

I Zu wenige Werte fur produktiven Einsatz, z.B. 8-bit User-ID

Einige”Haufige Fehler“ bei numerischen Berechnungen

I Verwendung inexakter Reprasentationen wo eine exakteReprasentation notig ware

I Z.B. Gleitkommazahlen fur Bruche

I Verwendung von Gleitkommazahlen mit zu geringer Prazision

I Verwendung instabiler AlgorithmenI Durchfuhrung numerischer Berechnungen ohne Rucksicht auf

Ordnung der OperationenI Kann numerischen Fehler drastisch vergroßern

Umfang der Unit Tests

Unit Tests sollen die getestete Einheit moglichst komplettabdecken

I Funktionen/MethodenI Aufruf mit Parametern aus jeder Input-Partition

I Klassen/ObjekteI Test aller relevanten OperationenI Mindestens ein Test fur jede ZustandspartitionI Tests fur alle moglichen ZustandstransitionenI Tests, die sicherstellen, dass geerbte Attribute und

Operationen wie gewunscht funktionieren

Kriterien fur Unit-Tests: FIRST

I FastI Jeder Test benotigt hochstens einige Millisekunden Laufzeit

I IsolatedI Test beschranken sich auf eine geringe Menge an Code und

sind vom Rest des Systems isoliertI Tests sind voneinander isoliert, Reihenfolge der Ausfuhrung

spielt keine Rolle

I RepeatableI Das Ergebnis des Tests sollte immer identisch seinI Haufige Probleme: Zeit, Datum

I Self-ValidatingI Es sollte keine externe Verifikation notig sein (z.B. manuelle

Inspektion der Testausgabe)

I TimelyI Unit-Tests sollten zusammen mit dem Code, den sie testen

erstellt werden

Was bzw. wie soll getestet werden? Right-BICEP

I Sind die Ergebnisse/Ausgaben des Programms korrekt (right)I

”Happy-Path Tests“ - Validierungstesten

I Boundary Conditions: Werden Randwerte korrekt behandelt?

I Inverse Relationships: Ist es sinnvoll die inverse Beziehung zutesten? (Beispiel: Quadratwurzel)

I Cross-Checking: Konnen Ergebnisse durch”Gegenprobe“

verifiziert werden? (Beispiel: langsamer aber einfacherAlgorithmus)

I Forcing Error Conditions: Konnen Fehlerbedingungenerzwungen werden?

I”Unhappy-Path Tests“ - Defekttesten

I Performance Characteristics: Ist die Performance derImplementierung ausreichend? Skaliert die Implementierung?

Bewertung: Statische Methoden versus Testen

Vorteile von statischen V&V-Techniken gegenuber Tests

I Interaktionen zwischen/”verspatete Effekte“ von Fehlern sind

beim Testen oft schwer zu finden

I Unvollstandige/nicht kompilierbare Systeme konnen uberpruftwerden (insbesondere bei Inspektionen/Reviews)

I Inspektionen konnen nicht nur Fehler finden sondern auchI die Qualitat der Modelle und des Codes uberprufen,I uberprufen ob Entwicklungsprozess und System die

erforderlichen Standards einhalten,I potentielle zukunftige Probleme identifizieren

I Formale Methoden konnen Korrektheit bezuglich derSpezifikation garantieren, sind aber aufwandig und teuer

I Formale Methoden konnen Randbedingungen identifizieren,die andernfalls vergessen werden

Vorteile des Testens

I Tests konnen automatisiert werdenDamit konnen Tests immer wieder ausgefuhrt werden umRegressionen zu finden

I Tests konnen Probleme identifizieren, die aus unerwartetenInteraktionen von Subsystemen resultieren

I Tests konnen Hinweise auf die Stellen im Code geben, dieFehler verursachen

I Tests konnen Fehler finden, die in Codereviews nur schwer zufinden sind

I Testen ist erheblich schneller und billiger als formaleVerifikation

Refactoring

Refactoring

I Verbesserung der internen Struktur des Codes ohne seineFunktionalitat oder sein beobachtbares Verhalten zubeeinflussen

I Ausgelost durchI Code SmellsI Gewunschtes Verhalten, das nicht gut zur momentanen

Struktur des Codes passt

I Katalog von Refactorings

I Oft Unterstutzung durch Entwicklungsumgebung

I Nur moglich, wenn automatische Validierung des Codesgegeben ist (typischerweise durch Tests)

Code Smells

I Lange Methoden

I Duplizierter Code

I Komplizierte Bedingungen

I Shotgun Surgery

I Feature Envy

Refactorings

I Methode/Variable umbenennen

I Lokale Variable extrahieren

I Methode extrahieren

I”Inline Method“

I Feld kapseln

I Methode durch Methoden-Objekt ersetzen

I Feld/Methode in Oberklasse/Unterklasse verschieben

The End

Programmierung und Softwaretechnik (PST) — PST - Veri zieren, … · 2016. 1. 27. ·...

Documents

Transcript of Programmierung und Softwaretechnik (PST) — PST - Veri zieren, … · 2016. 1. 27. ·...