A Dynamic Temporal Logic for Quality of Service in Choreographic Models

Autor:	Pombo, Carlos G. Lopez, Suñé, Agustín E. Martinez, Tuosto, Emilio
Rok vydání:	2023
Předmět:	Computer Science - Software Engineering 68U07 D.2.4
Druh dokumentu:	Working Paper
Popis:	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. Comment: 20 pages, Accepted for publication at International Conference on Theoretical Aspects of Computing 2023
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2311.01414 Zobrazit plný text záznamu View this record from Arxiv