Akshay Rajhans:
Robustness of Temporal Logic Specifications for Testing of Signals

Abstract: The use of temporal logic (TL) for specifications, which has traditionally been a part formal verification, is only a recent development in testing. In the case of continuous and hybrid systems where formal verification is undecidable/expensive, TL testing using Boolean abstraction of TL formulas can be a wise choice. However this Boolean abstraction is not robust and it makes test results vulnerable to parameter variations or to noise. Ideally, along with the Boolean result of a test, one would want to quantify the vulnerability to (or the robustness against) such perturbations.

The definition of this 'robustness degree' of a satisfaction of a TL specification by a signal marks the start of the contributions of this thesis. The analytical computation of this robustness degree from first principles can be expensive/not possible. We will see how the thesis defines new real-valued (also called robust) TL semantics, whose value (called 'robustness estimate') approximates the robustness degree we are looking for. To compute this robustness estimate, the thesis then proposes a monitoring algorithm and introduces a software tool aimed at facilitating this computation.

Since we are using a (discrete) computer to compute the robustness estimate of a continuous signal, we will also see the conditions and assumptions under which the robustness of a sampled version of a signal guarantees the robustness of the original continuous signal.

NOTE: This two-part presentation series titled "Robustness of temporal logic specifications" looks at some interesting contributions of the recently defended PhD thesis by Dr. Georgios Fainekos at the University of Pennsylvania. Part II of this talk will be scheduled at a later time in the near future.
Bio:
Akshay Rajhans is a PhD student in the Electrical and Computer Engineering department at Carnegie Mellon University. He received his Bachelor of Engineering degree in Electronics and Telecommunication from the University of Pune in 2003. From 2003 to 2005 he was working with the Research Development and Engineering department of Cummins India Limited, where he most recently served as a Manager of Electronic Controls. In January 2006 he joined the University of Pennsylvania, where he received his Master of Science degree in Electrical Engineering in December 2008. From January 2008 through June 2008, he was a temporary research staff under Prof. George Pappas at the General Robotics Automation Sensing and Perception (GRASP) Laboratory of the University of Pennsylvania. From July 2008 he is a PhD student at the Electrical and Computer Engineering department at Carnegie Mellon University.

Appointments: dcm@cs.cmu.edu


Maintainer Home > Seminar ]
`Last modified: Tues Aug 12 11:09:10 EDT 2008