Model-based testing is a compelling method for the end-to-end testing of microservices. However, when testing with a large number of services, state space explosion is a common problem. It is especially a problem since input-output conformance (ioco) is not compositional. We developed a novel and theoretically grounded testing method called model-based mocking (MBM) to end-to-end test microservice systems compositionally. We tested the MBM method using the Axini Modeling platform by inserting 20 mutants into an example microservice system. In our set of inserted bugs, MBM found more than half of the bugs faster compared to other methods and was slower for none of the bugs.

The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal mu-calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed.
Preprint