Show simple item record

dc.contributor.authorKhan, Waleed 19:02:10 (GMT) 19:02:10 (GMT)
dc.description.abstractA 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.en
dc.publisherUniversity of Waterlooen
dc.subjectSignal Temporal Logicen
dc.subjectruntime verificationen
dc.subjectruntime monitoringen
dc.subjecttemporal logicen
dc.subjectstructured English texten
dc.titleRuSTL: Runtime Verification using Signal Temporal Logicen
dc.typeMaster Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws.contributor.advisorFischmeister, Sebastian
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages