发表机构
Faculty of Informatics West University Timi s oara Romania
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种基于TLA+轨迹检查的监控工具，可从Kubernetes审计日志推断行为并检测多租户等违规，将形式化推理融入实时Kubernetes环境以提升监控与正确性检查效果。
AI 中文摘要
在分布式系统中，模型检查通常在设计阶段使用，用于构建系统的抽象模型，再穷举检查所有可能的行为。TLA+作为一种规约语言，常与TLC模型检查器搭配以这种方式使用。\n 本文提出了一种监控工具，其核心以不同方式利用TLA+规约。该工具使用TLA+轨迹检查规约，检测从Kubernetes审计日志推断出的行为中的违规情况。我们的主要用例聚焦于多租户违规，但该流程并不局限于该场景。具体而言，它展示了如何将形式化推理融入实时Kubernetes环境，以改进监控和正确性检查。
英文摘要
In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications in a different way. The tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from Kubernetes audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live Kubernetes environments to improve monitoring and correctness checking.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 51-66
