Compositionality in Model-Based Testing

1 Introduction

• MBT uses system models to automatically generate and execute tests, reducing test-suite work to creating and maintaining a model.Large, complex systems make those models difficult to create, often because no single person understands the whole system well enough.Source: §1 · p. 1
• Compositional MBT would let teams model and test components separately while inferring correctness of the composed system from component correctness.The paper identifies this as a response to the difficulty of creating models for complex systems.Source: §1 · pp. 1–2
• The paper defines mutual acceptance over component specifications to guarantee correct communication and preserve uioco under parallel composition.It uses labelled transition systems, uioco, and parallelism to model composition, and generalizes prior results with less restrictive assumptions and an associative composition operator.Source: §1 · p. 2
• Mutual acceptance is also presented as useful for retesting systems with updated components and for diagnosing component-based systems.The paper’s overview assigns these applications to its discussion of component substitution and diagnosis.Source: §1 · p. 2

2 Preliminaries

• A labelled transition system models events as transitions among states, with inputs, outputs, and unobservable internal transitions τ.Its formal tuple comprises states, input labels, output labels, a transition relation, and an initial state.Source: §2 · pp. 2–3
• Implementations are represented as input-enabled transition systems, reflecting the assumption that any input can be given to an implementation.Input-enabledness requires every input to be accepted in each state or after internal transitions.Source: §2 · p. 3
• Parallel composition executes components concurrently and synchronizes on shared labels; asynchronous communication requires an explicitly specified medium.The components’ output sets must be disjoint, while their input sets need not be disjoint.Source: §2 · p. 4
• The composition operator is associative and commutative, allowing more than two components to be composed regardless of grouping or order.Disjoint output sets are the remaining composability restriction; output labels can be renamed to satisfy it.Source: §2 · pp. 4–5
• The paper retains synchronized labels rather than hiding them as τ, because hiding removes information and can introduce divergence.The paper also notes that uioco handles nondeterministic underspecification differently from ioco and is better suited to reasoning about composition.Source: §2 · p. 5

3 Motivating Example: A Parking System

• The example pairs a sensor with a parking actuator; the actuator continues while the sensor signals safety and stops when an obstacle is detected.The sensor is intentionally underspecified after detecting an obstacle once it has been turned off, provided it does not start beeping.Source: §3 · p. 6
• Although each implementation is uioco-correct against its own specification, their composed implementation is not uioco-correct against the composed specification.The example shows the component specifications and implementations in Fig. 3 and their compositions in Fig. 4.Source: §3 · p. 6
• Composition exposes implementation-only outputs that trigger test errors, alongside a real error in which the parking system continues despite a newly detected obstacle.The component specifications rely on unspecified behavior; expanding them to be input complete would remove underspecification, which keeps models smaller and more readable and gives implementers freedom.Source: §3 · p. 7

4 Mutual Acceptance

• Under uioco, an absent input leaves all subsequent behavior unspecified, whereas outputs are either explicitly allowed or disallowed.The mutual-acceptance condition addresses this by requiring a component to accept a synchronized output produced by its partner after a trace of the composition.Source: §4 · pp. 7–8
• Mutual acceptance checks whether each component accepts the other’s synchronized outputs at reachable states of their composition.The passage describes the condition over traces of the composed specifications and the component states reached after those traces.Source: §4 · p. 8
• The relation is neither reflexive nor transitive, so each pair of specifications must be checked independently.It is defined only for composable specifications, and each pair has its own state pairs and shared labels to check.Source: §4 · p. 9

5 Compositionalility for uioco

• Mutual acceptance lets Utraces of a composed system be projected to component Utraces and reconstructed from them.This trace correspondence is needed because uioco concerns Utraces, including the special label δ.Source: §5 · pp. 9–10
• Composable systems give each composed trace a unique pair of component projections, because labels are synchronized or belong to only one component.This avoids ambiguity from unsynchronized shared labels.Source: §5 · p. 9
• For mutually accepting specifications, component-level uioco correctness is preserved under parallel composition.The theorem also says that a composed implementation failure can be found by testing at least one component, but not conversely.Source: §5 · p. 10
• Mutual acceptance prevents invalid communicated outputs but cannot enforce that a component produces a required output.A component's quiescence may therefore be masked by outputs from another component, so the reverse implication of the theorem fails.Source: §5 · p. 10
• The theorem assumes the composed implementations behave as their modeled composition, with channels connected as specified and no hidden environment effects.The physical composition must match the modeled parallel composition.Source: §5 · p. 10

6 The Parking System Revisited

• The original specifications are not mutually accepting: safe·obs reaches a state where S1 can output beep but S2 does not accept beep.Counterexamples identify where specifications need extension; the beep case requires the car to stop rather than continue parking.Source: §6 · p. 11
• I3||I4 uioco S3||S4 after the adapted specifications are used and each implementation is updated to conform to its own specification.Before those updates, the composition can produce park after safe·obs·beep, which is disallowed by the composed specification.Source: §6 · p. 11
• The composed adapted specification and implementation are shown as S3||S4 and I3||I4 in Fig. 6.The adapted specifications need not define every input, and the integration analysis does not require actual implementations.Source: Figure 6 · p. 12, §6 · p. 12

