Qualitätssicherung von Software (SWQS)

Prof. Dr. Holger Schlingloff

Humboldt-Universität zu Berlinund

Fraunhofer FOKUS

21.5.2013: Modellprüfung

Folie 2H. Schlingloff, Software-Qualitätssicherung

Fragen zur Wiederholung

• Was ist ein Modell, ein Transitionssystem, ein endlicher Automat?

• Unterschied Systemmodell – Testmodell?

• Testgenerierung aus UML State Machines: Testziele und Überdeckungskriterien?

• Was versteht man unter einer Transition Tour?

• Wie kann man die Effektivität einer Testsuite nachweisen?

Folie 3H. Schlingloff, Software-Qualitätssicherung

Wo stehen wir?

1. Einleitung, Begriffe, Software-Qualitätskriterien2. Softwaretest3. Verifikation und Validierung, Modellprüfung4. statische und dynamische Analysetechniken5. Softwarebewertung, Softwaremetriken6. Codereview- und andere Inspektionsverfahren7. Zuverlässigkeitstheorie, Fehlerbaumanalyse8. Qualitätsstandards, Qualitätsmanagement,

organisatorische Maßnahmen

Folie 4H. Schlingloff, Software-Qualitätssicherung

• Sprachgebrauch im V-Modell Verifikation: Vergleich des Ergebnisses eines

Entwicklungsschritts mit dem vorherigen Validierung: Vergleich des analytischen Artefaktes mit dem

entsprechenden synthetischen Artefakt

• alternativer Sprachgebrauch Verifikation = formaler Beweis

(„entspricht der Code der Spezifikation?“) Validierung = informelle Überprüfung

(„entspricht die Spezifikation den Anforderungen?“)

Verifikation und Validierung

Validierung

Verifikation

Folie 5H. Schlingloff, Software-Qualitätssicherung

Techniken für V&V

•Validierung Requirements Engineering, strukturierte Analyse Konsistenz- und Vollständigkeitsprüfung Schablonentechnik, systematische Fragebögen …

•Verifikation Hoare-Kalkül, mathematische Programmbeweise Modellprüfung, Erreichbarkeitsgraphen interaktive Abstraktions/Verfeinerungsbeweise …

Folie 6H. Schlingloff, Software-Qualitätssicherung

Modellprüfung

• Überprüfung eines formalen Modells des Systems gegenüber einer formalen Spezifikation der Anforderungen

• vollautomatisch für zustandsendliche Systeme

• Modellierung: Automaten, Petrinetze, StateCharts, SDL, …• Spezifikation: temporale Logik, Erreichbarkeit,

Verklemmungsfreiheit, …

Folie 7H. Schlingloff, Software-Qualitätssicherung

Beispiel (nuSMV)

Folie 8H. Schlingloff, Software-Qualitätssicherung

Ein Spielbeispiel

• Wie viele erreichbare Zustände gibt es?

• Wie kann man feststellen, ob ein Zustand erreichbar ist?

Folie 9H. Schlingloff, Software-Qualitätssicherung

Coding in SMV

Folie 10H. Schlingloff, Software-Qualitätssicherung

Coding in SMV (cont.)

• SMV findet sofort eine Lösung (rrddlluurrddlluurrddlluurrdd)

• Lola (Humboldt Univ.) ist sogar noch schneller

• für 3*4 gut machbar, 4*4 machbar, 5*5 nicht machbar (1025)

Folie 11H. Schlingloff, Software-Qualitätssicherung

Ein Hardware-Beispiel

• gibts vielleicht noch besser (color)

Folie 12H. Schlingloff, Software-Qualitätssicherung

Verifikationsmodell des Schieberegisters

Folie 13H. Schlingloff, Software-Qualitätssicherung

Reale Beispiele

•Hardware-Verifikation: Stand der Technik ALUs, PLAs, Memory Controller, Chip

Design, ...

•Software-Verifikation: Stand der Forschung Luftfahrtcomputer, Zugsteuerungen,

Automobil-Steuergeräte, nichttriviale Suchprobleme, ...

http://www-2.cs.cmu.edu/~modelcheck/tour.htm

Folie 14H. Schlingloff, Software-Qualitätssicherung

Another Example: Ivor Spence’s Sudoku

http://www.cs.qub.ac.uk/~I.Spence/SuDoku/sudoku.jar

Folie 15H. Schlingloff, Software-Qualitätssicherung

How Does He Do It?

• Propositional modelling 9 propositions per cell: proposition “ijk” indicates that row i,

column j contains value k individual cell clauses

- each cell contains exactly one value (ij1 v ij2 v … v ij9) ^ ~(ij1 ^ ij2) ^ … ^ ~(ij8 ^ ij9)

row and column clauses- each row i contains each number, exactly once

(i11 v … v i91) ^ (i12 v … v i92) ^ … (i19 v … v i99) j1 j2, k=1..9: ~(ij1k ^ ij2k)

- same for columns block clauses – similar pre-filled cells – easy

• SAT solving 729 propositions, ca. 3200 clauses few seconds

Folie 16H. Schlingloff, Software-Qualitätssicherung

Propositional verification

• In order to validate a system, we need to represent the transition relation.

•The representation is of utmost importance for the success of a verification attempt

•Algorithms and data structures are heavily dependent onto each other

•Needed: representation of sets, relations, boolean formulas, ...

Folie 17H. Schlingloff, Software-Qualitätssicherung

Binary Encoding of Domains

• Any variable on a finite domain D can be replaced by log(D) binary variables similar to encoding of data types by compilers e.g. var v: {0..15} can be replaced by

var v1,v2,v3,v4: boolean(0=0000, 1= 0001, 2=0010, 3=0011, ..., 15=1111)

• State space still in the order of original domain! e.g. three int8-variables can have 224=108 states e.g. buffer of length 10 with 10-bit values 1030

states

• Representation of large sets of states?

Folie 18H. Schlingloff, Software-Qualitätssicherung

Representation of Sets

Folie 19H. Schlingloff, Software-Qualitätssicherung

Ordered Tree Form

•Normal form for propositional formulas

•Uses only the connective Ite

•Linear ordering on the set of propositions e.g., most significant bit first

•Shannon expansion

Folie 20H. Schlingloff, Software-Qualitätssicherung

Truth table and tree form formula

Reduction: Replace Ite (v,ψ,ψ) by ψ

Folie 21H. Schlingloff, Software-Qualitätssicherung

Abbreviations

• Introduce abbreviations

•maximally abbreviated

Folie 22H. Schlingloff, Software-Qualitätssicherung

Binary Decision Trees (BDTs)

•Binary decision tree

•Elimination ofisomorphic subtrees(abbreviations)

Folie 23H. Schlingloff, Software-Qualitätssicherung

Binary Decision Diagrams (BDDs)

• Elimination ofredundant nodes(redundant subformulas) Ite (v,ψ,ψ) by ψ