We present WhyMon, a runtime monitoring tool that produces explanations as verdicts. Receiving as input a metric first-order temporal logic (MFOTL) formula and a stream prefix of time-stamped data-carrying events, WhyMon incrementally outputs explanations that describe why each variable assignment satisfies or violates the formula. The tool includes a graphical user interface that facilitates the exploration and understanding of these explanations. Additionally, it incorporates a formally verified checker that can certify the explanations. In this tool paper, we describe WhyMon’s architecture and its command line and interactive user interfaces, and demonstrate its usefulness in a case study.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts

  • Leonardo Lima,
  • Jonathan Julián Huerta y Munive,
  • Dmitriy Traytel

摘要

We present WhyMon, a runtime monitoring tool that produces explanations as verdicts. Receiving as input a metric first-order temporal logic (MFOTL) formula and a stream prefix of time-stamped data-carrying events, WhyMon incrementally outputs explanations that describe why each variable assignment satisfies or violates the formula. The tool includes a graphical user interface that facilitates the exploration and understanding of these explanations. Additionally, it incorporates a formally verified checker that can certify the explanations. In this tool paper, we describe WhyMon’s architecture and its command line and interactive user interfaces, and demonstrate its usefulness in a case study.