Mousavi_day1_p2_4.pdf

Model-Based Testing: Testing from Finite State Machines Mohammad Mousavi University of Leicester, UK

IPM Summer School 2017

Mousavi

FSM-Based Testing

IPM 2017

1 / 64

Finite State Machines

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

2 / 64

Finite State Machines

Context: FSM-Based Conformance Testing Problem Given an FSM spec M and a black-box implementation I, does I conform to M, i.e., does I implement the same output and transfer function as M?

Mousavi

FSM-Based Testing

IPM 2017

3 / 64

Finite State Machines

Context: Testing Finite-State Machines

Problem Given an FSM spec M and a black-box implementation I, does I conform to M, i.e., does I implement the same output and transfer function as M? Solution: Complete Test Suite For each state s and input i in the spec: 1

bring the FSM to s,

2

apply i and observe the expected output o, and

3

check the target state s 0

Mousavi

FSM-Based Testing

IPM 2017

4 / 64

Finite State Machines

Context: Testing Finite-State Machines

Problem Given an FSM spec M and a black-box implementation I, does I conform to M, i.e., does I implement the same output and transfer function as M? Solution: Complete Test Suite For each state s and input i in the spec: 1

bring the FSM to s, (final state identification)

2

apply i and observe the expected output o, and

3

check the target state s 0 (initial state identification / verification )

Mousavi

FSM-Based Testing

IPM 2017

4 / 64

Finite State Machines

Notations I a /0

 : empty sequence

s1

next : target state after a sequence of inputs (naturally generalized to sets of states:next (S , x )) by definition:next (s , ) = s

b /1 a /1

s2

b /0

b /1 s3

a /0

Mousavi

FSM-Based Testing

IPM 2017

5 / 64

Finite State Machines

Notations I a /0

 : empty sequence

s1

next : target state after a sequence of inputs (naturally generalized to sets of states:next (S , x )) by definition:next (s , ) = s next (s1 , bba ) = next (next (s1 , b ), ba ) = next (s2 , ba ) = next (next (s2 , b ), a ) = next (s3 , a ) = s3

Mousavi

FSM-Based Testing

b /1 a /1

s2

b /0

b /1 s3

a /0

IPM 2017

5 / 64

Finite State Machines

Notations II a /0 output : action sequence after a sequence of inputs (generalized to sets of states:output (S , x )) assumption: output (s , ) = 

s1

b /1 a /1

s2

b /0

b /1 s3

a /0

Mousavi

FSM-Based Testing

IPM 2017

6 / 64

Finite State Machines

Notations II a /0 output : action sequence after a sequence of inputs (generalized to sets of states:output (S , x )) assumption: output (s , ) =  output (s1 , bba ) = output (s1 , b ) output (next (s1 , b ), ba ) = 1 output (s2 , ba ) = 1 output (s2 , b ) output (next (s2 , b ), a ) = 1 1 output (s3 , a ) =110

Mousavi

FSM-Based Testing

s1

b /1 a /1

s2

b /0

b /1 s3

a /0

IPM 2017

6 / 64

Final State Identification

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

7 / 64

Final State Identification

Final State Identification

Problem: Given an FSM, we do not know which state it is in Solution: Perform a test (homing sequence), observe output sequence and determine the final state of the machine An FSM is reduced when each two different states can show different output on at least one sequence of inputs

Mousavi

FSM-Based Testing

IPM 2017

8 / 64

Final State Identification

Final State Identification

Problem: Given an FSM, we do not know which state it is in Solution: Perform a test (homing sequence), observe output sequence and determine the final state of the machine An FSM is reduced when each two different states can show different output on at least one sequence of inputs Reduced FSM always has a homing sequence FSM that is not reduced may not have a homing sequence

Mousavi

FSM-Based Testing

IPM 2017

8 / 64

Final State Identification

Determining a homing sequence

Algorithm: (for reduced machine) 1

let x =  ,

Mousavi

FSM-Based Testing

IPM 2017

9 / 64

Final State Identification

Determining a homing sequence

Algorithm: (for reduced machine) 1 2

let x =  , while there exists a set B of states such that |next (B , x )| > 1 and for each two s , s 0 ∈ B, output (s , x ) = output (s 0 , x ), 1 take two states s , s 0 ∈ next (B , x ) (with s , s 0 ) 2

