Research

In this project, we developed a probabilistic framework that employs tools from statistical analysis to detect sensor attacks on UAS. Since UAS are highly coupled nonlinear systems with an uncertain operational environment characterized by disturbances like sensor noise, wind gusts, and atmospheric turbulence, a major hurdle in detecting malicious attacks on UAS is to be able to distinguish between the response of the UAS to usual disturbances and the response due to malicious attacks. The proposed framework consists of a layered approach, where attack indicators at each layer are identified and then used as evidences in a Bayesian network to detect a sensor attack. By explicitly incorporating knowledge about the UAS dynamics, the framework is designed to have a low false alarm rate, which is a major challenge for UAS operating in dynamic environments. The effectiveness of the framework was demonstrated through a case study involving detection of a spoofing attack on the GPS of a fixed-wing UAS.

Civilian UAS, in general, do not have redundant actuators, so an attack on even one of the actuators could be catastrophic, resulting in loss of control. To that end, in this work, we identified the security vulnerabilities of existing UAS actuators and proposed three different methods of differing complexity and effectiveness to detect and mitigate the security threats. The first two methods involve developing algorithms for detection of actuator attacks and do not require any hardware modifications. However, a separate mitigation strategy is required to ensure safe operation of the UAS in the event of an attack. In the first method, judiciously designed excitation signals are superimposed on the control commands to increase the detectability of the attack. The second method involves the use of an unknown input observer, which in addition to detecting the attack, also estimates the magnitude of the attack. The third method focuses on identifying the vulnerabilities of the existing actuators and using that information to design actuators that are resilient to malicious attacks, thereby obviating the need for a separate mitigation strategy.

The common approach to verifying that a CPS satisfies some desired global safety property is to perform complete system-level simulation and/or testing. The analyst faces the challenge of evaluating the system for all possible inputs and operational scenarios, which can be prohibitive for a complex CPS such as UAS. Therefore, it is desirable to minimize the use of simulation/testing in the verification process. To that end, in this project, tools from formal methods such as compositional verification are used to design an unmanned multi-aircraft system that is deployed in a geofencing application, where the design objective is to guarantee a critical global system property. Verifying such a property for the multi-aircraft system using monolithic (system-level) verification techniques is a challenging task due to the complexity of the components and the interactions among them. To overcome these challenges, we design the components of the multi-aircraft system to have a modular architecture, thereby enabling the use of component-based reasoning to simplify the task of verifying the global system property. For component properties that can be mathematically verified, we employ results from Euclidean geometry and formal methods to prove those properties. For properties that are difficult to be mathematically verified, we rely on Monte Carlo simulations. We demonstrate how compositional reasoning is effective in reducing the use of simulations/tests needed in the verification process, thereby increasing the reliability of the unmanned multi-aircraft system.

In this project, we developed a formally-verified distributed connectivity maintenance algorithm for an unmanned underwater vehicle (UUV) network, where the agents interact using the time-division multiple-access protocol. Due to the communication constraints imposed by the protocol, the agents do not have access to the current positions of their neighbors. This presents a significant challenge in developing a connectivity maintenance algorithm that can be formally verified. Using only local information from a UUV’s neighbors, the proposed algorithm provides motion constraints for the UUVs in the network, which can then be used by each UUV’s motion planner to plan a connectivity-preserving trajectory. Under suitable assumptions on each UUV’s motion planner and controller, we provided formal proofs that establish network connectivity for the algorithm. The formal proofs were carried out using the KeYmaera X theorem prover, which is an interactive formal verification tool for hybrid systems. This work also highlights the utility of formal verification tools in identifying scenarios that could be overlooked when employing proofs that are not carried out in a formal system for complex distributed algorithms such as the one considered. 

One of the challenges associated with UAS in general and autonomous UAS in particular is operating effectively in the presence of significant environmental disturbances, such as steady wind and turbulence. The performance guarantees against plant uncertainties and exogenous disturbances provided by robust controllers make them an appropriate choice for application to path-following control of UAS. In this project, we employ the robust Hinfinity control approach to design, analyze, and flight test different path-following robust controllers for a small fixed-wing UAS that enable it to follow arbitrary planar curvature-bounded paths under significant disturbances such as sensor noise, wind, and turbulence. A linear-parameter varying path-following controller designed using a lumped system model, which combines the virtual-vehicle-based path-following dynamics and the standard 6-DOF UAS equations of motion, was shown to yield improved performance for a wide array of geometric paths. Through extensive simulations and flight tests, the path-following controllers were shown to be sufficiently robust to sensor noise, disturbances, time delays, and modeling inaccuracies.

It is conceivable that a multi-agent CPS, such as a UAS network, would be required to switch missions, which may be triggered by environmental factors, direct commands, or situational awareness. During the switching process, the multi-agent system experiences a transient behavior that could adversely affect the mission performance. At the time of switching, the soon-to-be-active controller has to deal with a bounded, uncertain initial (error) state of the network, which lies in some ellipsoid and has to do with the previous mission operation. In this work, we proposed an approach wherein this uncertainty in the initial state is incorporated into the control design process to design a distributed controller, which would successfully recover the system from this initial state and ultimately force the network to exhibit the new desired behavior without adversely affecting the mission performance. We applied the control approach to a formation tracking problem involving a network of three fixed-wing UAS, wherein we demonstrated that the distributed controller thus designed improves the transient response of the UAS network when switching between different trajectories.

Oftentimes, control design involves the laborious task of tuning the penalty weights of the controller manually, which could be a very time-consuming process. To overcome this hurdle, along with our collaborators, we showed how a tool that utilizes integral quadratic constraint (IQC) theory to perform robustness analysis could be used to automatically tune the penalty weights of an LPV path-following controller for an autonomous underwater vehicle (AUV). The LPV controller was designed to provide guaranteed performance for any planar path whose inverse radius of curvature is bounded. Such a flexibility provided by the LPV controller offers significant advantages in AUV missions such as seabed mapping and mine countermeasures. Through IQC analysis and simulations, the LPV controller thus designed was shown to be robust in the presence of hydrodynamic uncertainties, unmodeled servo dynamics, neglected nonlinear dynamics, and sensor noise.