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性质。