An Operational Guide to Monitorability
SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2019)(2019)
摘要
Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy-Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Hence our work gives a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络