PaperlayerView exact revision on arXiv

Source-linked AI summary

Model-Based Testing IoT Communication via Active Automata Learning

Martin Tappler, Bernhard K. Aichernig, Roderick Bloem

arXiv:1904.07075v1cs.SE

TL;DR

The paper addresses black-box detection of faults in reactive-system implementations by learning models of multiple implementations and cross-checking them. In a case study of five MQTT brokers, the authors found 17 bugs, with none in Mosquitto, and discuss limits including the counterexample-analysis burden for more complex systems.

  • Problem

    The paper targets fault detection in reactive-system implementations whose internal structure is unknown but which implement a common specification.

    Source: D. Bug Hunt · p. 7

  • Method

    The authors learn models of five MQTT brokers, use a mapper to abstract their large input space, and cross-check learned models for counterexamples.

    Source: 1) Architecture · p. 4, 3) Discussion · p. 9

  • Results

    17 bugs were found across the implementations, none in Mosquitto; two cases of unexpected non-determinism hindered learning and were excluded from that total.

    Source: D. Bug Hunt · p. 7

  • Takeaways & Limitations

    Non-trivial protocol-implementation bugs can be found with reasonable effort despite severe abstraction, and setting up a learning environment is relatively low effort.

    Source: 3) Discussion · p. 9

    For more complex systems, learning may be hindered by the large number of counterexamples that require analysis.

    Source: 3) Discussion · p. 9

Abstract

from arXiv · show

This paper presents a learning-based approach to detecting failures in reactive systems. The technique is based on inferring models of multiple implementations of a common specification which are pair-wise cross-checked for equivalence. Any counterexample to equivalence is flagged as suspicious and has to be analysed manually. Hence, it is possible to find possible failures in a semi-automatic way without prior modelling. We show that the approach is effective by means of a case study. For this case study, we carried out experiments in which we learned models of five implementations of MQTT brokers/servers, a protocol used in the Internet of Things. Examining these models, we found several violations of the MQTT specification. All but one of the considered implementations showed faulty behaviour. In the analysis, we discuss effectiveness and also issues we faced.

I. INTRODUCTION

The paper proposes and evaluates black-box learning and cross-checking to find faults in MQTT brokers, addressing a gap in case studies of conformance checking between learned models. It asks whether this approach can find non-trivial faults despite abstraction and what limits it.

I. INTRODUCTION

  • The approach learns models of multiple implementations, cross-checks them pair-wise for conformance, and manually analyzes counterexamples against the standard to identify bugs or underspecification.The implementations are treated as black boxes with unknown structure and a common natural-language specification.Source: §I · p. 1
  • The approach may miss faults shared by all examined implementations, and detection is limited by the abstraction level used for learning.These limitations motivate questions about detecting non-trivial faults despite severe abstraction and about the approach's limits.Source: §I · p. 1
  • The paper empirically evaluates the approach by learning models of five MQTT brokers and examining detection effort, runtime issues, and general challenges.MQTT is a lightweight publish/subscribe protocol suited to resource-constrained IoT environments; brokers forward published messages to subscribed clients.Source: §I · p. 2
  • The authors identify a gap in case studies applying conformance checking between learned models in a purely black-box setting and in verification of MQTT implementations.They contrast their unknown implementations with prior work on artificially seeded faults in implementations generated from known models.Source: §I · pp. 1–2

II. RELATED WORK

Related work combines learning with testing or verification, while this paper's setting emphasizes unknown system structure and network-communication challenges. The paper uses Mealy machines to represent reactive systems and compare their output behavior.

II. RELATED WORK

  • Unlike work on generated or seeded-fault implementations, the paper addresses unknown system structure and network-communication challenges such as long response times.Aarts et al. learned models of a reference and mutated implementations whose structure was known.Source: §II · p. 2
  • Prior studies also learned models of black-box systems, analyzed TLS implementations, targeted protocol state-machine flaws, and applied model checking to TCP implementations.The cited examples include Peled et al. and Groce et al., de Ruiter and Rutten, Beurdouche et al., and Fiterău-Broștean et al.,.Source: §II · p. 2

A. Mealy Machines

  • A Mealy machine models a reactive system as a finite-state automaton that changes state on inputs and produces exactly one output per input.The paper uses this formalism because it suits reactive systems and is supported by LearnLib.Source: A. Mealy Machines · p. 2
  • Two deterministic Mealy machines are equivalent when they produce the same outputs for every input sequence; a sequence with differing outputs is a counterexample.The paper's equivalence definition compares the output functions of the machines over all input sequences.Source: A. Mealy Machines · p. 3

