We present MoCheQoS, a tool to analyse quality of service (QoS) properties of message-passing systems. Building on the logic and the choreographic model we defined in recently published work, MoCheQoS implements a bounded model checking algorithm. We discuss strengths and weaknesses of MoCheQoS through some case studies.

翻译：我们提出MoCheQoS，一种用于分析消息传递系统服务质量属性的工具。基于我们在最近发表工作中定义的逻辑和编排模型，MoCheQoS实现了有界模型检测算法。我们通过若干案例研究讨论了MoCheQoS的优势与不足。