3 4

find a sequence y, separating s and s 0 i.e., output (s , y ) , output (s 0 , y ) x := x y partition B into the subsets with the same output after x

Mousavi

FSM-Based Testing

IPM 2017

9 / 64

Final State Identification

Example b /0 a /0

s1

b /1

s2

b /1

s3

a /0

a /1 Partition of S: {{s1 , s2 , s3 }} Take B = {s1 , s2 , s3 }, next (B , ) = B. Take: s1 and s2

Mousavi

FSM-Based Testing

IPM 2017

10 / 64

Final State Identification

Example b /0 a /0

s1

b /1

s2

b /1

s3

a /0

a /1 Partition of S: {{s1 , s2 , s3 }} Take B = {s1 , s2 , s3 }, next (B , ) = B. Take: s1 and s2 Separating sequence: a Output sequences: output (s1 , a ) = output (s3 , a ) = 0 and output (s2 , a ) = 1 New partition: {{s1 , s3 }, {s2 }}

Mousavi

FSM-Based Testing

IPM 2017

10 / 64

Final State Identification

Example b /0 a /0

s1

b /1

s2

b /1

s3

a /0

a /1 Partition of S: {{s1 , s3 }, {s2 }} Take B = {s1 , s3 }, next (B , a ) = B. Take: s1 and s3 . Separating sequence: b Output sequences: output (s1 , b ) = 1 and output (s3 , b ) = 0 New partition: {{s1 }, {s3 }, {s2 }}

Mousavi

FSM-Based Testing

IPM 2017

11 / 64

Final State Identification

Example

b /0 a /0

s1

b /1

s2

b /1

s3

a /0

a /1 Partition of S: {{s1 }, {s3 }, {s2 }} Homing sequence: a b

Mousavi

FSM-Based Testing

IPM 2017

12 / 64

Initial State Identification

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

13 / 64

Initial State Identification

State identification

Problem: Given an FSM, can we determine the initial state of the FSM? An input sequence that solves this problem is a distinguishing sequence.

Mousavi

FSM-Based Testing

IPM 2017

14 / 64

Initial State Identification

Distinguishing sequence

A distinguishing sequence for a machine is a rooted tree T with exactly |S | leaves internal nodes are labeled with input symbols leaves are labeled with states edges are labeled with output symbols such that for each node, the labels of the outgoing edges are different for each leaf, if x and y are input and output sequence on path from root to the leaf and the leaf is labeled by state s, then output (s , x ) = y

Mousavi

FSM-Based Testing

IPM 2017

15 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0

s2

a /0 b /0

a /1 s5

a /1 b /0

Mousavi

s3

s4

a /0 b /0

FSM-Based Testing

IPM 2017

16 / 64

Initial State Identification

Example a

b /0 a /1 b /0 s6

s1

b /0

a

1

b

0

Mousavi

a

0

s3

s4

0

b

a /1

a /1 b /0

b

1

s2

a /0 b /0 s5

0

a

a /0

1

a /0 b /0

a s1

FSM-Based Testing

1

s6

1

0

b

0

0

s5

a s2

1

0 s4

0 s3

IPM 2017

16 / 64

Initial State Identification

Non-existence of distinguishing sequence

b /1 a /0

s1

a /0

s2

b /1

s3

a /1

b /0

distinguishing sequence cannot start with a because then s1 and s2 are not distinguishable since from both s1 is reached with output 0 distinguishing sequence cannot start with b because then s2 and s3 are not distinguishable since from both s2 is reached with output 1

Mousavi

FSM-Based Testing

IPM 2017

17 / 64

Initial State Identification

Existence of distinguishing sequence An input a is valid for a set C of states if it does not merge any two states s and s 0 from C without distinguishing them, i.e.,

∀s ,s 0 ∈C output (s , a ) , output (s 0 , a ) ∨ next (s , a ) , next (s 0 , a ) b /0 a /1 a /0 s1 b /0 a /0 b /0

s6

b /0

Input symbol b is not valid for set of states S

s2

a /1 s5

a /1 b /0

Mousavi

s3 s4

