From 57b4951c046f1c71860a263166c0fb8bf16d1b24 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 21 Jan 2016 15:53:12 +0100 Subject: [PATCH] mbt done' git pus --- recap_mbt.txt | 31 +++++++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/recap_mbt.txt b/recap_mbt.txt index b56d7c6..1a6a0a7 100644 --- a/recap_mbt.txt +++ b/recap_mbt.txt @@ -48,19 +48,46 @@ Representation - 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 =============================================================================== -- 2.20.1