Week 7

Question 1

What is an LTS with inputs and outputs (Input Output Transition System - IOTS)?

Answer 1

An LTS that distinguishes for any given action where it is an input or output of a system

Question 2

How is an LTS formally defined

Answer 2

(S,s0,Li,Lu,->)

Question 3

How are inputs and outputs distinguished in an LTS with inputs and outputs?

Answer 3

Inputs have a ? before whilst outputs have a !

Question 4

Do all outputs have to be enabled in every state of an LTS with inputs and outputs?

Answer 4

No, all outputs do not have to be enabled in every state.

Question 5

Do all inputs have to be enabled in every state of an LTS with inputs and outputs?

Answer 5

Yes, all inputs ahve to be enabled in every state of an LTS with inputs and outputs.

Question 6

What is an implementation under test (IUT)?

Answer 6

A system or component being tested, i.e., the actual implementation of the system being evaluated for conformity to certain specifications.

Question 7

For every implementation under test (IUT) and a test t, there exists an IOTS model mIUT such that:

Answer 7

IUT passes t if and only if mIUT passes t

Question 8

What is conformance of an implementation to a specification (informal answer)?

Answer 8

Implementation i conforms to specification s when any behaviour from implementation i is predicted/allowed by specification s.

Question 9

When is a state s quiescent?

Answer 9

If for all outputs and internal transitions, the state does not have a transition defined by them.

Question 10

How is quiescence drawn?

Answer 10

As a self-loop with a greek symbol.

Question 11

What are the suspension traces starting in a given state s?

Answer 11

All of the weak traces starting in that state extended with quiescence too

Question 12

What is the output of a state?

Answer 12

All of the different outputs plus quiescence that leave from that state.

Question 13

Input-Output Conformance - Formal Definition:

i ioco s means:

Answer 13

For all suspension traces t of the specification s, the outputs after running t on implementation i are a subset of the outputs after running t on specification s.

Question 14

What is a test transition system TTS

Answer 14

An LTS used for test generation defined as follows:

Has Labels L U theta, where L are the inputs and outputs of the LTS it tests, and theta represents the quiescence label.

Inputs and outputs have exchanged signs.

Tree structure.

Finite, deterministic.

Final states “pass” and “fail”

From each state that is not a pass or a fail you either have:
- one input !a and all outputs ?x
OR
- all outputs ?x and theta

Question 15

Test Generation Algorithm

Answer 15

To generate a test case t(S) from a transition system specification with S set of states, apply the following steps non-deterministically:

1. End test case
2. Supply input
3. Observe output

Question 16

What is a test run of a TTS on an implementation?

Answer 16

The parallel running of a shared suspension trace that either reaches fail or pass in the TTS.

Question 17

What is a test case?

Answer 17

An entire test transition system generated by the Test Generation Algorithm.

Question 18

When does an implementation pass a test case?

Answer 18

An implementation passes a test case when for all shared suspension traces of the implementation and test test transition system, the test transition system does not reach a fail for any of them.

Question 19

When is a test case t sound?

Answer 19

A test case t is sound if it never fails with a correct implementation.

Question 20

What does i ioco s imply in relation to all tests t generated by the Test Generation Algorithm? Consequently, what does i fails t imply in relation to i ioco s?

Answer 20

That i passes all of these tests t.

i ioco s does not hold.

Question 21

What is the effect on the soundness of a previously sound test if it is changed from a fail to a pass?

Answer 21

It remains sound as it still never fails a correct implementation.

Question 22

What is the effect on the soundness of a previously sound test if it is changed from a pass to a fail?

Answer 22

The test may possibly not be sound anymore.

Question 23

When is test generation exhaustive?

Answer 23

When each incorrect implementation can be detected with a test.

Question 24

When is a test generation complete?

Answer 24

When it is sound and exhaustive.

Thus, a complete test suite finds all bugs.

Question 25

Is test generation with the Test Generation Algorithm complete?

Answer 25

It is sound and technically complete, though an infinite number of test cases is needed for exhaustiveness.

Question 26

What is the problem of underspecification for ioco?

Answer 26

specification in ioco only considers outputs of suspension traces of specification, but specifications are not input-enabled

Question 27

What is the problem of composition for ioco and how can it be fixed?

Answer 27

ioco cannot be used on subcomponents to draw conclusions about entire compositions

this can be fixed by ensuring that specifications are input-enabled

Question 28

What does S refuses L mean, where S is a set of states and L is a set of labels?

Answer 28

This means that there exists a state s in S such that for all labels in L including the internal transition, s cannot go anywhere.

Question 29

What are the Utraces of a given state?

Answer 29

The set of suspension traces t starting in that state such that for any two combinations of labels including quiescence s1, s2 and an input a, if t=s1as2 then it does not hold that the specification s after label s1 refuses a.

Question 30

i uioco s means

Answer 30

For all Utraces u starting in s, the outputs of i after u is a subset of the outputs of s after u.

Question 31

What is the purpose of demonic completion? How does it work?

Answer 31

To make specifications input-enabled

Add a special error state and from all states add a a transition to this error state for all non-enabled inputs.

The error state cannot be left.