Input symbol a is valid for set of states S

a /0 b /0

FSM-Based Testing

IPM 2017

18 / 64

Initial State Identification

Algorithm 1 2

Start with partition π of S with only one block {S }. While there is a block B ∈ π with |B | > 1, 1 Take a valid input symbol a ∈ I for B such that two states s , s 0 ∈ B (s , s 0 ), output (s , a ) , output (s 0 , a ) or move to states in different blocks of π, 2 refine the partition π by replacing block B by a set of new blocks, where two states in B are assigned to the same block in the new partition iff they produce the same output on a and move to the same block in π.

Property An FSM has a distinguishing sequence iff the final partition contains singleton sets.

Mousavi

FSM-Based Testing

IPM 2017

19 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0 Initial partition π = {S } s2

a /0 b /0

Input symbol b is not valid a /1

s5

a /1 b /0 Mousavi

s3

s4

Input symbol a is valid New partition: π = {{s1 , s3 , s5 }, {s2 , s4 , s6 }}

a /0 b /0 FSM-Based Testing

IPM 2017

20 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0 Initial partition π = {{s1 , s3 , s5 }, {s2 , s4 , s6 }}

s2

a /0 b /0

a /1 s5

a /1 b /0 Mousavi

s3

s4

Input symbol b is valid for {s1 , s3 , s5 } New partition: π = {{s1 }, {s3 , s5 }, {s2 , s4 , s6 }}

a /0 b /0 FSM-Based Testing

IPM 2017

21 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0 Initial partition π = {{s1 }, {s3 , s5 }, {s2 , s4 , s6 }}

s2

a /0 b /0

a /1 s5

a /1 b /0 Mousavi

s3

s4

Input symbol a is valid for {s2 , s4 , s6 } New partition: π = {{s1 }, {s3 , s5 }, {s2 , s4 }, {s6 }}

a /0 b /0 FSM-Based Testing

IPM 2017

22 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0 Initial partition π = {{s1 }, {s3 , s5 }, {s2 , s4 }, {s6 }}

s2

a /0 b /0

a /1 s5

a /1 b /0 Mousavi

s3

s4

Input symbol b is valid for {s3 , s5 } New partition: π = {{s1 }, {s3 }, {s5 }, {s2 , s4 }, {s6 }}

a /0 b /0 FSM-Based Testing

IPM 2017

23 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0

Initial partition π = {{s1 }, {s3 }, {s5 }, {s2 , s4 }, {s6 }} Input symbol a is valid for {s2 , s4 }

s2

a /0 b /0

a /1 s5

a /1 b /0 Mousavi

s3

s4

New partition: π = {{s1 }, {s3 }, {s5 }, {s2 }, {s4 }, {s6 }} Thus FSM has a distinguishing sequence

a /0 b /0 FSM-Based Testing

IPM 2017

24 / 64

Initial State Identification

Example b /0 a /1 b /0 s6

s1

b /0

a /0 Initial partition π = {{s1 }, {s3 }, {s5 }, {s2 }, {s4 }, {s6 }}

s2

a /0 b /0

a /1 s5

a /1 b /0 Mousavi

Thus FSM has a distinguishing sequence

s3

s4

a /0 b /0 FSM-Based Testing

IPM 2017

25 / 64

Initial State Identification

Finite State Machines (recap)

states: abstractions of the past, transitions: reactions to input by producing output and moving to a new state state transition function next: S × I → S

rst/0 s0

output function output: S × I → O

t/1 rst/0 t/0 s1

Mousavi

FSM-Based Testing

IPM 2017

26 / 64

Initial State Identification

Finite State Machines (recap)

states: abstractions of the past, transitions: reactions to input by producing output and moving to a new state state transition function next: S × I → S

rst/0 s0

output function output: S × I → O next and output are generalized to sets of states and sequences of inputs.

t/1 rst/0 t/0 s1

Mousavi

FSM-Based Testing

IPM 2017

26 / 64

Initial State Identification

Finite State Machines (recap)

states: abstractions of the past, transitions: reactions to input by producing output and moving to a new state state transition function next: S × I → S

rst/0 s0

output function output: S × I → O next and output are generalized to sets of states and sequences of inputs. Assumption: FSM’s are reduced, deterministic and complete.

