Automated Static Analysis of Quality of Service Properties of Communicating Systems

We present , a bounded to statically analyse Quality of Service ( ) 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 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 . These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.