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.

翻译：近期，一种名为合约自动机运行时环境（CARE）的分布式中间件应用被提出，用于实现基于有限状态自动机变体描述的服务应用。本文详细阐述了CARE的形式化建模、验证与测试过程。我们将其形式化为一个随机时间自动机网络模型，并利用Uppaal工具，通过穷举与统计模型检测技术对模型进行期望属性验证。从Uppaal模型生成的抽象测试用例被具体化以用于CARE测试。本研究强调了采用形式化建模、验证与测试流程对提升开源分布式应用可靠性的优势。我们讨论了应用建模的方法论以及从抽象模型生成具体测试用例的技术，并阐述了已识别与修复的问题。