Mousavi

FSM-Based Testing

t/1 rst/0 t/0 s1

IPM 2017

26 / 64

Initial State Identification

Essential Notions

1

Reduced FSM: for all distinct s , s 0 ∈ S, there exists an x ∈ I∗ such that output (s , x ) , output (s 0 , x ). I.e., x separates s and s 0 .

2

Completeness: For each input a, and state s, there exists a s 0 such that next (s , a ) = s 0 .

3

Determinism: For each input a, and state s, there exists at most one s 0 such that next (s , a ) = s 0 .

Mousavi

FSM-Based Testing

IPM 2017

27 / 64

Initial State Identification

Equivalence

1

State equivalence: for s ∈ S and s 0 ∈ S 0 s ≈ s 0  ∀x ∈I∗ output (s , x ) = output (s 0 , x )

2

Machine equivalence M ≈ M 0  ∀s ∈S ∃s 0 ∈S 0 s ≈ s 0 ∧ ∀s 0 ∈S 0 ∃s ∈S s 0 ≈ s

Mousavi

FSM-Based Testing

IPM 2017

28 / 64

Conformance Testing

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

29 / 64

Conformance Testing

Five Fundamental Testing Problems

1

Determine the final state

√

homing sequence: a testcase to reveal the final state

Mousavi

FSM-Based Testing

IPM 2017

30 / 64

Conformance Testing

Five Fundamental Testing Problems

1

Determine the final state

√

homing sequence: a testcase to reveal the final state 2

State identification (identify the initial state)

√

adaptive distinguishing sequence

Mousavi

FSM-Based Testing

IPM 2017

30 / 64

Conformance Testing

Five Fundamental Testing Problems

1

Determine the final state

√

homing sequence: a testcase to reveal the final state 2

State identification (identify the initial state)

√

adaptive distinguishing sequence 3

Conformance testing (is blackbox A equivalent to the FSM?)

Mousavi

FSM-Based Testing

IPM 2017

30 / 64

Conformance Testing

Five Fundamental Testing Problems

1

Determine the final state

√

homing sequence: a testcase to reveal the final state 2

State identification (identify the initial state)

√

adaptive distinguishing sequence 3

Conformance testing (is blackbox A equivalent to the FSM?)

4

Machine identification (derive the FSM from a blackbox)

Mousavi

FSM-Based Testing

IPM 2017

30 / 64

Conformance Testing

Basic Idea

Specification: FSM A Implementation: A blackbox B, only input-output observable Problem: given the specification determine a testcase (a sequence of inputs) to determine whether A ≈ B (Also called: fault detection, machine testing)

Mousavi

FSM-Based Testing

IPM 2017

31 / 64

Conformance Testing

Basic Idea

Specification: FSM A Implementation: A blackbox B, only input-output observable Problem: given the specification determine a testcase (a sequence of inputs) to determine whether A ≈ B (Also called: fault detection, machine testing) Challenge: for each testcase t, B can always behave the same as A up to | t |

Mousavi

FSM-Based Testing

IPM 2017

31 / 64

Conformance Testing

Example a/0 s0

specification:

Mousavi

FSM-Based Testing

IPM 2017

32 / 64

Conformance Testing

Example a/0 s0

specification:

suppose that sequence a n is the testcase (the answer to the conformance testing problem)

Mousavi

FSM-Based Testing

IPM 2017

32 / 64

Conformance Testing

Example a/0 s0

specification:

suppose that sequence a n is the testcase (the answer to the conformance testing problem)

s0 a/0 n a/0 sn

for any n, some incorrect implementation may pass the test:

Mousavi

FSM-Based Testing

a/1 sn

IPM 2017

32 / 64

Conformance Testing

Simplifying Assumptions

rst/0

Assumptions on A strongly connected: (testcase long enough ⇒ each state visited) reduced: (equivalence: interesting / efficient on reduced FSMs)

Mousavi

FSM-Based Testing

s0 t/1 rst/0 t/0 s1

IPM 2017

33 / 64

Conformance Testing

Simplifying Assumptions Assumptions on A strongly connected: (testcase long enough ⇒ each state visited) reduced: (equivalence: interesting / efficient on reduced FSMs) A has the following transitions set (j )/0: a transition from each state

