Modelling, verifying and testing the contract automata runtime environment with Uppaal
Basile D.
Contract automata Runtime environment Formal verification Testing Uppaal Model-based
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.
Source: ISTI Working papers, 2023
Back to previous page
@techreport{oai:it.cnr:prodotti:487363,
title = {Modelling, verifying and testing the contract automata runtime environment with Uppaal},
author = {Basile D.},
institution = {ISTI Working papers, 2023},
year = {2023}
}
0000-0002-7196-6609