RuSTL: Runtime Verification using Signal Temporal Logic

Abstract

A system is classified to be a safety-critical system if its failure and/or malfunction of these devices may result in severe injuries or in extreme cases loss of human life. Such systems are all around us, examples of which include pacemakers, respiratory equipment, electrical locks, fire sprinklers and cars among many others. Runtime Verification (RV) is used to monitor the execution of such systems either while running or after execution to ensure that the system under observation does not violate any safety constraints.

RV employs formal specification languages to evaluate a real-world systems. Pnueli introduced the formal specification for Linear Temporal Logic (LTL) in 1977 for specifying propositional time properties of reactive and concurrent systems. Signal Temporal Logic (STL) is a popular extension of LTL, which analyzes dense-time real-valued signal properties with quantitative timing constraints.

In this thesis, we introduce Runtime Verification using Signal Temporal Logic (RuSTL), an offline qualitative semantic tool for monitoring STL properties. RuSTL is designed to parse any valid STL formula ’ and create a stand-alone executable monitor program, which checks the property against a given trace σ. RuSTL also take in as input structured English text and convert it into an equivalent STL formula. The application also has the capability to automatically generate diagnostic plots that help the user visually inspect the results of the monitor against a given trace.

We prove that the monitor program generated by RuSTL is sound and it terminates for any given valid STL property. Furthermore, we prove that the parsing algorithm used to create the monitor program is complete.

We evaluated RuSTL’s performance over traces collected from an autonomous self-driving vehicle. The experimental results for our RV monitor show that the execution time of the monitor grows linearly with respect to the length of the signal trace provided.