A dynamic temporal logic for quality of service in choreographic models

We propose a framework for expressing and analysing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). Our main contributions are: (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) a bounded model-checking algorithm to verify QoS property of communicating systems.