7 Component Substitution and Diagnosis

• Replacing a deprecated component can change the other components' environment and expose them to inputs not previously tested.The paper cites the Ariane-5 failure as an example of reuse in a changed environment invalidating prior testing.Source: §7 · p. 12
• Testing done before a component replacement remains useful because MBT tests every defined input sequence and mutually accepting specifications communicate only defined inputs.If the replacement specification is not mutually accepting with the rest of the system, counterexamples identify undefined inputs for specification improvement and focused testing.Source: §7 · pp. 12–13
• When the whole system fails and some components are uioco-correct, mutual acceptance can narrow a system counterexample to a specific faulty component.The last output identifies the component unless it is δ; for δ, projected traces can be replayed in each component.Source: §7 · p. 13

8 Related Work

• Interface automata encode environmental constraints through missing input transitions, while their pruning approach can remove behavior needed to express the desired correct behavior.The paper instead adds transitions to component specifications until problem areas no longer exist.Source: §8 · pp. 13–14
• The paper’s parallel composition differs slightly from interface automata’s to make it associative, and its mutual acceptance relation seems to coincide with the absence of reachable error states.The paper includes quiescence and links directly to uioco, making the theory easier to apply with existing MBT tools.Source: §8 · pp. 13–14
• Eco relates an environment specification to a black-box component implementation; conformance is checked by testing, must be redone completely whenever a component changes, and requires all labels to communicate.Source: §8 · p. 14
• Contract theory also models valid environments and implementations, but the account in restricts environments and components and omits internal transitions and quiescence.The cited work extends contract properties, while studies decomposing requirements into component contracts.Source: §8 · p. 14
• The operating-guideline approach assumes asynchronous communication, whereas this paper assumes synchronous communication.It describes a most-permissive communication partner, with concrete partners related to it by refinement.Source: §8 · pp. 14–15

9 Future Work

• Mutual acceptance adds behavior to specifications; the beep transition may capture missed behavior, while most added selfloops make unspecified inputs ignorable.If inputs are instead buffered until a component is ready, specifying them immediately may not be necessary; investigating automatic repair is also proposed.Source: §9 · p. 15
• Practical algorithms for checking mutual acceptance and testing procedures analogous to eco remain to be developed.The paper defines the relation but gives no practical checking method.Source: §9 · p. 15
• The theory is developed for two components; inferring multiway mutual acceptance from pairwise acceptance is postulated, and complicated communication structures need further investigation.Repeated parallel composition and theorem 1 offer one way to treat larger systems, though checking an intermediate composition may become complicated.Source: §9 · p. 15
• Requiring mutual acceptance at every intermediate step rules out unexpected outputs even when other components would prevent them in the final composition.The paper suggests investigating a different definition for mutual acceptance among more than two components at once.Source: §9 · p. 15
• Practical application requires extending the theory with data, since real systems exchange instances of data types rather than using a finite set of labels.Extending the concepts to symbolic transition systems (STS), the formalism underlying several MBT tools, is proposed.Source: §9 · pp. 15–16

10 Conclusion

• Under faithful parallel composition, mutual acceptance preserves uioco-correctness when component implementations are composed, without requiring all specifications to be input-enabled.The result applies when each component has been tested for uioco-correctness against its specification.Source: §10 · p. 16
• The conclusion also identifies uses for mutual acceptance when replacing older components and localising a faulty component during diagnosis.These uses are stated alongside the compositionality result.Source: §10 · p. 16

A Proofs for Section 2 (Preliminaries)

• Parallel composition is commutative and associative up to isomorphism.In particular, (s || e) || t is isomorphic to s || (e || t).Source: A Proofs for Section 2 (Preliminaries) · p. 21

• The proofs adapt earlier lemmas [18] to avoid requiring input-enabled specifications and use the mutual-acceptance relation instead.Source: B Proofs for Section 5… · p. 25
• Lemma 7 relates single transitions of a composition to component transitions; the reverse direction generally fails for LTSs but holds both ways for input-enabled systems under Lemma 8.Source: B Proofs for Section 5… · p. 29
• The trace proofs use induction and divide transitions into label-set cases because trace membership and projection behavior depend on whether labels are inputs, outputs, or shared.Source: B Proofs for Section 5… · pp. 36, 41
• If s and e mutually accept and each implementation conforms to its specification under uioco, then their composition also conforms under uioco.Source: B Proofs for Section 5… · p. 45

• Input-complete components rule out communication problems: if one produces an output, the other accepts it as an input.Source: C Proofs for Section 7 (Component… · p. 48
• When both component states are quiescent, the proof identifies a counterexample to uioco correctness for at least one component.Source: C Proofs for Section 7 (Component… · p. 48