We present MoCheQoS, a bounded model checker to analyse (QoS) properties of message-passing systems. Building on the dynamic temporal logic, the choreographic model, and the bounded model checking algorithm defined in our ICTAC 2023 paper, MoCheQoS enables the static analysis of QoS properties of systems built out from the composition of services. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics for example those relating monetary cost to memory usage. The implementation of the tool is accompanied by an experimental evaluation. More precisely, we present two case studies meant to evaluate the applicability of MoCheQoS; the first is based on the AWS cloud while the second analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of MoCheQoS. These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.

翻译：本文提出MoCheQoS，一种用于分析消息传递系统服务质量（QoS）属性的有界模型检测器。该工具基于我们在ICTAC 2023论文中定义的动态时序逻辑、编排模型及有界模型检测算法，能够对通过服务组合构建的系统进行QoS属性的静态分析。我们关注可度量的应用层属性及资源消耗指标（例如将货币成本与内存使用相关联的指标）上的QoS属性。工具实现附有实验评估，具体包括两个用于验证MoCheQoS适用性的案例研究：第一个基于AWS云平台，第二个分析从代码自动提取的通信系统。此外，我们通过合成生成的实验评估了MoCheQoS的可扩展性。实验表明，我们的模型能够准确捕获并有效分析工业级场景中的QoS属性。