Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of properties, which are used to automatically synthesise monitors. A monitor is a device that, given a sequence of events representing a system execution, returns a verdict symbolising the satisfaction or violation of the formal property. Properties that can (resp. cannot) be verified at runtime by a monitor are called monitorable and non-monitorable, respectively. In this paper, we revise the notion of monitorability from a practical perspective, where we show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties. Finally, we present the implications both from a theoretical and practical perspectives.
翻译:运行时校验是一种轻量级的正式核查技术, 用于在运行时核实正在分析的系统是否如预期的那样运作。 预期的行为通常通过属性方式正式确定, 用于自动合成监测器。 显示器是一种设备, 根据系统执行过程中的一系列事件, 返回一个表示对正式属性满意度或违反的结论。 显示器无法在运行时被监测器核查的属性分别被称为可监测性和非监测性。 在本文中, 我们从实际角度修改可监测性概念, 我们从实际角度显示如何仍然使用不可监测的属性生成部分监测器, 以部分检查属性。 最后, 我们从理论和实践角度介绍其影响。