Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal

The contract automata runtime environment (CARE) is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.