Browsing by Author "Pappas, GJ"

Now showing 1 - 5 of 5

Open Access
Automatic verification of linear controller software
(2015 Proceedings of the International Conference on Embedded Software, EMSOFT 2015, 2015-11-04) Pajic, M; Park, J; Lee, I; Pappas, GJ; Sokolsky, O
© 2015 IEEE.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.
Open Access
Opportunistic Control Over Shared Wireless Channels
(IEEE Transactions on Automatic Control, 2015-12-01) Gatsis, K; Pajic, M; Ribeiro, A; Pappas, GJ
© 2015 IEEE.We consider a wireless control architecture with multiple control loops over a shared wireless medium. A scheduler observes the random channel conditions that each control system experiences over the shared medium and opportunistically selects systems to transmit at a set of non-overlapping frequencies. The transmit power of each system also adapts to channel conditions and determines the probability of successfully receiving and closing the loop. We formulate the optimal design of channel-aware scheduling and power allocation that minimize the total power consumption while meeting control performance requirements for all systems. In particular, it is required that for each control system a given Lyapunov function decreases at a specified rate in expectation over the random channel conditions. We develop an offline algorithm to find the optimal communication design, as well as an online protocol which selects scheduling and power variables based on a random observed channel sequence and converges almost surely to the optimal operating point. Simulations illustrate the power savings of our approach compared to other non-channel-aware schemes.
Open Access
Robustness of attack-resilient state estimators
(2014 ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2014, 2014-01-01) Pajic, M; Weimer, J; Bezzo, N; Tabuada, P; Sokolsky, O; Lee, Insup; Pappas, GJ
The interaction between information technology and phys ical world makes Cyber-Physical Systems (CPS) vulnerable to malicious attacks beyond the standard cyber attacks. This has motivated the need for attack-resilient state estimation. Yet, the existing state-estimators are based on the non-realistic assumption that the exact system model is known. Consequently, in this work we present a method for state estimation in presence of attacks, for systems with noise and modeling errors. When the the estimated states are used by a state-based feedback controller, we show that the attacker cannot destabilize the system by exploiting the difference between the model used for the state estimation and the real physical dynamics of the system. Furthermore, we describe how implementation issues such as jitter, latency and synchronization errors can be mapped into parameters of the state estimation procedure that describe modeling errors, and provide a bound on the state-estimation error caused by modeling errors. This enables mapping control performance requirements into real-time (i.e., timing related) specifications imposed on the underlying platform. Finally, we illustrate and experimentally evaluate this approach on an unmanned ground vehicle case-study. © 2014 IEEE.
Open Access
The wireless control network: A new approach for control over networks
(IEEE Transactions on Automatic Control, 2011-10-01) Pajic, M; Sundaram, S; Pappas, GJ; Mangharam, R
We present a method to stabilize a plant with a network of resource constrained wireless nodes. As opposed to traditional networked control schemes where the nodes simply route information to and from a dedicated controller (perhaps performing some encoding along the way), our approach treats the network itself as the controller. Specifically, we formulate a strategy for each node in the network to follow, where at each time-step, each node updates its internal state to be a linear combination of the states of the nodes in its neighborhood. We show that this causes the entire network to behave as a linear dynamical system, with sparsity constraints imposed by the network topology. We provide a numerical design procedure to determine appropriate linear combinations to be applied by each node so that the transmissions of the nodes closest to the actuators will stabilize the plant. We also show how our design procedure can be modified to maintain mean square stability under packet drops in the network, and present a distributed scheme that can handle node failures while preserving stability. We call this architecture a Wireless Control Network, and show that it introduces very low computational and communication overhead to the nodes in the network, allows the use of simple transmission scheduling algorithms, and enables compositional design (where the existing wireless control infrastructure can be easily extended to handle new plants that are brought online in the vicinity of the network). © 2011 IEEE.
Open Access
Topological conditions for in-network stabilization of dynamical systems
(IEEE Journal on Selected Areas in Communications, 2013-04-04) Pajic, M; Mangharam, R; Pappas, GJ; Sundaram, S
We study the problem of stabilizing a linear system over a wireless network using a simple in-network computation method. Specifically, we study an architecture called the Wireless Control Network (WCN), where each wireless node maintains a state, and periodically updates it as a linear combination of neighboring plant outputs and node states. This architecture has previously been shown to have low computational overhead and beneficial scheduling and compositionality properties. In this paper we characterize fundamental topological conditions to allow stabilization using such a scheme. To achieve this, we exploit the fact that the WCN scheme causes the network to act as a linear dynamical system, and analyze the coupling between the plant's dynamics and the dynamics of the network. We show that stabilizing control inputs can be computed in-network if the vertex connectivity of the network is larger than the geometric multiplicity of any unstable eigenvalue of the plant. This condition is analogous to the typical min-cut condition required in classical information dissemination problems. Furthermore, we specify equivalent topological conditions for stabilization over a wired (or point-to-point) network that employs network coding in a traditional way-as a communication mechanism between the plant's sensors and decentralized controllers at the actuators. © 1983-2012 IEEE.