B. Active Automata Learning

The paper describes active automata learning in the minimally adequate teacher framework, where a learner builds and revises a hypothesis through queries to a teacher. Counterexamples trigger another learning round.

B. Active Automata Learning

1) Minimally Adequate Teacher Framework:

  • Membership queries gather information for a hypothesis, while equivalence queries ask whether that hypothesis matches the target and may return a counterexample.In Angluin's L∗ example, membership queries ask whether strings belong to a language.Source: 1) Minimally Adequate Teacher Framework · p. 3
  • When a counterexample is returned, the learner incorporates it and starts another round of membership queries followed by an equivalence query.This iterative pattern is shared by MAT algorithms, with adaptations for learning Mealy machines.Source: 1) Minimally Adequate Teacher Framework · p. 3

2) Learning Mealy Machines:

Learning Mealy machines requires output queries against the black-box system and an approximate equivalence test, since direct equivalence checking is generally unavailable. Testing-based equivalence checks can be incomplete, so learned models may remain incorrect.

2) Learning Mealy Machines:

  • Mealy-machine learning algorithms based on L∗ use output queries, in which an input sequence receives a corresponding output sequence from the teacher.For black-box systems, such queries assume inputs execute from the initial state, so the system must be resettable.Source: 2) Learning Mealy Machines · p. 3
  • Because a black-box system cannot normally be checked directly for equivalence with a hypothesis, the teacher approximates equivalence queries through conformance testing.The teacher compares outputs from tests on the system and hypothesis; a mismatch supplies a counterexample to the learner.Source: 2) Learning Mealy Machines · p. 3
  • Replacing equivalence queries with incomplete testing can leave the learned model incorrect, including when W-method state-count assumptions do not hold.The paper then introduces its approach and technical considerations for learning Mealy-machine models.Source: 2) Learning Mealy Machines · pp. 3–4, §IV · p. 4

A. Learning

The MQTT learning setup controls multiple clients and uses a mapper to handle the large packet input space. Its practical choices simplify asynchronous outputs but trade away some ordering information and exclude features that require time-dependent or data-dependent behavior.

1) Architecture:

  • Multiple clients are needed to capture MQTT broker behavior because clients have dependencies and each client's received messages must be recorded.The setup uses client adapters and interfaces to control the environment around the broker.Source: 1) Architecture · p. 4
  • A static mapper abstracts the large packet input space, with manual setup changes when abstraction or output processing causes detected nondeterminism.Unlike cited approaches, the abstraction is not refined iteratively.Source: 1) Architecture · p. 4

2) Practical Considerations:

  • A configurable timeout groups received messages into an abstract output; no message before the timeout is represented as Empty.The paper notes that communication is asynchronous and a broker may produce no output.Source: 2) Practical Considerations · p. 4
  • Messages are sorted alphabetically and concatenated to make one deterministic output per client, but sorting loses ordering information restricted by MQTT.This is a completeness-versus-efficiency tradeoff against learning nondeterministic models.Source: 2) Practical Considerations · pp. 4–5
  • The analysis excludes ping behavior and acknowledgement behavior, which require time-dependent modeling and matching sent and received identifiers, respectively.Acknowledgements are sent automatically; the authors note these exclusions do not affect the MQTT parts they learn.Source: 2) Practical Considerations · p. 5

B. Learning-Based Testing

The approach learns models of multiple implementations, checks them pairwise for conformance, and manually investigates counterexamples. Its scope is bounded by abstraction and shared faults, while splitting inputs and learning models offers practical benefits and tradeoffs.

B. Learning-Based Testing

  • Because no implementation is known to be correct, violations are suspicious traces for manual review, not errors established by model comparison alone.A learned model may itself be incorrect if its implementation is faulty.Source: B. Learning-Based Testing · p. 5
  • Some faults remain undetectable when abstraction hides them or when all compared implementations share them; comparing five implementations reduces the latter risk.A counterexample may reveal zero, one, or two errors depending on specification freedom and which implementations are faulty.Source: B. Learning-Based Testing · p. 5
  • Separating the input alphabet into subsets assumes independence across subsets, which may impede fault detection.Inputs within each subset are selected for interesting dependencies.Source: B. Learning-Based Testing · p. 5
  • Learn models for each input alphabet, check every model pair for equivalence, then test counterexamples on the implementations and manually assess their outputs.Testing the traces on the implementations checks that a counterexample reflects an implementation difference rather than a learning error.Source: B. Learning-Based Testing · p. 5
  • The approach avoids formalizing the full natural-language requirements, reducing manual effort, but gives less control over test selection.Learning algorithms select the tests, whereas traditional model-based testing can direct test generation with selection criteria.Source: B. Learning-Based Testing · p. 6
  • Learned models provide models for further verification and a stopping criterion: testing can stop when learning yields a correct system model.The paper contrasts this with random test suites that do not provide a learned model.Source: B. Learning-Based Testing · p. 6

