MoCheQoS: Automated Analysis of Quality of Service Properties of Communicating Systems
Carlos G. Lopez Pombo, Agustín E. Martinez Suñé, Emilio Tuosto
TL;DR
MoCheQoS addresses the challenge of statically analyzing quality-of-service properties in distributed, choreographed, message-passing systems. It introduces a bounded model-checking approach built on QoS-extended CFSMs, a dynamic temporal logic $ mathcal{QL}$ indexed by global choreographies, and an aggregation framework that accumulates QoS constraints along runs, with SMT-based checking for atomic QoS constraints via real-closed-field reasoning. The tool integrates Z3 and ChorGram to realize the analysis and is evaluated through AWS cloud-inspired case studies, code-extracted systems, and synthetic scalability experiments, demonstrating effectiveness in industrial-strength scenarios. The work positions MoCheQoS as the first static analysis tool tailored for QoS properties of choreographic models, and outlines avenues for extending the framework to richer time and probabilistic aspects and to domain-specific modeling languages.
Abstract
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.