Candidate: Waleed Qadir Khan
Title: RuSTL: Runtime Verification Framework Using Signal Temporal Logic
Date: April 4, 2019
Place: EIT 3145
Supervisor(s): Fischmeister, Sebastian
Runtime Verification (RV) is used to monitor the execution of a running system either offline or online. Safety-critical device area part of our everyday lives whose failure and/or malfunction may result in severe injuries or in extreme cases loss of human life. Over the years many extensions of Temporal Logic (TL) have been developed to perform RV on hybrid-systems. Signal Temporal Logic (STL) is a popular extension of Linear Temporal Logic (LTL), which analyzes dense-time real-valued signal properties with quantitative timing constraints.
In this thesis, we introduce Runtime Verification Framework using STL (RuSTL), an offline qualitative semantic tool for
monitoring STL properties. RuSTL is designed to parse any valid STL formula and creates a stand-alone executable script which
checks the property against a given trace . RuSTL can also take as input structured English text and convert it into an STL formula. RuSTL can automatically generate diagnostic plots that help the user visually inspect the results of the monitor.
We prove that the output generated by RuSTL is sound and it terminates. Along with that, we prove that the parsing algorithm used to create the executable script 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.
200 University Avenue West
Kitchener, ON N2L 3G1