SVVAT Approach to Software Design and Testing, Study notes of Health sciences

Download SVVAT Approach to Software Design and Testing and more Study notes Health sciences in PDF only on Docsity! software design and testing the SVVAT approach sarfraz khurshid khurshid@ece.utexas.edu http://svvat.ece.utexas.edu EDGE lecture SVVAT launch 3/9/6 2 software verification validation and testing group* doctoral students • daryl shannon • danhua shao • engin uzuncaova masters/doctoral students • daniel garcia • khalid ghori • muhammad zubair malik • chen su • mohammad younas graduated students • yuk lai suen (masters, microsoft) • ivan garcia (masters, intel) *funded in part by NSF SoD #0438967 5 our approach constraint-based systematic analysis is inspired by traditional model checking performs bounded exhaustive analysis exploits “small scope hypothesis” focuses on data intensive properties, e.g., structural constraints applies to designs (viz jackson’s alloy) and implementations provides new algorithms for solving structural constraints • korat • abstract symbolic execution • translation to netlists (joint work with aziz and zaraket) • several orders of magnitude faster than alloy analyzer enables repair of corrupt program states may even enable repair of buggy programs!? 6 outline constraint-based test generation our other projects • architecture and design • implementation 7 software testing most commonly used technique for validating software quality expensive and ineffective as practiced at present • creating test suite is heavily labor intensive • especially hard for structurally complex data 10 what’s done in practice manual test selection construction sequences • t = new TreeSet().add(1).add(2).add(3); support from tools, such as JUnit • automate test execution and error reporting test generation is still a problem • very time consuming • poor test suites 11 why not generate automatically? generate at representation level or abstract level? generate a few or many or all? representation level may be okay for generating very few # valid / # total → 0 abstract level (using construction sequences) okay for a few need large number of sequences e.g., red-black: 10 nodes; 10! sequences; 240 trees hard to avoid equivalent tests may need “deletions” during construction need full implementation assume constructors work 12 use more sophisticated techniques? from constraints (e.g., EFFIGY, TESTGEN, INKA) • tools typically handle only primitive types from grammars (e.g., DGL, lava) • mainly syntactic, not semantically rich • can’t easily capture complex constraints how to generate a binary search tree? how to generate all binary search trees with n nodes? 15 challenges how to generate instances? how to abstract/concretize? how to eliminate equivalent tests? constraint all small instances solve tests concretize 16 outline constraint-based test generation • example • framework • experiments our other projects 17 postcondition: isTree() && isOrdered() && “removes only i” binary search tree class BinarySearchTree { Node root; int size; static class Node { int info; Node left, right; } } void remove(int i) { … } precondition: isTree() && isOrdered() 20 framework overview notation • constraints in first-order logic + transitive closure • succinct path expressions, e.g., root.*(left + right) scheme • phase 1 • generate “all” test inputs from input constraint • systematic exploration of input space • phase 2 • execute code for each input • check correctness • abstract domain (postconditions as test oracles) 21 TestEra [ASE 2001, J-ASE 2004] oracle run code a2j j2a non-isom instances abstract output counter example N Y Java output Java input abstract input ok? scope input constraint constraint solver constraints jar Java driver TestEra 22 binary search tree constraints precondition boolean isTree() { # root.*(left + right) = size // consistency of size all n: root.*(left + right) { n !in n.^(left + right) // no directed cycles sole n.~(left + right) // at most one parent no n.left & n.right } } // left and right child not the same node boolean isOrdered() { // binary search all n: root.*(left + right) { all nl: n.left.*(left + right) { n.info > nl.info } all nr: n.right.*(left + right) { n.info < nr.info } } } postcondition root.*(left + right).info = root`.*(left` + right`).info` - i 25 abstract instance BinarySearchTree = { BST0 } Node = { N0, N1, N2 } int = { 1, 2, 3 } root = { (BST0, N0) } size = { (BST0, 3) } info = { (N0, 2), (N1, 1), (N2, 3) } left = { (N0, N1) } right = { (N0, N2) } N0: 2 N1: 1 N2: 3 left BST0: 3 root right 26 concretization (algorithm) InputsAndMaps a2j(Instance a) { Map mapAJ, mapJA; // for each atom create a corresponding Java object foreach (sig in sigs(a)) foreach (atom in sig) { SigClass obj = new SigClass(); mapAJ.put(atom, obj); mapJA.put(obj, atom); } // establish relationships between created Java objects foreach (rel in relations(a)) foreach (<x, y> in rel) setField(mapAJ.get(x), rel, mapAJ.get(y)); // set inputs Object[] inputs = ...; result = (inputs, mapAJ, mapJA); } 27 concretization (illustration) translate abstract instance to Java BinarySearchTree = { BST0 } Node = { N0, N1, N2 } int = { 1, 2, 3 } root = { (BST0, N0) } size = { (BST0, 3) } info = { (N0, 2), (N1, 1), (N2, 3) } left = { (N0, N1) } right = { (N0, N2) } N0: 2 N1: 1 N2: 3 left BST0 root : 3 right 30 relations root ⊆ BinarySearchTree × Node × State size ⊆ BinarySearchTree × int × State info ⊆ Node × int × State left, right ⊆ Node × Node × State state (mutation) etc. [OOPSLA 2002] how to model mutation in a first-order relational setting? • associate a distinct graph with each state sets BinarySearchTree Node int State = { Pre, Post } postcondition: only “i” removed root.*(left + right).info = root`.*(left` + right`).info` - i (root.Post).*(left.Post + right.Post).(info.Post) = (root.Pre).*(left.Pre + right.Pre).(info.Pre) - i 31 summary of translations between Java objects and abstract instances • concretization • translates data from abstract instances to Java • used for test case generation • abstraction • translates data from Java to abstract instances • used for correctness checking users can define actual abstractions fully automatic translation for usual embedding 32 enabling technology relational formula relational instance scope translate formula mapping translate instance boolean formula SAT solver boolean instance Alloy Analyzer 35 nonisomorphism (example) N0: 2 N1: 1 N2: 3 left right N0: 2 N2: 1 N1: 3 left right N1: 2 N0: 1 N2: 3 left right N2: 2 N0: 1 N1: 3 left right N1: 2 N2: 1 N0: 3 left right N2: 2 N1: 1 N0: 3 left right 36 nonisomorphism (BinarySearchTree) order Node as [N0, N1, N2] define traversal to visit nodes in pre-order • visit node, then left, then right fun BinarySearchTree::BreakSymmetries { this.root in OrdFirst(Node) all n: this.root.*(left + right) { some n.left => n.left = OrdNext(n) some n.right && no n.left => n.right = OrdNext(n) some n.right && some n.left => n.right in OrdNext(n.left.*(left + right)) } } left right N0: 2 N1: 1 N2: 3 38 nonisomorphism (method inputs) consider method m(T1 f1, ..., Tn fn) • make a dummy class class Input_m { T1 f1; ...; Tn fn; } where class invariant of Input_m is pre-condition of m • isomorphism among inputs is defined as isomorphism among structures of class 41 SAT performance (mChaff) state space time (sec) structures* generated sizebenchmark 2119 2215 32 512 1716 24310 7 9 java.util.HashSet 2263 2407 111 742 35 122 7 9 java.util.TreeMap 2191 2362 1 304 877 115975 7 10 java.util.LinkedList 2186 2292 7 618 429 4862 7 9 BinarySearchTree 272 2110 6 1172 13139 1005075 6 8 HeapArray * Sloane’s online encyclopedia of integer sequences 42 evaluation of “small scope hypothesis” many bugs can be found by checking exhaustively on small inputs seems to hold for abstract models evaluate for code • measure branch/statement coverage • measure mutant killing rate • mutant: syntactic modification of original program 44 testing on all small inputs [MIT-TR 2003]* Binary Search Tree 0 20 40 60 80 100 0 1 2 3 4 5 6 7 scope co ve ra ge /r at e (% ) statement branch mutant killing *experiments performed using the Korat and Ferastrau frameworks 47 an intentional name root servicecity washington building whitehouse wing west room oval-office camera data-type picture resolution 640 x 480 accessability public source: Adjie-Winoto et al, SOSP’99 48 lookup(query, database) = {R0} intentional names adv0 NE-43 building service camera adv1 printerNE-43 building service ; add building service NE-43 camera printer database R0 R1 , lookup query NE-43 service camera building 49 published wildcard claim source: Adjie-Winoto et al, SOSP’99 a0 v0 qr Lookup-Name(db, qr) = {} Lookup-Name(db, q) = {R0} db a0 v0 a1 v1 R0 a0 v0 a1 * q (counterexample) 56 summary systematic testing • feasible for real systems • can identify subtle bugs that went unnoticed for years • ability to characterize test purposes is key to usability effort • few hours to write constraints/manual translations technical points • SAT even though not optimized, is practical for enumeration • symmetry breaking plays a crucial role 57 outline constraint-based test generation • example • framework • experiments our other projects • architecture and design • implementation 58 architecture and design core methodologies • constraint-based architecture analysis [uzuncaova] • lightweight modeling and analysis of distributed systems [younas & shakil] optimized analyses • incremental analyses for software modeling tools [shannon, LDTA’06] • compiler optimizations for declarative formulas [SAT’05] • sequential encoding for relational analysis [joint work with aziz & zaraket]