Report

Lecture 6 Model-based Testing and Automated Test Case Generation Automated Test-Case Generation (TCG) • By now we have seen that manual construction of test cases is a difficult, time-consuming and error-prone activity that requires expertise. • Automated Test-Case Generation (TCG) has been the “holy grail” of testing for some time. • Is this even possible? If so, how? • Black/white-box testing • Want algorithms which generate test cases (preferably with a known level of coverage) Constraint Solving • A constraint is a logical formula with one or more free variables • Examples: x >= 0, x+1 > y, x2 = 2.0, etc. • A constraint solver is an algorithm which finds values for the free variables, which make a formula true, aka. solutions • Examples: – x=1 I= x >= 0 ( I= is the satisfaction symbol ) – x=1.41421356 I= x2 = 2.0 • Exist many different kinds of constraint solvers Specification-based Black-box Testing 1. System requirement (Sys-Req) 2. System under Test (SUT ) 3. Test verdict pass/fail (Oracle step) Sys-Req Test case pass/fail Output TCG SUT Oracle Constraint solver Language runtime Constraint checker Example: ATCG for numerical code Newton’s Square root algorithm Postcondition Ι y*y – x Ι ≤ ε precondition x ≥ 0.0 x=4.0 TCG Input Constraint solver x=4.0 satisfies x ≥ 0.0 y=2.0 SUT Newton Code Output Oracle Constraint checker Verdict x=4.0, y=2.0 satisfies Ι y*y – x Ι ≤ ε TCG for MBT of Embedded Systems • We can make a simple model of an embedded system as a deterministic Kripke structure (or Moore machine) • M = ( Q, Σ, q0, δ, λ ) • Where – q0 Q, - initial state – δ : Q x Σ Q - state transition function – λ: Q Bn - n-bit output function Example: 2-bit shift register • Q = A, B, C, D, Σ = 0,1, q0=A 1 A, λ(A) =00 0 1 0 0 1 B, λ(B) =10 C, λ(C) =01 0 D, λ(D) =11 1 Another Representation • Q = A, B, C, D, Σ = 0,1, q0=A 1 !Bit1 & !Bit2 0 1 0 0 1 Bit1 & !Bit2 !Bit1 & Bit2 0 Bit1 & Bit2 1 2-Bit Shift Reg in nuSMV format MODULE main VAR Bit1 : boolean; -- Boolean var Bit2 : boolean; input : boolean; state : {A, B, C, D}; -- scalar var variable ASSIGN init(state) := A; init(Bit1) := 0; init(Bit2) := 0; -- var “input” is uninitialised! next(state) := case state = A & input = 1 state = B & input = 0 state = B & input = 1 state = C & input = 0 state = C & input = 1 state = D & input = 0 TRUE : state; -- why? esac; next(Bit1) := case ?? next(Bit2) := case ?? : : : : : : B; C; D; A; B; C; esac; esac; Propositional Linear Temporal Logic PLTL in nuSMV syntax • • • • • • • • • • • • Simple temporal logic to express automaton requirements Requirements are statements about all possible simulations Boolean variables A, B, …, X, Y, .. MyVar, etc. Boolean operators !ϕ, (ϕ & φ), (ϕ ϕ) , (ϕ -> ϕ) ,… LTL operators Fϕ (sometime in the future ϕ) Gϕ (always in the future ϕ) ϕ U φ (φ holds until ϕ holds) Xϕ (next step ϕ holds) Write Xnϕ for X X … Xϕ (n times) Examples Today is Wednesday Wednesday Tomorrow is Wednesday X Wednesday (A) Thursday (always) immediately follows (a) Wednesday G( Wednesday -> Thursday ) (A) Saturday (always) follows (a) Wednesday G( Wednesday -> F( Saturday ) ) Yesterday was (a) Wednesday G( Wednesday -> X Thursday) & Thursday • Exercise: define the sequence of days precisely, i.e. just one solution • Question: are there any English statements you can’t make in LTL? • Question: what use cases can you express in LTL? Useful Logical Identities for LTL • Boolean identities !!φ φ, !(ϕ φ) (!ϕ & !φ) , (ϕ -> φ) (!ϕ φ) etc. • LTL identities !G(!ϕ ) F(ϕ) !X(ϕ) X(!ϕ) G(φ & ϕ) G(φ)& G(ϕ) G(φ) φ & X G(φ) • Exercise: using these identities, prove: !F(!φ) G(φ) F(φ ϕ) F(φ) F(ϕ) F(φ) φ X F(φ) • Remark TCG usually involves negating formulas, so its useful to understand what a negation means Specifications in nuSMV files LTLSPEC G( Bit1 <-> X Bit2 ) –- the value of Bit1 now always equals the -- value of Bit2 in the next time step -- This is obviously TRUE! G( –the --- Bit1 <-> X Bit1 ) the value of Bit1 now always equals value of Bit2 in the next time step This is obviously FALSE! Model Checking • nuSMV is a temporal logic model checker • A model checker is a tool which takes as input • • • • – An automaton model M – A temporal logic formula φ If φ is a true statement about all possible behaviors of M then the model checker confirms it (proof) If φ is a false statement about M the model checker constructs a counterexample (a simulation sequence) A counterexample to φ satisfies !φ A simulation sequence can be executed as a test case nuSMV Output Example -- specification G( Bit1 <-> X Bit2 ) -- is true -- specification G( Bit1 <-> X Bit1 ) -- is false -- as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 1.1 <state = A Bit1 = false Bit2 = false -> Input: 1.2 <input = 1 -> State 1.2 <state = A Bit1 = true Bit2 = false Automated White-box TCG • We can use a model checker to generate counterexamples to formulas (i.e. test cases) with specific structural properties. • This is done by inspecting the graph structure of the automaton • i.e. white/glass box testing • “Most” use of model checkers concerns this. Test Requirements/ Trap Properties • Recall a test requirement is a requirement that can be satisfied by one or more test cases • Basic idea is to capture each test requirement as an LTL formula known as a “trap property” Example Suppose the test requirement is “cover state D” Trap property is G!( Bit1 & Bit2 ) This formula is False and any counterexample must be a path that goes through state D. Case Study: Car Controller !accelerate accelerate Velocity = stop Velocity = slow brake accelerate brake Basic idea (incomplete) Velocity = fast !accelerate Module main Var accelerate: boolean; brake: boolean; velocity: {stop, slow, fast} ASSIGN init(velocity) := stop next(velocity := case accelerate & !brake & velocity = stop : slow; accelerate & !brake & velocity = slow : fast; !accelerate & !brake & velocity = fast : slow; !accelerate & !brake & velocity = slow: stop; Brake: stop; TRUE: velocity; esac; Trap properties for Structural Coverage Models • Let us use nuSMV to automatically construct test suites that satisfy the different structural coverage models introduced in Lecture 2. • Examples: – Node coverage NC – Edge coverage EC – Condition coverage PC • How to interpret these concepts? Node Coverage for CC • • • • • • • Want a path that visits each node Simple approach: 1 trap property per node General form: G(!“unique_state_property”) Counterexamples satisfy: F(“unique_state_property” ) Examples: G(!velocity = stop) G(!velocity = slow) G(!velocity = fast) • Clearly this will give redundant test cases, but method is still linear in state-space size. Edge coverage for CC • Want to be sure we traverse each edge between any pair of nodes α φ β • General form G( α & ϕ -> X !β ) • Counterexample satisfies F(α & ϕ & X β ) • Example (5 more cases): G(velocity=stop & accelerate -> X velocity=slow) • Exercise: define the remaining 5 trap formulas Condition Coverage for CC • For each transition, and each Boolean guard v there exist two test cases for the transition: (1) guard is true. (2) guard is false α G!(α & v) -> X(!β) G!(α & !v) -> X(!β) β Boolean v; Requirements-based TCG • Can we also perform requirements-based test case generation? • Want to test the requirements are fulfilled rather than explore structure of the code. • Can look at negation of a requirement Car Controller LTL requirements 1. Whenever the brake is activated, car has to stop G(brake -> X velocity=stop) 2. When accelerating and not braking, velocity has to increase gradually G(!brake& accelerate&velocity=stop -> X velocity=slow ) G(!brake& accelerate&velocity=slow -> X velocity=fast ) 3. When not accelerating and not braking, velocity has to decrease gradually G(!brake& !accelerate&velocity=fast -> X velocity=slow) G(!brake& accelerate&velocity=slow -> X velocity=stop) Safety Requirements • A safety requirement describes a behavior that may not occur on any path. • “Something bad may not happen” • To verify, all execution paths must be checked exhaustively • Safety properties usually have the form G!φ where φ is the “bad thing” • Counterexamples (test cases) are finite Liveness Requirements • A liveness requirement describes a behavior that must hold on all execution paths • “Something good eventually happens” • Safety does not imply liveness • Liveness does not imply safety • Liveness properties may have the form F(φ) or G(ϕ -> Xnφ ) or G(ϕ -> Fφ ) where φ describes the “good” thing and ϕ is some precondition needed for it to occur. • Counterexamples may be finite or infinite (why?) Infinite Counterexamples • nuSMV describes infinite counterexamples as a “loop and handle” • a,b,c,d,(x,y,z)ω or handle(loop) ω • a, …, d, x, …, z are the individual states • We can generate these sequences, but can we execute them? • Are they test cases at all? • We call a liveness requirement finite if all counterexamples are finite • Use cases are examples of finite liveness requirements TCG for Finite Liveness Requirements • A common form of liveness requirement is G( φ -> Xn ϕ ) (1) • Negating (1) and rewriting gives F( φ & Xn (!ϕ ) ) (2) • Every counterexample to (2) is a solution to (1) i.e. an intended behavior. • We can ask nuSMV for these intended behavior, and compare them against the actual behavior. • Edit the sequence to delete all internal and output variables • Agreement = pass, disagreement = fail Car Controller Examples (1)F(brake & X !velocity=stop) (2) F(!brake & accelerate & velocity=stop -> X velocity=slow) Conclusions • TCG is certainly possible using various existing algorithms. • Generally requirements MBT is trickier than structural MBT using this approach. • There are other approaches to requirements testing. See next lecture.