Qualitätssicherung von Software (SWQS) Prof. Dr. Holger Schlingloff Humboldt-Universität zu Berlin...
-
Upload
andrew-sharp -
Category
Documents
-
view
214 -
download
0
Transcript of Qualitätssicherung von Software (SWQS) Prof. Dr. Holger Schlingloff Humboldt-Universität zu Berlin...
Qualitätssicherung von Software (SWQS)
Prof. Dr. Holger Schlingloff
Humboldt-Universität zu Berlinund
Fraunhofer FOKUS
28.5.2013: Modellprüfung II - BDDs
Folie 2H. Schlingloff, Software-Qualitätssicherung
Existenzgründer gesucht!
Folie 3H. Schlingloff, Software-Qualitätssicherung
Fragen zur Wiederholung
• Unterschied Verifikation – Validierung?
• Wie kann man Sudoku aussagenlogisch beschreiben?
• Wie ist die Komplexität des Erfüllbarkeitsproblems?
• Was versteht man unter Modellprüfung?
• Unterschied Sudoku – Schiebepuzzle?
Folie 4H. 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 5H. Schlingloff, Software-Qualitätssicherung
Representation of Sets
Folie 6H. Schlingloff, Software-Qualitätssicherung
Truth table and tree form formula
Reduction: Replace Ite (v,ψ,ψ) by ψ
Folie 7H. Schlingloff, Software-Qualitätssicherung
Abbreviations
• Introduce abbreviations
•maximally abbreviated
• for any given order of variables the maximal abbreviated form is uniquely determined!
Folie 8H. Schlingloff, Software-Qualitätssicherung
Binary Decision Trees (BDTs)
•Binary decision tree
•Elimination ofisomorphic subtrees(abbreviations)
Folie 9H. Schlingloff, Software-Qualitätssicherung
Binary Decision Diagrams (BDDs)
• Elimination ofredundant nodes(redundant subformulas) Ite (v,ψ,ψ) by ψ
formula: ((V1 V2) V4)
Folie 10H. Schlingloff, Software-Qualitätssicherung
Calculation of BDDs
Folie 11H. Schlingloff, Software-Qualitätssicherung
Boolean operations on BDDs
Folie 12H. Schlingloff, Software-Qualitätssicherung
Satisfiability
•This procedure can be applied for arbitrary boolean connectives (or, and, not) BDD() is the constant node p = (p), (pq) = (pq) etc. direct algorithms for , possible this amounts to set union, intersection, and
complement with respect to the base set
•Formula φ is satisfiable iff BDD(φ) any path through the BDD to T defines a model
Folie 13H. Schlingloff, Software-Qualitätssicherung
Binary Encoding of Relations
• A relation is a subset of the product of two sets Thus, a relation is nothing but a set
• Example: var v: {0..3}, w:{0..7};var v0, v1, w0, w1, w2: boolean;“divides”-Relation:
v divides w iff v=1, or v=2 and w even,or v=3 and w in {0,3,6}
boolean formula:
0 1 2 3 4 5 6 7
0 - - - - - - - -
1 + + + + + + + +
2 + - + - + - + -
3 + - - + - - + -
Folie 14H. Schlingloff, Software-Qualitätssicherung
The Influence of Variable Ordering
Folie 15H. Schlingloff, Software-Qualitätssicherung
Boolean Quantification
•Substitution by constants is trivial
•Boolean quantification:
• ! This works for arbitrary finite domains !
Folie 16H. Schlingloff, Software-Qualitätssicherung
Bounded Model Checking
• State s is reachable from s0 iff it is reachable in 0 steps: s=s0, or
it is reachable in 1 step: R(s0,s), or
it is reachable in 2 steps: s1(R(s0,s1) R(s1,s)), or it is reachable in 3 steps:
s1s2(R(s0,s1) R(s1,s2) R(s2,s)), or ..., or it is reachable in n steps, where n is the diameter
of the model
• Idea: Check each of these formulas sequentially
Folie 17H. Schlingloff, Software-Qualitätssicherung
Transitive Closure
•Each finite (transition) relation can be represented as a BDD
•The transitive closure of a relation R is defined recursively by
•Thus, transitive closure be calculated by an iteration on BDDs
Folie 18H. Schlingloff, Software-Qualitätssicherung
Reachability
•State s is reachable iff s0R*s, where s0S0 is an initial state and R is the transition relation
•Reachability is one of the most important properties in verification most safety properties can be reduced to it in a search algorithm, is the goal reachable?
•Can be arbitrarily hard for infinite state systems undecidable
•Can be efficiently calculated with BDDs