- 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
+ - 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
===============================================================================
repositories / tt1516.git / commitdiff