Generating runtime verification specifications based on static code analysis alerts

Abstract

Runtime verification techniques verify dynamic system behavior with respect to a set of specifications. These specifications are often created manually based on system requirements and constraints. In this paper, we introduce a rule-based approach for automatically generating runtime verification specifications based on alerts that are reported by static code analysis tools. We define a set of rules to be checked for an alert type. Violations of these rules indicate either the absence or existence of an actual bug designated by the instances of that alert type. Formal verification specifications are automatically generated for each reported alert instance based on the defined rules. Then, runtime monitors are automatically synthesized and integrated to the system. These monitors report detected errors or false positive alerts during software execution. The approach is applied on two open source software systems.