We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic temporal logic capable of expressing QoS, properties of systems relative to the g-choreography that specifies the communication protocol, (III) the semi-decidability of our logic which enables a bounded model-checking approach to verify QoS property of communicating systems.

翻译：我们提出了一种框架，用于表达和分析消息传递系统的服务质量（QoS），该框架采用由g-编舞和通信有限状态机（CFSMs）组成的编舞模型。我们的主要贡献包括以下三点：（I）扩展CFSMs以包含非功能契约，用于指定本地计算的定量约束；（II）一种能够表达QoS的动态时序逻辑，该逻辑相对于指定通信协议的g-编舞来表达系统属性；（III）我们逻辑的半可判定性，它使得能够采用有界模型检测方法来验证通信系统的QoS属性。