V. CASE STUDY

The case study combines active automata learning with application-specific MQTT components and configuration. Seven mappers cover selected behaviors; the study does not aim to test brokers completely.

A. Learning

  • The learning implementation uses LearnLib through its Java library, with application-specific mappers and a component for configuring experiments.The learning portion was implemented in Scala.Source: A. Learning · p. 6

1) Application-Specific Components:

  • The application-specific setup implements an adapter, client interface, and mapper; the mapper specifies the learning target.The adapter and client interface parse, serialize, and send packets.Source: 1) Application-Specific Components · p. 6
  • Seven interchangeable mappers use the same client interface to test different aspects, while the study explicitly does not aim at complete MQTT broker testing.Examples include a basic one-client mapper and a two-client retained-will mapper.Source: 1) Application-Specific Components · p. 6

2) Configuration:

  • Experiments use the TTT learning algorithm and LearnLib's random-walk equivalence oracle because thorough methods such as W-method and Wp-method do not scale well at moderate model complexity.The random walks use a 0.05 reset probability and a maximum of 10,000 steps; an application-specific timeout is also configured.Source: 2) Configuration · p. 6

B. Conformance Checking

The study checks learned-model equivalence using bisimulation and investigates counterexamples, while experiments learn models of five MQTT brokers. Extended exploration exposed under-tested models and prompted longer random equivalence testing.

B. Conformance Checking

  • The equivalence check builds a product of two Mealy machines and finds fail-states when an input produces different outputs, thereby checking observation equivalence.The implementation uses depth-first search and returns traces to fail-states as counterexamples.Source: B. Conformance Checking · p. 7
  • The ordinary exploration may miss a second bug on a trace after a wrong output; extended exploration can continue to seek further differences, at added analysis effort.The extended search can be bounded by a preset maximum number of differences along a trace.Source: B. Conformance Checking · p. 7
  • Extended exploration found no additional bugs, but cross-checking exposed two incorrectly learned models and led to more random equivalence-testing steps.The issue arose from insufficient equivalence testing.Source: setup · p. 7

C. Experiments

  • The case study learned models of five freely available MQTT brokers, all implementing MQTT version 3.1.1, with implementation-specific message-receipt timeouts.The timeout values were experimentally chosen and are neither claimed optimal nor a general measure of broker performance.Source: C. Experiments · p. 7

D. Bug Hunt

The bug hunt found 18 bugs across the implementations, including specification violations in connection handling and retained-message delivery. Four bugs had already been reported; the remaining bugs were reported by the authors and were under review or fixed.

D. Bug Hunt

  • 18 bugs were found overall, with none in Mosquitto; two non-determinism cases were excluded from the bug count.Although none implemented one specification detail strictly, four behaved as users would expect and were considered correct; the last implementation behaved incorrectly.Source: D. Bug Hunt · pp. 7–8
  • Four bugs had already been reported, while the rest were reported by the authors and were under review or already fixed.The authors state that they will give examples of bugs and issues encountered.Source: D. Bug Hunt · p. 8

1) Violations of the Specification:

A Client can only send the CONNECT Packet once

  • After a repeated subscription, emqttd and ActiveMQ fail to resend a matching retained message, contrary to the MQTT requirement.In the example sequence, Mosquitto resends the retained message “bye,” unlike emqttd and ActiveMQ.Source: A Client can only send the CONNECT… · p. 8

2) Non-Determinism:

The experiments found that non-determinism can stop learning, while manual counterexample analysis and long runtimes constrain the approach. The authors nevertheless conclude that non-trivial protocol bugs can be found with reasonable effort despite harsh abstraction.

2) Non-Determinism:

  • Timeouts address uncertain broker response times but introduce imprecision; time-related non-determinism may be more severe for other IoT protocols.The paper notes this possibility when comparing TCP with UDP use in IoT.Source: 2) Non-Determinism · p. 8
  • Three of 35 bug-hunt learning experiments could not be completed because the setup could not reasonably accommodate actual non-determinism.Additional MQTT implementations were excluded after showing non-deterministic behaviour even with the simplest mapper.Source: 2) Non-Determinism · pp. 8–9

