一句话：用 Uppaal 对 CARE 中间件做随机时间自动机建模、穷尽与统计模型检测，并自动生成具体测试用例。
CARE 是一个分布式中间件，用于运行以有限状态自动机方言描述的服务应用。本文对 CARE 进行了形式化建模、验证与测试：首先将其形式化为随机时间自动机网络，再用 Uppaal 以穷尽模型检测和统计模型检测两类技术验证若干期望性质。作者进一步从 Uppaal 模型生成抽象测试，并将其具体化为可作用于 CARE 的测试用例。论文讨论了应用建模方法以及从抽象模型生成具体测试的流程，并报告了在过程中发现并修复的问题，说明形式化建模、验证与测试能有效提升开源分布式应用的可信性。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2501-12932,
title = {Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing},
author = {Davide Basile},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:8)2026}
}