Skip to main content
User manualDeveloper documentation
TopologiesUse casesFAQs

22. Test High-level Properties using Model-Based Testing

· 2 min read

Status​

Accepted

Context​

  • We have been experimenting with quickcheck-dynamic for a while, leading to the implementation of basic Model-Based tests for the Hydra Head Protocol
  • These tests fill a gap in our testing strategy, between BehaviorSpec tests which test a "network" of nodes but only at the level of the off-chain Head logic, and EndToEndSpec tests which test a full blown network of nodes interconnected through real network connections and to a real cardano-node:
    • The former are fast but do not test the complete lifecycle of a Head. Furthermore, they are only unit tests so do not provide coverage into various corner cases that could arise in practice
    • The latter exercise the full lifecycle but are very slow and brittle
  • Because they run in io-sim, those Model-based tests are fast and robust as they don't depend on system interactions. Moreover, decoupling the System-under-Test from IO makes it easy to simulate an environment that deviates from the "happy path" such as delays from the network, filesystem errors, or even adversarial behaviour from the node, or the chain.

Decision​

  • We will maintain and evolve the Model over time to cover more features
  • Key properties of the whole system should be written-down as proper DynamicLogic properties and thoroughly tested using quickcheck-dynamic. This includes but is not limited to:
    • Liveness of the Head
    • Consistency of the Head
    • Soundness of Chain
    • Completeness of Chain

Consequences​

  • We need to ensure the Model covers the full lifecycle of a Hydra Head network which at the time of writing this ADR is not the case
  • There cannot be One Model to Rule Them All so we should refrain from defining different StateModel or different RunModel depending on what needs to be tested
  • In particular, testing against adversarial conditions will certainly require defining different instances of the Network or Chain components, for example:
    • An Accepted Adversary that fully the controls the protocol and the parties,
    • A Network Adversary that can delay and or drop messages,
    • A Faulty Filesystem that can causes exceptions when reading or writing files,
    • ...