update

[tt1516.git] / recap_mbt.txt

diff --git a/recap_mbt.txt b/recap_mbt.txt
index ded951e..1a6a0a7 100644 (file)
--- a/recap_mbt.txt
+++ b/recap_mbt.txt
@@ -22,16 +22,72 @@ FSM: States, transitions, inputs, outputs
 
 MBT with LTS 1
 ===============================================================================
+Terminology:
+s0->s1 transition
+s0=>s1 transition composition
+s0=>   executable sequence
+s0=/>  non-executable sequence
+
+trace: sequence of possible
+reachable states: s after omega
+- s: state
+- omega: trace
+
+Representation
+- 4-tuple: (S, L, T, s0) States, Labels, Transition function, initial state
+- tree/graph
+- language/behaviour expression:
+       - :=   : assignment
+       - stop : termination
+       - ;    : sequence
+       - label: transition input
+       - []   : choice
+       - |||  : parallel
+       - |[G]|: parallel synchronized on elements in G
+- equivalence from strong to weak
+       - isomorphism: need to observe tau
+       - bisimulation: infinite undo, copy and repeat
+       - failure trace: test with another lts and continue on failure
+       - testing trace: test LTS with another LTS, refusal
+       - completed trace: observe sequence and end
+       - trace: observe sequence
 
 MBT with LTS 2
 ===============================================================================
+i imp s: implementation i implements specification s
+- trace preorder:
+       i <=_tr s: all traces(i) subset of traces(s)
+- testing preorder:
+       i <=_te s: test with another lts, refusal
+- i ioco s:
+       - for all straces s: x after omega in i subset of x after omega s
+       - intuitively:
+               - if i produces x after omega then s can produce x after omega
+               - if i can't produce output after omega then s can't produce output
+                 after omega
 
 MBT with LTS 3
 ===============================================================================
+- testcase is a lts
+       - ! is input, ? output. Other way around
+       - L and theta, theta is quiescence
+       - tree, finite deterministic
+       - complete
+- generation: recursively do either:
+       - end test case
+       - supply !a
+       - observe all outputs
+- execution: all parallel possible executions should pass
+- soundness: i ioco s -> i passes t
+       - disprove: find a failing test if ioco
+- exhaustiveness: i not ioco s -> there is a testcase for which i fails t
+       - disprove: prove there all testcases pass
 
 MBT with LTS 4
 ===============================================================================
-
+- test selection by: user, test tool, random
+- compositionality: if systems input enabled ioco is preserved in composition.
+  otherwise not
 
 MBT with GAST
 ===============================================================================