recap_mbt.txt

   1 FSM-based testing
   2 ===============================================================================
   3 FSM: States, transitions, inputs, outputs
   4 (S, s0, I, O, delta, lambda)
   5 (States, initial, inputs, outputs, transition function, output function)
   6
   7 - Deterministic, complete, connected, reduced
   8 - Tests length k only prove models with k extra states(k-complete)
   9 - With resets
  10 - W method
  11         - we test a state by testing that after reaching it the input/output is
  12           good
  13 - Transition tour, one loop all transitions
  14 - Synchonizing, get always to a fixed state
  15
  16 - Compare with LTS:
  17         - has to be deterministic and complete
  18         - Only i/o alternation
  19         - not compositional
  20         - more intuitive
  21         - older theory
  22
  23 MBT with LTS 1
  24 ===============================================================================
  25 Terminology:
  26 s0->s1 transition
  27 s0=>s1 transition composition
  28 s0=>   executable sequence
  29 s0=/>  non-executable sequence
  30
  31 trace: sequence of possible
  32 reachable states: s after omega
  33 - s: state
  34 - omega: trace
  35
  36 Representation
  37 - 4-tuple: (S, L, T, s0) States, Labels, Transition function, initial state
  38 - tree/graph
  39 - language/behaviour expression:
  40         - :=   : assignment
  41         - stop : termination
  42         - ;    : sequence
  43         - label: transition input
  44         - []   : choice
  45         - |||  : parallel
  46         - |[G]|: parallel synchronized on elements in G
  47 - equivalence from strong to weak
  48         - isomorphism: need to observe tau
  49         - bisimulation: infinite undo, copy and repeat
  50         - failure trace: test with another lts and continue on failure
  51         - testing trace: test LTS with another LTS, refusal
  52         - completed trace: observe sequence and end
  53         - trace: observe sequence
  54
  55 MBT with LTS 2
  56 ===============================================================================
  57 i imp s: implementation i implements specification s
  58 - trace preorder:
  59         i <=_tr s: all traces(i) subset of traces(s)
  60 - testing preorder:
  61         i <=_te s: test with another lts, refusal
  62 - i ioco s:
  63         - for all straces s: x after omega in i subset of x after omega s
  64         - intuitively:
  65                 - if i produces x after omega then s can produce x after omega
  66                 - if i can't produce output after omega then s can't produce output
  67                   after omega
  68
  69 MBT with LTS 3
  70 ===============================================================================
  71 - testcase is a lts
  72         - ! is input, ? output. Other way around
  73         - L and theta, theta is quiescence
  74         - tree, finite deterministic
  75         - complete
  76 - generation: recursively do either:
  77         - end test case
  78         - supply !a
  79         - observe all outputs
  80 - execution: all parallel possible executions should pass
  81 - soundness: i ioco s -> i passes t
  82         - disprove: find a failing test if ioco
  83 - exhaustiveness: i not ioco s -> there is a testcase for which i fails t
  84         - disprove: prove there all testcases pass
  85
  86 MBT with LTS 4
  87 ===============================================================================
  88 - test selection by: user, test tool, random
  89 - compositionality: if systems input enabled ioco is preserved in composition.
  90   otherwise not
  91
  92 MBT with GAST
  93 ===============================================================================
  94 Functional, black box, cycle detection, automatic generation, quickcheck,
  95 quantification
  96 - Property
  97 - Model
  98
  99 MBT with SpecExplorer
 100 ===============================================================================