We present MoCheQoS , a bounded mo del che cker to statically analyse Quality of Service ( QoS ) properties of message-passing systems. The tool implements a theoretical framework for compositional analysis of QoS properties across distributed systems using QoS-extended communicating finite state machines (qCFSMs) and the dynamic temporal logic QL with choreography-indexed modalities. To achieve this, MoCheQoS integrates Z3 SMT solver for constraint verification and ChorGram for choreographic model processing. Our methodology enables systematic verification of QoS properties on measurable application-level attributes and resource consumption metrics (e.g., monetary cost, execution time, memory usage) through bounded model checking with user-specified run length limits.

Abstract We present "Image missing", a bounded "Image missing""Image missing"to statically analyse Quality of Service ( "Image missing") properties of message-passing systems. 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 applicability of "Image missing"is evaluated through case studies and experiments. A first case study is based on the AWS cloud while a second one analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of "Image missing". These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.