Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Computer Sciences

CPS Embedded Control

2015

Articles 1 - 7 of 7

Full-Text Articles in Computer Engineering

Attack-Resilient State Estimation In The Presence Of Noise, Miroslav Pajic, Paulo Tabuada, Insup Lee, George Pappas Dec 2015

Attack-Resilient State Estimation In The Presence Of Noise, Miroslav Pajic, Paulo Tabuada, Insup Lee, George Pappas

Departmental Papers (CIS)

We consider the problem of attack-resilient state estimation in the presence of noise. We focus on the most general model for sensor attacks where any signal can be injected via the compromised sensors. An l0-based state estimator that can be formulated as a mixed-integer linear program and its convex relaxation based on the l1 norm are presented. For both l0 and l1-based state estimators, we derive rigorous analytic bounds on the state-estimation errors. We show that the worst-case error is linear with the size of the noise, meaning that the attacker cannot exploit noise ...


Automatic Verification Of Linear Controller Software, Miroslav Pajic, Junkil Park, Insup Lee, George J. Pappas, Oleg Sokolsky Oct 2015

Automatic Verification Of Linear Controller Software, Miroslav Pajic, Junkil Park, Insup Lee, George J. Pappas, Oleg Sokolsky

Departmental Papers (CIS)

We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller’s state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller’s transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.


Robust Estimation Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, George Pappas, Insup Lee Sep 2015

Robust Estimation Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, George Pappas, Insup Lee

Departmental Papers (CIS)

This paper presents the context-aware filter, an estimation technique that incorporates context measurements, in addition to the regular continuous measurements. Context measurements provide binary information about the system’s context which is not directly encoded in the state; examples include a robot detecting a nearby building using image processing or a medical device alarming that a vital sign has exceeded a predefined threshold. These measurements can only be received from certain states and can therefore be modeled as a function of the system’s current state. We focus on two classes of functions describing the probability of context detection given ...


Robust Localization Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, Insup Lee, George Pappas Jul 2015

Robust Localization Using Context-Aware Filtering, Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, Insup Lee, George Pappas

Departmental Papers (CIS)

In this paper we develop a robot localization technique that incorporates discrete context measurements, in addition to standard continuous state measurements. Context measurements provide binary information about detected events in the robot’s environment, e.g., a building is recognized using image processing or a known radio station is received. Such measurements can only be detected from certain positions and can, therefore, be correlated with the robot’s state. We investigate two specific examples where context measurements are especially useful – an urban localization scenario where GPS measurements are not reliable as well as the capture of the RQ-170 Sentinel drone ...


Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract, Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee Jun 2015

Towards Synthesis Of Platform-Aware Attack-Resilient Control Systems: Extended Abstract, Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee

Stephanie Weirich

No abstract provided.


Verified Ros-Based Deployment Of Platform-Independent Control Systems, Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee Apr 2015

Verified Ros-Based Deployment Of Platform-Independent Control Systems, Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee

Departmental Papers (CIS)

The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always ...


Controller Synthesis For Autonomous Systems Interacting With Human Operators, Lu Feng, Clemens Wiltsche, Laura Humphrey, Ufuk Topcu Apr 2015

Controller Synthesis For Autonomous Systems Interacting With Human Operators, Lu Feng, Clemens Wiltsche, Laura Humphrey, Ufuk Topcu

Departmental Papers (CIS)

We propose an approach to synthesize control protocols for autonomous systems that account for uncertainties and imperfections in interactions with human operators. As an illustrative example, we consider a scenario involving road network surveillance by an unmanned aerial vehicle (UAV) that is controlled remotely by a human operator but also has a certain degree of autonomy. Depending on the type (i.e., probabilistic and/or nondeterministic) of knowledge about the uncertainties and imperfections in the operatorautonomy interactions, we use abstractions based on Markov decision processes and augment these models to stochastic two-player games. Our approach enables the synthesis of operator-dependent ...