EPIC: Model-Based Testing using the Quint model

[p-offtermatt]

Problem

The existing difftest model is unmaintained. We want an alternative approach to automatically generating test traces.

Closing criteria

We have a minimal prototype for MBT of ICS using the Quint model.
It allows

• generating traces, and
• replaying traces

Problem details

The goal of this epic is to get a proof-of-concept prototype of model-based testing for interchain security.
The key outcome of this epic is data on the effort/reward ratio of model-based testing, and generally to get experience with the MBT approach. Accordingly, this epics deliverable is a minimal prototype.

A secondary goal is also to improve our confidence:
a) in the correctness of the model
b) in the alignment of the code with the model
c) and thus in the correctness of the code

The confidence increase in the correctness of the implementation is not the main outcome of the epic - the part of interchain security that the model deals with is already well tested (it is running in production!).
It is rather to try out this approach and get familiar with it, to judge whether this is something we want to incorporate more deeply e.g. when we make changes to the protocol, where increasing our confidence is crucial.

Task list

Must have

Beta Give feedback

1. Rewrite the TLA+ ICS model in Quint (see https://github.com/cosmos/ibc/pull/911) #1239
   S: Productivity scope: testing +2
   
2. Modify the e2e framework to take traces as an input #1240
   S: Productivity scope: testing +2
   
3. Write a shim/driver that handles Quint-generated traces #1241
   S: Productivity scope: testing +2
   

Nice to have

Beta Give feedback

No tasks being tracked yet.