Runtime verification (RV) is a formal monitoring technique that uses formal specifications to create monitors. Stream runtime verification (SRV) extends RV from Boolean observations and verdicts to diverse data, allowing much richer monitors. This expressivity is challenging for developers of monitoring engines, so SRV tools end up fixing a collection of data theories for an application domain, and require significant overhead to incorporate new datatypes. Recent results allow incorporating Haskell datatypes transparently into generic SRV engines through the use of an embedded DSL, but the resulting syntax is conditioned by Haskell, every new monitor requires recompilation and error reporting is cryptic. In this paper, we introduce Mola, a generic implementation of an SRV engine that uses reflection in Haskell to implement a universal interpreter that offers data-theory extensibility and type guarantees as well as a simple syntax with useful error reports. Mola introduces the role of data-theory engineer, who easily defines datatypes for each application domain and compiles Mola  into a specialized engine. The resulting tool is then used by specification engineers who define monitors that the engine can evaluate without recompilation. Hence, Mola finally realizes the promise of SRV to provide a clean separation between datatypes and temporal engines.

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

MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs

  • Felipe Gorostiaga,
  • Martin Ceresa,
  • César Sánchez

摘要

Runtime verification (RV) is a formal monitoring technique that uses formal specifications to create monitors. Stream runtime verification (SRV) extends RV from Boolean observations and verdicts to diverse data, allowing much richer monitors. This expressivity is challenging for developers of monitoring engines, so SRV tools end up fixing a collection of data theories for an application domain, and require significant overhead to incorporate new datatypes. Recent results allow incorporating Haskell datatypes transparently into generic SRV engines through the use of an embedded DSL, but the resulting syntax is conditioned by Haskell, every new monitor requires recompilation and error reporting is cryptic. In this paper, we introduce Mola, a generic implementation of an SRV engine that uses reflection in Haskell to implement a universal interpreter that offers data-theory extensibility and type guarantees as well as a simple syntax with useful error reports. Mola introduces the role of data-theory engineer, who easily defines datatypes for each application domain and compiles Mola  into a specialized engine. The resulting tool is then used by specification engineers who define monitors that the engine can evaluate without recompilation. Hence, Mola finally realizes the promise of SRV to provide a clean separation between datatypes and temporal engines.