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.

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