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.
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
|