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
  52         - completed trace: observe sequence and end
  53         - trace: observe sequence
  54
  55 MBT with LTS 2
  56 ===============================================================================
  57
  58 MBT with LTS 3
  59 ===============================================================================
  60
  61 MBT with LTS 4
  62 ===============================================================================
  63
  64
  65 MBT with GAST
  66 ===============================================================================
  67 Functional, black box, cycle detection, automatic generation, quickcheck,
  68 quantification
  69 - Property
  70 - Model
  71
  72 MBT with SpecExplorer
  73 ===============================================================================