MASc Seminar: RuSTL: Runtime Verification Framework Using Signal Temporal Logic

Thursday, April 4, 2019 2:00 pm - 2:00 pm EDT (GMT -04:00)

Candidate: Waleed Qadir Khan

Title: RuSTL: Runtime Verification Framework Using Signal Temporal Logic

Date: April 4, 2019

Time: 2:00PM

Place: EIT 3145

Supervisor(s): Fischmeister, Sebastian

Abstract:

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.