DSLs for Runtime Verification

Runtime verification (RV) allows monitoring executions of systems against formal specifications. A major challenge in increasing the capabilities and scope of formal methods stems from the tradeoff in increasing the expressiveness of the specification formalism used, while taming down the complexity of the involved algorithms and preserving the succinctness of the specifications. Limiting the focus of RV to a single execution at a time allows a great flexibility in the way RV is implemented and towards achieving these goals. We focus here on the options for implementing RV logics as external DSLs (Domain-Specific Languages), internal DSLs, and hybrid DSLs - a mix of the two. We also address the use of AI to generate monitors from natural language requirements. We survey the possibilities and focus in particular on the effect it has on achieving a desired level of expressiveness. A concrete challenge on which we focus here is allowing the use of arithmetic operations and relations on data that appear in the monitored events.