POLIMON：运行时检查乱序流上的时序属性
计算机科学中的逻辑
2024-04-25 v1
摘要
本文介绍了监控工具POLIMON，用于在运行时检查系统行为是否满足以实时逻辑MTL或其带冻结量词的扩展公式表达的规约。该工具的显著特点是POLIMON可以接收描述系统事件的消息，即使这些消息是乱序到达的。此外，由于POLIMON立即处理接收到的消息，当消息描述的系统事件导致违反规约时，它会迅速输出判定结果。这使得该工具非常适合用于验证具有不可靠信道的分布式系统在运行时的行为。
引用
@article{arxiv.2404.15723,
title = {POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime},
author = {Felix Klaedtke},
journal= {arXiv preprint arXiv:2404.15723},
year = {2024}
}