VyPR2: A Framework for Runtime Verification of Python Web Services
Runtime Verification 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. Our first contribution is the VyPR runtime verification tool for single-threaded Python programs. The tool handles specifications in our, previously introduced, Control-Flow Temporal Logic (CFTL), which supports the specification of state and time constraints over runs of functions. VyPR minimally 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 the VyPR2 tool. We first describe the necessary modifications to the architecture of VyPR, and then describe our experience applying VyPR2 to a service that is critical to the physics reconstruction pipeline on the CMS Experiment at CERN.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | Monitoring and Runtime VerificationTACAS at SUN I Chair(s): Ondřej Lengál Brno University of Technology | ||
16:30 30mTalk | Specification and Efficient Monitoring Beyond STL TACAS Link to publication | ||
17:00 30mTalk | VyPR2: A Framework for Runtime Verification of Python Web Services TACAS Joshua Dawes University of Manchester and CERN, Giles Reger University of Manchester, Giovanni Franzoni , Andreas Pfeiffer , Giacomo Govi Link to publication | ||
17:30 30mTalk | Constraint-based Monitoring of Hyperproperties TACAS Link to publication |