set(0)/0

rst/0

status/0

s0 t/1 set(0) set(1) rst/0 t/0 /0 /0

to state j, status /i: a self-loop indicating the current state

s1 status/1

set(1)/0

Last assumption: only for convenience; to be dropped later. Mousavi

FSM-Based Testing

IPM 2017

34 / 64

Conformance Testing

Simplifying Assumptions

Assumptions on B constant FSM (should not change; should be finite) at most | SA | states (an upper bound is needed; here, only transfer and output faults tested no new states due to faults)

Mousavi

FSM-Based Testing

IPM 2017

35 / 64

Conformance Testing

Fault Model

set(0)/0

rst/0

status/0

t/1

set(1) /0

status/0

set(0)/0

rst/0

set(1)/0

Specification

Mousavi

status/0 s0

t/1 set(0) set(1) status/1 rst/0 t/0 /0 /0

t/1 set(0) set(1) rst/0 t/1 /0 /0

s1

s1 status/1

rst/0 s0

s0 set(0) rst/0 t/0 /0

set(0)/0

s1

set(1)/0

Transfer Fault

FSM-Based Testing

status/1

set(1)/0

Output Fault

IPM 2017

36 / 64

Conformance Testing

Basic Algorithm

For each state s and input a in A: set the state to s, supply input a and check in B whether 1 output is output (s , a ) 2 the target is next (s , a )

, and .

N.B. all transitions are covered by the algorithm (a transition tour is taken).

Mousavi

FSM-Based Testing

IPM 2017

37 / 64

Conformance Testing

Basic Algorithm

For each state s and input a in A: set the state to s, using set (s ) supply input a and check in B whether 1 output is output (s , a ) (observe the output), and 2 the target is next (s , a ) (supply status and observe the output). N.B. all transitions are covered by the algorithm (a transition tour is taken).

Mousavi

FSM-Based Testing

IPM 2017

37 / 64

Conformance Testing

Example testcase: set(0), status, status, status, set(0)/0

rst/0

status, status, rst, status, t, status, set(1), status, t, status, set(1), rst, status, set(1), set(0), status status/0

s0 t/1 set(0) set(1) rst/0 t/0 /0 /0 s1 status/1

set(1)/0

Specification 0,0, 0,0, 0, 0, 1, 1, 0,1, 1,1, 0, 0, 0,0,0, 0,0,0

Mousavi

FSM-Based Testing

IPM 2017

38 / 64

Conformance Testing

Example testcase: set(0), status, status, status, set(0)/0

rst/0

status, status, rst, status, t, status, set(1), status, t, status, set(1), rst, status, set(1), set(0), status

status/0

t/1

set(1) /0

status/0

set(0)/0

rst/0

set(1)/0

status/0 s0

t/1 set(0) t/1 set(1) status/1 set(0) set(1) rst/0 t/0 rst/0 t/1 /0 /0 /0 /0 s1

s1 status/1

rst/0 s0

s0 set(0) rst/0 t/0 /0

set(0)/0

s1

set(1)/0

Specification Transfer Fault 0,0, 0,0, 0, 0, 1, 1, 0,1,

status/1

set(1)/0

Output Fault

1,1, 0, 0, 0,0,0, 0,0,0

Mousavi

FSM-Based Testing

IPM 2017

39 / 64

Conformance Testing

Example testcase: set(0), status, status, status, set(0)/0

rst/0

status, status, rst, status, t, status, set(1), status, t, status, set(1), rst, status, set(1), set(0), status

status/0

t/1

set(1) /0

status/0

set(0)/0

rst/0

set(1)/0

status/0 s0

t/1 set(0) t/1 set(1) status/1 set(0) set(1) rst/0 t/0 rst/0 t/1 /0 /0 /0 /0 s1

s1 status/1

rst/0 s0

s0 set(0) rst/0 t/0 /0

set(0)/0

s1

set(1)/0

status/1

set(1)/0

Specification Transfer Fault Output Fault 0,0, 0,0, 0, 0, 1, 1, 0,1, 0,0, 0, 0, 0, 0, 1,1, 0,1, 1,1, 0, 0, 0,0,0, 0,0,0 1, 0, 1,1, 0,0,0 0,0,0 Mousavi

