update

[tt1516.git] / recap_mbt.txt

diff --git a/recap_mbt.txt b/recap_mbt.txt
new file mode 100644 (file)
index 0000000..ded951e
--- /dev/null
+++ b/recap_mbt.txt
@@ -0,0 +1,44 @@
+FSM-based testing
+===============================================================================
+FSM: States, transitions, inputs, outputs
+(S, s0, I, O, delta, lambda)
+(States, initial, inputs, outputs, transition function, output function)
+
+- Deterministic, complete, connected, reduced
+- Tests length k only prove models with k extra states(k-complete)
+- With resets
+- W method
+       - we test a state by testing that after reaching it the input/output is
+         good
+- Transition tour, one loop all transitions
+- Synchonizing, get always to a fixed state
+
+- Compare with LTS:
+       - has to be deterministic and complete
+       - Only i/o alternation
+       - not compositional
+       - more intuitive
+       - older theory
+
+MBT with LTS 1
+===============================================================================
+
+MBT with LTS 2
+===============================================================================
+
+MBT with LTS 3
+===============================================================================
+
+MBT with LTS 4
+===============================================================================
+
+
+MBT with GAST
+===============================================================================
+Functional, black box, cycle detection, automatic generation, quickcheck,
+quantification
+- Property
+- Model
+
+MBT with SpecExplorer
+===============================================================================