MoCheQoS: A tool for static analysis of QoS in communicating systems

Abstract

We present MoCheQoS, a bounded model checker 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 con- straint 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., monet- ary cost, execution time, memory usage) through bounded model checking with user-specified run length limits.