FSM-Based Testing

IPM 2017

39 / 64

Conformance Testing

Example testcase: set(0), status, status, status, set(0)/0

rst/0

status, status, rst, status, t, status, set(1), status, t, status, set(1), rst, status, set(1), set(0), status

status/0

t/1

set(1) /0

status/0

set(0)/0

rst/0

set(1)/0

status/0 s0

t/1 set(0) t/1 set(1) status/1 set(0) set(1) rst/0 t/0 rst/0 t/1 /0 /0 /0 /0 s1

s1 status/1

rst/0 s0

s0 set(0) rst/0 t/0 /0

set(0)/0

s1

set(1)/0

status/1

set(1)/0

Specification Transfer Fault Output Fault 0,0, 0,0, 0, 0, 1, 1, 0,1, 0,0, 0, 0, 0, 0, 1,1, 0,1, 0,0, 0, 0, 0, 0, 1,1, 0,1, 1,1, 0, 0, 0,0,0, 0,0,0 1, 0, 1,1, 0,0,0 0,0,0 1,1, 1, 0, 0,0,0 0,0,0 Mousavi

FSM-Based Testing

IPM 2017

39 / 64

Conformance Testing

Transfer Sequence

FSM’s usually have no set (j ): use homing sequence and transfer sequences

rst/0

A transfer sequence τ(i , j ): next (si , τ(si , sj )) = sj

τ(i , j ) need not be unique; the shortest

status/0

s0 t/1 rst/0 t/0

path can be found efficiently s1

Examples: HS = rst τ(0, 1) = t, τ(1, 0) = t or rst.

Mousavi

status/1

FSM-Based Testing

IPM 2017

40 / 64

Conformance Testing

Algorithm with Transfer/Homing Sequences

1 2

Go to a known final state s 0 For each state s and input a in A: set the state from s 0 (the current known state) to s, supply input a and check in B whether 1 2

Mousavi

output is output (s , a ) the target is next (s , a )

FSM-Based Testing

, and

IPM 2017

41 / 64

Conformance Testing

Algorithm with Transfer/Homing Sequences

1 2

Go to a known final state s 0 (using the homing sequence) For each state s and input a in A: set the state from s 0 (the current known state) to s, using τ(s 0 , s ) supply input a and check in B whether 1 2

Mousavi

output is output (s , a ) (observe the output), and the target is next (s , a ) (supply status and observe the output, if successful let s 0 = next (s , a ))

FSM-Based Testing

IPM 2017

41 / 64

Conformance Testing

Example testcase: first supply HS = rst, then supply ts, where: ts = status, status, rst, status, t, status, status, status, rst, status, t, t, status rst/0

rst/0 status/0

s0

status/0

rst/0 status/0

s0

s0

t/1

t/1 rst/0 t/0

rst/0 t/1

t/1 rst/0 t/0

status/1 s1

s1

s1

status/1

Specification 0, 0,0, 0,0, 1,1, 1,1, 0,0, 1,0,0

Mousavi

status/1

Transfer Fault 0, 0,0, 0, 0, 1,1, 1,0, , 0,0, 1,0,0

FSM-Based Testing

Output Fault 0, 0,0, 0,0, 1,1, 1,1, 0,0, 1,1,0

IPM 2017

42 / 64

Conformance Testing

“Status”, Realistic?

Sometimes present: registers in hardware, state dumps (logs) in protocols Usually not: let’s do without them and apply state identification (e.g., preset or adaptive distinguishing sequence) Challenge: distinguishing sequences change the state

Mousavi

FSM-Based Testing

IPM 2017

43 / 64

Conformance Testing

Algorithm with Nuts and Bolts 1

Go to a known final state s0 (homing sequence)

Mousavi

FSM-Based Testing

IPM 2017

44 / 64

Conformance Testing

Algorithm with Nuts and Bolts 1 2

Go to a known final state s0 (homing sequence) Take a sequence of all states s0 , . . . , sn+1 , where s0 = sn+1 . (state tour or state cover seq.) and let i = 0: 1 2

supply the DS and check if FSM is in si , FSM is in ti (due to DS), supply τ(ti , si +1 ) and repeat for i := i + 1, until i =n+1

Mousavi

FSM-Based Testing

IPM 2017

44 / 64

Conformance Testing

Algorithm with Nuts and Bolts 1 2

Go to a known final state s0 (homing sequence) Take a sequence of all states s0 , . . . , sn+1 , where s0 = sn+1 . (state tour or state cover seq.) and let i = 0: 1 2

3

supply the DS and check if FSM is in si , FSM is in ti (due to DS), supply τ(ti , si +1 ) and repeat for i := i + 1, until i =n+1

For each state si and input label a, (assuming that current state is sj0 ) 1

2

supply τ(sj0 , si −1 ), DS, τ(ti −1 , si ), take yourself back to the safe path, supply the input a , DS and check whether the output is output (si , a ) and FSM is in next (si , a ), the current state is sj0+1 (due to a , DS)

N.B. In step 3.1, one may apply τ(ti −1 , si ), if sj0 = ti −1 and skip the step if sj0 = si . Mousavi

FSM-Based Testing

IPM 2017

44 / 64

Conformance Testing

Example

rst/0 s0

rst/0 s0

t/1 rst/0 t/0 s1

Specification

Mousavi

t/1 rst/0 t/1 s1

Output Fault

FSM-Based Testing

IPM 2017

45 / 64

Conformance Testing

Example testcase: first supply HS = rst, output = 0 (no other choice!), then supply the state tour: t , t, then start testing t , t , rst , t , t , t , rst , t rst/0 s0

rst/0 s0

t/1 rst/0 t/0 s1

Specification

t/1 rst/0 t/1 s1

Output Fault

0, 1, 0, 1, 0, 0, 1, 0,1 0, 1

Mousavi

FSM-Based Testing

IPM 2017

45 / 64

Conformance Testing

Example testcase: first supply HS = rst, output = 0 (no other choice!), then supply the state tour: t , t, then start testing t , t , rst , t , t , t , rst , t rst/0 s0

rst/0 s0

t/1 rst/0 t/0 s1

t/1 rst/0 t/1 s1

Specification

Output Fault

0, 1, 0,

0, 1, 1,

1, 0, 0, 1, 0,1 0, 1

1, 1, 0,1, 1, 1, 0, 1

Mousavi

FSM-Based Testing

IPM 2017

45 / 64

Conformance Testing

Example

s0

s0 a/0

b/1

a/0 a/1

a/1

b/1

s1

a/0

s2

s1

b/0

b/0

Specification

Mousavi

a/0

b/0

s2

b/0

Transfer Fault

FSM-Based Testing

IPM 2017

46 / 64

Conformance Testing

Solution

Homing sequence: ba observed output 00 target state s2

01 s0

10 s2

Adaptive distinguishing sequences: DS (s0 ) = aa, output (s0 , aa ) = 00 DS (s1 ) = aa, output (s1 , aa ) = 01 DS (s2 ) = a, output (s2 , a ) = 1

Mousavi

FSM-Based Testing

IPM 2017

47 / 64

Machine Identification

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

48 / 64

Machine Identification

Basic Idea

Implementation: A blackbox B, only input-output observable Problem: by applying a testcase (a sequence of inputs) determine an FSM A such that A = B Same challenges as in conformance checking: B should be strongly connected, finite and constant. But that is not all...

Mousavi

FSM-Based Testing

IPM 2017

49 / 64

Machine Identification

Simple solution

Construct all different reduced and strongly connected FSM’s with n states and IB and OB as inputs and outputs, Use conformance testing: find the one conforming to B!

Mousavi

FSM-Based Testing

IPM 2017

50 / 64

Machine Identification

Towards Automata Learning

State-space explosion: with n states, p inputs and q outputs, (nq)np /n! machines 2 states, 2 inputs, 2 outputs, 256 machines! Possible Solutions: Run all possible machines simultaneously (construct “direct sum” machines) Use machine learning: have an oracle which provides a test-case for each failure

Mousavi

FSM-Based Testing

IPM 2017

51 / 64

Machine Identification

Towards Automata Learning

Mousavi

FSM-Based Testing

IPM 2017

