Search for: All records

We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (I-STL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the min and max functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to I-STL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate I-STL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates. 

Certain Android applications, such as but not limited to malware, conceal their presence from the user, exhibiting a self-hiding behavior. Consequently, these apps put the user's security and privacy at risk by performing tasks without the user's awareness. Static analysis has been used to analyze apps for self-hiding behavior, but this approach is prone to false positives and suffers from code obfuscation. This research proposes a set of three tools utilizing a dynamic analysis method of detecting self-hiding behavior of an app in the home, installed, and running application lists on an Android emulator. Our approach proves both highly accurate and efficient, providing tools usable by the Android marketplace for enhanced security screening.