论文标题
一阶分支时间属性的双向运行时执行
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
论文作者
论文摘要
运行时执行是一种动态分析技术，它可以用系统启动监视器，以确保其正确性，如某些属性所指定的。本文探讨了描述系统输入和输出行为的属性的双向执法策略。我们为双向执行开发了一个操作框架，并使用它来研究Hennessy-Milner逻辑与递归（SHML）的安全片段的可执行性。我们提供了一种自动合成功能，该函数可从SHML公式生成正确的显示器，并表明该逻辑可通过特定类型的双向执行监视器强制执行，称为“动作禁用监视器”。
Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.
