Specification of temporal properties of functions for runtime verification

Runtime verification (RV) is the process of checking whether a run of a computer system satisfies a specification. RV techniques often utilise specification languages that are (i) reasonably expressive, and (ii) relatively abstract (i.e. they operate on a level of abstraction separating them from the monitored system). Inspired by the problem of monitoring systems involved in processing data generated by the high energy physics experiments at CERN, we propose a specification language, Control-Flow Temporal Logic (CFTL), whose distinguishing characteristic is its tight coupling with the control-flow of the programs for which it is used to write specifications. The coupling admits an efficient monitoring algorithm and optimised instrumentation techniques based on static analysis.