52 / 64

Reversibility and Testing

Outline

1

Finite State Machines

2

Final State Identification

3

Initial State Identification

4

Conformance Testing

5

Machine Identification

6

Reversibility and Testing

Mousavi

FSM-Based Testing

IPM 2017

53 / 64

Reversibility and Testing

State Verification and Reversibility

UIO sequence A UIO sequence for a state s is a walk ρ such that ρ produces different output sequence from s than from any other state s 0 .

Mousavi

FSM-Based Testing

IPM 2017

54 / 64

Reversibility and Testing

State Verification and Reversibility

UIO sequence A UIO sequence for a state s is a walk ρ such that ρ produces different output sequence from s than from any other state s 0 . Hardness of State Verification Checking the existence of UIO Sequences is PSPACE-complete.

Mousavi

FSM-Based Testing

IPM 2017

54 / 64

Reversibility and Testing

State Verification and Reversibility

UIO sequence A UIO sequence for a state s is a walk ρ such that ρ produces different output sequence from s than from any other state s 0 . Hardness of State Verification Checking the existence of UIO Sequences is PSPACE-complete. General Idea Once a UIO sequence for a given state is found, one can construct UIOs for other states by taking transitions backwards.

Mousavi

FSM-Based Testing

IPM 2017

54 / 64

Reversibility and Testing

State Verification and Reversibility

General Idea Once a UIO sequence for a given state is found, one can construct UIOs for other states by taking backward transitions.

Mousavi

FSM-Based Testing

IPM 2017

55 / 64

Reversibility and Testing

State Verification and Reversibility General Idea Once a UIO sequence for a given state is found, one can construct UIOs for other states by taking backward transitions.

Mousavi

FSM-Based Testing

IPM 2017

56 / 64

Reversibility and Testing

State Verification and Reversibility General Idea Once a UIO sequence for a given state is found, one can construct UIOs for other states by taking backward transitions.

Mousavi

FSM-Based Testing

IPM 2017

57 / 64

Reversibility and Testing

State Verification and Reversibility General Idea Once a UIO sequence for a given state is found, one can construct UIOs for other states by taking backward transitions.

Empirical Evidence In 89% of the cases, UIOs can be constructed using invertible sequences from the UIO of a state. [Hierons and Turker, IEEE TSE’15] Mousavi

FSM-Based Testing

IPM 2017

58 / 64

Reversibility and Testing

Chasing Invertible Sequences

Mousavi

FSM-Based Testing

IPM 2017

59 / 64

Reversibility and Testing

Chasing Invertible Sequences

Mousavi

FSM-Based Testing

IPM 2017

60 / 64

Reversibility and Testing

Chasing Invertible Sequences

Mousavi

FSM-Based Testing

IPM 2017

61 / 64

Reversibility and Testing

Invertible sequences and Testing

Our order of business Finding a set of states S with UIO sequences; finding maximal (number of) invertible sequences to S.

Mousavi

FSM-Based Testing

IPM 2017

62 / 64

Reversibility and Testing

Invertible sequences and Testing

Our order of business Finding a set of states S with UIO sequences; finding maximal (number of) invertible sequences to S. Proper invertible sequences and UIO sequence An invertible sequence ρ is proper when all its suffixes are invertible sequences.

Mousavi

FSM-Based Testing

IPM 2017

62 / 64

Reversibility and Testing

Our Past Results in a Nutshell

Criteria: Maximizing the Number of Visited States 1

Finding the longest proper invertible sequences: NP-Complete

2

Finding spanning trees of invertible sequences: NP-Complete

3

Finding sets of invertible sequences: PSPace-Complete ¨ [Hierons, Kirkedal, MRM, Turker. SOFSEM’17]

Mousavi

FSM-Based Testing

IPM 2017

63 / 64

Reversibility and Testing

Ongoing Work

Finding long invertible sequences Idea: 1

Project the FSM into an properly invertible sub-FSM

2

Reverse the invertible sub-FSMs

3

Perform breadth-first search from the state(s) with UIOs

4

For the remaining states (without a proper invertible sequence), perform a subset construction (guided by heuristics) to find invertible sequences

Mousavi

FSM-Based Testing

IPM 2017

64 / 64