一种用于编排模型中服务质量描述的动态时序逻辑
软件工程
2023-11-07 v3
摘要
我们提出一个利用编排模型来表达和分析消息传递系统服务质量（QoS）的框架，该模型由 g-编排（g-choreography）和通信有限状态机（CFSM）组成。我们的三个主要贡献如下：（I）对 CFSM 扩展非功能契约以规定局部计算的定量约束；（II）一种能够表达 QoS 的动态时序逻辑，即相对于规定通信协议的 g-编排来表达系统性质；（III）我们逻辑的可半判定性，其支持有界模型检测方法以验证通信系统的 QoS 性质。
引用
@article{arxiv.2311.01414,
title = {A Dynamic Temporal Logic for Quality of Service in Choreographic Models},
author = {Carlos G. Lopez Pombo and Agustín E. Martinez Suñé and Emilio Tuosto},
journal= {arXiv preprint arXiv:2311.01414},
year = {2023}
}
备注
20 pages, Accepted for publication at International Conference on Theoretical Aspects of Computing 2023