CPS Events
Designing State Estimators for Safety-Critical Aerospace Positioning, Navigation and Timing Systems
Abstract
The integration of digital connectivity with physical processes in IoT environments has enabled sensors and actuators to interact with each other over the physical space. However, IoT environments have complex physical interactions between actuators and sensors that create new classes of vulnerabilities. Unfortunately, traditional IoT security measures ignore such complex physical interactions and fail to achieve sufficient breadth and fidelity to uncover these vulnerabilities, causing poor accuracy and false alarms.
We discuss an approach that is used in the design of state estimators used in safety-critical positioning, navigation, and timing systems used for aerospace applications. A key requirement in the design of these estimator is being able to demonstrate that they satisfy stringent safety standards established by certification authorities. While these standards are normally performance requirements given in stochastic terms, proving compliance with them requires a combination of analytical and experimental approaches. This presentation will discuss the challenges associated with designing these estimators. The tradeoff between safety and performance will be described and discussed in detail. As a case study, we will describe a synthetic air data estimator designed as a backup for the traditional pitot-static systems used in an Unmanned Aerial Vehicle (UAV). In closing, we describe some of the open research question associated with the application of sensing and state estimation to the design of safety-critical avionics.
Bio
Demoz Gebre-Egziabher is a professor in the Department of Aerospace Engineering and Mechanics at the University of Minnesota, Twin Cities. At the University of Minnesota, he teaches courses in aerospace systems and directs a research lab focusing on the design of multi-sensor navigation and attitude determination systems for aerospace vehicles. He is the current director of the NASA/Minnesota Space Grant Consortium. He is a Fellow of the Institute of Navigation (ION) and an associate fellow of the American Institute of Aeronautics and Astronautics (AIAA). From 1990 to 1996 he was an officer in the United States Navy where he served as a system engineer on the staff of the Naval Sea Systems Command division of naval reactors in Washington D.C. Dr. Gebre-Egziabher holds a B.S in Aerospace Engineering from the University of Arizona, a M.S in Mechanical Engineering from the George Washington University and a Ph.D. in aeronautics and astronautics from Stanford University. He is a registered professional engineer (mechanical engineering)
Compositional Safety and Security Reasoning in IoT Environments
Abstract
The integration of digital connectivity with physical processes in IoT environments has enabled sensors and actuators to interact with each other over the physical space. However, IoT environments have complex physical interactions between actuators and sensors that create new classes of vulnerabilities. Unfortunately, traditional IoT security measures ignore such complex physical interactions and fail to achieve sufficient breadth and fidelity to uncover these vulnerabilities, causing poor accuracy and false alarms.
In this talk, I will discuss our efforts in safety and security reasoning in IoT deployments through physical modeling and formal analysis. First, I will introduce our approach to discovering physical interaction vulnerabilities in IoT deployments. Our approach builds the joint physical behavior of interacting IoT apps through code and dynamic analysis. It next validates a set of new metric temporal logic policies through falsification. Second, I will demonstrate how attackers can evade existing IoT defenses by exploiting complex physical relations between actuators and sensors. I will next introduce software patching and sensor placement to make the existing defenses robust against evasion attacks. Through these efforts, we create holistic physical models toward achieving the compositional safety and security of an IoT system.
Bio
Muslum Ozgur Ozmen is currently pursuing a Ph.D. degree in the Department of Computer Science at Purdue University, where he is advised by Professor Z. Berkay Celik. Prior to joining Purdue, Ozgur earned his Master of Science degree in computer science from Oregon State University, USA, and his Bachelor‘s degree in electrical and electronics engineering from Bilkent University, Turkey. His research interests broadly lie in the area of systems security. Through systems design and formal verification, his research seeks to improve security and privacy guarantees in emerging computing platforms. His research approach is best illustrated by his work in IoT safety and security. He expects to earn his Ph.D. in the Spring of 2024. More information can be obtained at https://ozgurozmen.github.io/.
Runtime Verification with Copilot and Ogma
Abstract
Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: Copilot 3, a stream-based runtime verification language for real-time embedded systems, and NASA's Ogma, a tool to transform high-level specifications into Copilot monitors. When used in combination, the toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware. Apart from generating standalone monitors, our tools generate self-contained units ready to be integrated in NASA Core Flight System cFS and Robot Operating System (ROS2) applications.
Bio
Dr. Ivan Perez is a senior research scientist contractor at NASA Ames Research Center, and has been a member of the NASA Formal Methods Group since 2018. Dr Perez investigates the application of formal methods to problems in aerospace, with particular focus on runtime verification of unmanned aerial vehicles. Prior to joining NASA, Dr. Perez founded and led Keera Studios, the first mobile Haskell game programming company in the world, and Cubilabs.com, a functional programming company focused on business applications. Over the last two decades, Dr. Perez has also worked as a programmer and researcher for the High Performance Computing Center (Germany), IMDEA Software (Spain), the Technical University of Madrid (Spain), and the University of Twente (Netherlands), as well as for multiple functional programming companies. Dr. Perez completed his PhD in Computer Science at the University of Nottingham (UK), which focused on testing and functional programming applied to games and user interfaces. He also holds a Master's Degree in Computational Logic and a Degree of Engineer in Computer Science, both from the Technical University of Madrid.
Real-time Motion Planning and Predictive Control by Mixed-integer Programming for Autonomous Vehicles
Abstract
A lot of progress has been made in the development of computational algorithms and software tools for optimization-based motion planning and control of (semi-)autonomous systems. There exist many efficient convex quadratic programming (QP) algorithms for model predictive control (MPC) of linear or linearized systems, as well as sequential convex programming (SCP) algorithms for MPC of smooth nonlinear systems. Motivated by these successes, a relatively new trend in the control community relates to the development and application of mixed-integer programming (MIP) for real-time motion planning and decision making, including both continuous and discrete variables. In this talk, I present some recent work on a tailored branch-and-bound method for real-time motion planning and decision making on embedded processing units. In addition, I will discuss two applications related to automated driving and traffic control.
Bio
Rien Quirynen received the Bachelor’s degree in computer science and electrical engineering and the Master’s degree in mathematical engineering from KU Leuven, Belgium. He received a four-year Ph.D. Scholarship from the Research Foundation–Flanders (FWO) in 2012-2016, and the joint Ph.D. degree from KU Leuven, Belgium and the University of Freiburg, Germany. Since the start of 2017, Dr. Quirynen joined Mitsubishi Electric Research Laboratories (MERL) in Cambridge, MA, USA, where he is currently a principal research scientist. His research focuses mainly on numerical optimization algorithms for decision making, motion planning and control of autonomous systems.
Measuring and enhancing network resilience; performance metrics and defense strategies
Abstract
Resilience, understood as the ability of a network to carry out its goals under adversarial attacks and unexpected failures, is critical for autonomy. Despite important advances in the design of distributed coordination and decision-making algorithms, multi-agent networks have proven fragile to targeted attacks. Novel theories and tools are therefore needed to guarantee resiliency of these systems, being the development of notions and techniques that characterize network resilience critical. However, obtaining such characterizations is difficult as resilience and performance are a complex function of the network’s and adversary’s capabilities, knowledge, resources, and the network interconnection structure. At the same time, we also need novel design methodologies that can protect multi-agent networks and adaptively manage their interconnection over time to achieve performance guarantees. In this talk, we present our recent progress in these directions.
Bio
Sonia Martínez is a Full Professor at the Department of Mechanical and Aerospace Engineering at the University of California, San Diego and a Jacobs Faculty Scholar. Prof. Martínez received her Ph.D. degree in Engineering Mathematics from the Universidad Carlos III de Madrid, Spain, in May 2002. Following a year as a Visiting Assistant Professor of Applied Mathematics at the Technical University of Catalonia, Spain, she obtained a Postdoctoral Fulbright Fellowship and held appointments at the Coordinated Science Laboratory of the University of Illinois, Urbana-Champaign during 2004, and at the Center for Control, Dynamical systems and Computation (CCDC) of the University of California, Santa Barbara during 2005. From January 2006 to June 2010, she was an Assistant Professor with the department of Mechanical and Aerospace Engineering at the University of California, San Diego. From July 2010 to June 2014, she was an Associate Professor with the department of Mechanical and Aerospace Engineering at the University of California, San Diego. Dr Martínez' research interests include networked control systems, multi-agent systems, and nonlinear control theory with applications to robotics, cyber-physical systems, and natural/social networks. In particular, she has focused on the modeling and control of robotic sensor networks, the development of distributed coordination algorithms for groups of autonomous vehicles, and the geometric control of mechanical systems. For her work on the control of underactuated mechanical systems she received the Best Student Paper award at the 2002 IEEE Conference on Decision and Control. She was the recipient of a NSF CAREER Award in 2007. For the co-authored papers "Motion coordination with Distributed Information," and "Tutorial on dynamic average consensus: The problem, its applications, and the algorithms", she received respectively the 2008 and 2021 Control Systems Magazine Outstanding Paper Award. She is a Senior Editor of Automatica and an IEEE Fellow. Recently, she was named the inaugural Editor in Chief of a new Control System Society publication, the IEEE Open Journal of Control Systems (IEEE OJCS).
