Runtime Verification (RV) is the process of checking whether a run of a system holds a given property. In order to perform such a check online, the algorithm used to monitor the property must induce minimal overhead. This paper focuses on two areas: Python programs and web services.

Our first contribution is the VyPR runtime verification tool for single-threaded Python programs. The tool handles specifications in Control-Flow Temporal Logic (CFTL), which supports specification of state and time constraints over runs of functions. VyPR minimally (in terms of reachability) instruments the input program with respect to a CFTL specification and then uses instrumentation information to optimise the monitoring algorithm.

Our second contribution is the lifting of VyPR to the web service setting, resulting in VyPR2. We first describe the necessary modifications to VyPR’s architecture, and then describe our experience applying VyPR2 to a service that is critical to the physics reconstruction pipeline on the CMS Experiment at CERN.