Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

TL;DR

This paper presents a formal approach to model, verify, and test the CARE distributed middleware using stochastic timed automata and Uppaal, enhancing its dependability through rigorous analysis.

Contribution

It introduces a formal modelling and verification framework for CARE with Uppaal, including test generation from models, improving reliability of distributed automata applications.

Findings

Successful formal modelling of CARE as stochastic timed automata

Verification of properties using Uppaal's exhaustive and statistical methods

Generation of concrete tests from abstract models for system testing

Abstract

Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing 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, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. 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 generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.