异步系统的分布式监控
On distributed monitoring of asynchronous systems
摘要：
分布式系统是出了名的难以理解和分析，以维护其正确w.r.t.给定属性。一旦活动实体（对等体、代理、进程等）以异步方式运行，它们通常会表现出大量不同的行为。这样的系统的模型化已经是一项重要的任务，更不用说它们的形式化验证了。本文的目的是讨论一个简单的模型的有限状态分布式自动机的分布式监控问题的基础上共享的行动，称为异步自动机。监视是一个与运行时验证相关的问题：假设我们必须针对未知或非常复杂的系统$A$检查属性$L$，因此经典的静态分析是不可能的。因此，使用监视器而不是模型检查，它在运行时检查底层系统的属性。我们在这里感兴趣的是监视异步自动机建模的分布式系统。要求监视器与底层系统属于同一类型是很自然的，因此我们在这里考虑分布式监视。分布式监视器不具有系统的全局视图，因此我们提出了局部可监视跟踪语言的概念。我们的主要结果表明，如果分布式字母表的行动是连接的，如果$L$是一个集的无限迹，使$L$和它的补充$L^c$是可数的联合的局部安全语言，那么$L$是局部监测。我们还表明，在无限的痕迹，可识别可数工会的局部安全的语言正是确定性语言的补充。
英文摘要：
Distributed systems are notoriously difficult to understand and analyze in order to assert their correction w.r.t. given properties. They often exhibit a huge number of different behaviors, as soon as the active entities (peers, agents, processes, etc) behave in an asynchronous manner. Already the modelization of such systems is a non-trivial task, let alone their formal verification. The purpose of this paper is to discuss the problem of distributed monitoring on a simple model of finite-state distributed automata based on shared actions, called asynchronous automata. Monitoring is a question related to runtime verification: assume that we have to check a property $L$ against an unknown or very complex system $A$, so that classical static analysis is not possible. Therefore instead of model-checking a monitor is used, that checks the property on the underlying system at runtime. We are interested here in monitoring distributed systems modeled as asynchronous automata. It is natural to require that monitors should be of the same kind as the underlying system, so we consider here distributed monitoring. A distributed monitor does not have a global view of the system, therefore we propose the notion of locally monitorable trace language. Our main result shows that if the distributed alphabet of actions is connected and if $L$ is a set of infinite traces such that both $L$ and its complement $L^c$ are countable unions of locally safety languages, then $L$ is locally monitorable. We also show that over infinite traces, recognizable countable unions of locally safety languages are precisely the complements of deterministic languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
