Checking Complex Source Code-Level Constraints using Runtime Verification

Runtime Verification (RV) is the process of taking a trace, representing an execution of some computational system, and checking it for satisfaction of some specification, written in a specification language.RV approaches are often aimed at being used as part of software development processes.In this case, engineers might maintain a set of specifications that capture properties concerning their source code's behaviour at runtime.To be used in such a setting, an RV approach must provide a specification language that is practical for engineers to use regularly, along with an efficient monitoring algorithm that enables program executions to be checked quickly.This work develops an RV approach that has been adopted by two industry partners.In particular, we take a source code fragment of an existing specification language, Source Code and Signal Logic, which enables properties of interest to our partners to be captured easily, and develop 1) a new semantics for the fragment, 2) an instrumentation approach, and 3) a monitoring procedure for it.We show that our monitoring procedure scales to program execution traces containing up to one million events, and describe initial applications of our prototype framework (that implements our instrumentation and monitoring procedures) by the partners themselves. CCS CONCEPTS• Software and its engineering → Formal software verification; • Theory of computation → Modal and temporal logics.