3) Discussion:

  • Analysing suspicious traces took significant manual effort, and extended bisimulation checking added further effort.Counterexamples were also tested as stand-alone tests to identify spurious ones and form a regression suite focused on previously detected bugs.Source: 3) Discussion · p. 9
  • Seven counterexamples from standard bisimulation and 24 from extended exploration pointed to only two bugs in the Fig. 4 models.This illustrates that counterexample counts need not correspond to distinct bugs.Source: 3) Discussion · p. 9
  • Counterexample reduction or automated grouping may be crucial for complex systems, where input-enabled models can interleave irrelevant inputs into traces.The authors did not use their manual filters because coarse patterns may cause bugs to go undetected.Source: 3) Discussion · p. 9
  • Incomplete learning and inherently incomplete testing leave open the possibility that erroneous behaviour will go undetected.The authors also observe that bugs usually produce several counterexamples, which lowers—but does not remove—the probability of missing them.Source: 3) Discussion · p. 9
  • Non-trivial protocol bugs can be found with reasonable effort despite the necessary harsh abstraction.Applying the approach to more complex systems may be hindered by the number of counterexamples requiring analysis.Source: 3) Discussion · p. 9

E. Efficiency

Learning runtime was substantial even for small models, largely because individual tests and queries took a long time. The experiments measured model size, membership-query costs, and conformance-testing costs across two mappers.

E. Efficiency

  • The experiments recorded model states, membership-query time and count, and conformance-testing time and count.Conformance-test counts represent tests run during equivalence queries; the number of equivalence queries gives the learning rounds and hypotheses constructed.Source: E. Efficiency · p. 9
  • The largest learned model had 18 states and the larger alphabet had nine inputs, yet long individual tests and queries still caused efficiency problems.The two tables cover the Simple mapper with alphabet size 7 and Two Clients with Retained Will with alphabet size 9.Source: E. Efficiency · p. 9, Table II · p. 10, Table III · p. 10
  • Unlike the cited TLS learning setup, MQTT learning continued after connection closure to capture persistent-session behaviour such as session resumption.The paper says this contributes to the observed runtime context.Source: E. Efficiency · p. 10
  • Almost 16 minutes were needed to learn VerneMQ’s simplest model, while ActiveMQ’s Two Clients with Retained Will experiment took over 110 minutes for an 18-state model.The paper argues that these runtimes make minimizing the number and length of queries important.Source: E. Efficiency · p. 10, Table III · p. 10

VI. CONCLUSION

The case study found 18 faults in four of five MQTT brokers and showed that failures can be investigated without prior modelling. The conclusion also identifies nondeterminism and timing as directions for further work.

A. Summary

  • 18 faults were found in four of the five MQTT brokers examined.The case study’s learned models exposed observable differences that were inspected manually for specification violations.Source: A. Summary · p. 10
  • The study learned abstract broker models, detected implementation differences automatically, and manually checked whether they violated the specification.The authors describe this as the first case study of its kind focused on reactive systems implemented independently by open-source developers, and the first attempt at model-based testing MQTT brokers.Source: A. Summary · p. 10
  • The approach can detect bugs without prior modelling, but long interactions and unknown response delays can make learning inefficient.The paper notes that active automata learning has efficiency problems with large input alphabets and state spaces, which is especially problematic for MQTT implementations with long, unknown response delays.Source: A. Summary · p. 10
  • Protocol testing is a particularly suitable application because protocols can have low-state abstractions and commonly have well-defined standards; the approach may also support regression testing.For regression testing, a new version’s learned model could be checked for conformance to a previous version’s model.Source: A. Summary · p. 10

B. Future Work

  • Nondeterministic behavior remains difficult to learn completely: the needed number of repeated input sequences is unknown, and repetition increases computation time.The authors suggest investigating nondeterministic Mealy machines or input-output transition systems, while noting that neither approach can guarantee that all behaviors have been observed.Source: B. Future Work · p. 10
  • Probabilistic models learned from prior samples are another proposed way to address output nondeterminism.The authors point to passive state-merging approaches as candidates for further investigation.Source: B. Future Work · p. 10
  • Time-dependent behavior may matter more in IoT protocols using less reliable communication than TCP, motivating investigation of timed-system learning methods.The cited active event-recording automata approach is less restricted in expressiveness than passive single-clock timed automata, but has higher worst-case complexity.Source: B. Future Work · pp. 10–11
  • A possible MQTT extension is to learn client models as well as broker models and verify properties of their composition.The authors note that a similar approach has been used to analyze TCP implementations.Source: B. Future Work · p. 11
Loading 1904.07075v1…