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
===============================================================================
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
===============================================================================
Functional, black box, cycle detection, automatic generation, quickcheck,
quantification
- Property
- Model

MBT with SpecExplorer
===============================================================================