A Dynamic Temporal Logic for Quality of Service in Choreographic Models

TL;DR

This paper introduces a dynamic temporal logic framework to specify and verify Quality of Service (QoS) properties in message-passing systems modeled by choreographies and CFSMs, enabling bounded model-checking of QoS constraints.

Contribution

It extends CFSMs with non-functional contracts, develops a new logic for QoS properties, and proves semi-decidability to facilitate bounded model-checking.

Findings

Logic can express QoS properties relative to communication protocols.

The framework supports semi-decidable verification of QoS in systems.

Bounded model-checking approach is enabled for practical analysis.

Abstract

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.