In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for \(\omega \) -regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation.

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

Runtime Consultants

  • Dana Fisman,
  • Elina Sudit

摘要

In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for \(\omega \) -regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation.