CPS Events
Planning via Constrained Markov Decision Processes
Abstract:
In this talk I will retrace our research journey in the area of autonomous and intelligent systems. I will then present a high-level architecture for autonomy and dive into the technical details of a planning system we have implemented to bridge the gap between mission and motion level planning. In particular, I will discuss the problem of planning in a domain where the outcome of an action is probabilistic. Such planning problems are typically solved using Markov Decision Processes (MDP). To account for realistic mission requirements, we extend the MDP planning framework by accepting behavioral goals described in Linear Temporal Logic, and by incorporating constraints on critical resources or probability of mission success. The resulting planning problem can be solved via Constrained Markov Decision Processes. I will conclude the talk with a list of challenges that we consider still open in the area of autonomy for aerospace applications including explainability and assurance.
Bio:
Dr. Pinto is a Technical Fellow at the United Technologies Research Center (UTRC). He works at the intersection of embedded system design, model-based design automation, and autonomous and intelligent systems. His current interests include architectural design for autonomous systems, knowledge representation, algorithms for high-level reasoning and decision making, safety assurance for autonomous systems, and compositional design methodologies. He is the recipient of the 2014 UTC Outstanding Achievement Award for his contributions in the area of Autonomous Rotorcraft Technology Development and Demonstration, and of the 2016 UTRC Technical Excellence Award. Dr. Pinto earned a Laurea degree in Electrical Engineering from the University of Rome “La Sapienza”, and a Ph.D. degree in Electrical Engineering and Computer Sciences from the University of California, Berkeley.
Software Exploitation: Hardware is the New Black
Abstract:
What would the world be like if software had no bugs? Software systems would be impenetrable and our data shielded from prying eyes? Not quite. In this talk, I will present evidence that reliable attacks targeting even "perfect" software are a realistic threat. Such attacks exploit properties of modern hardware to completely subvert a system, even in absence of software or configuration bugs. To substantiate this claim, I will illustrate practical attacks in real-world systems settings, such as browsers, clouds, and mobile. The implications are worrisome. Even bug-free (say formally verified) software can be successfully targeted by a relatively low-effort attacker. Moreover, state-of-the-art security defenses, which have proven useful to raise the bar against traditional software exploitation techniques, are completely ineffective against such attacks. It is time to revisit our assumptions on realistic adversarial models and investigate defenses that consider threats in the entire hardware/software stack. Pandora's box has been opened.
Bio:
Cristiano Giuffrida is a Tenured Assistant Professor in the Computer Science Department at the Vrije Universiteit Amsterdam. His research interests span across several aspects of computer systems, with a strong focus on systems security. He received a Ph.D. cum laude from the Vrije Universiteit Amsterdam under the supervision of Andy Tanenbaum in 2014. He was awarded the Roger Needham Award at EuroSys and the Dennis M. Ritchie Award at SOSP for the best PhD dissertation in Computer Systems in 2015 (Europe and worldwide). He was awarded a VENI grant (the Dutch Equivalent of a NSF CAREER Award, PhD+3) in 2017. He has served on the program committee of a number of top systems and security venues, such as SOSP, OSDI, EuroSys, S&P, CCS, NDSS, and USENIX Security.
-
Bridging the Gap Between Requirements and Model Analysis: Evaluation on Ten Cyber-Physical Challenge Problems
Abstract:
We present a framework for introducing high-level requirement specifications in the automated analysis of dataflow models. By integrating the Formal Requirements Elicitation Tool (FRET) with the CoCoSim analyzer, our framework enables the analysis of hierarchical Simulink models against requirements written in a restricted English language. More precisely, we support: automatic extraction of Simulink model information and association of high-level requirements with target model signals and components; translation of temporal logic formulas into synchronous dataflow specifications as well as Simulink monitors; and interpretation of counterexamples produced by the analysis both at the requirement and model levels. For the analysis, we use the Kind2, Zustre, and Simulink Design Verifier (SLDV) tools. The features provided by our framework are NA generic and can be used to integrate other requirements elicitation and Simulink/Lustre analysis tools. We report on lessons learned from the application of our approach to the Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.
Bio:
Anastasia Mavridou is a Computer Scientist at the Robust Software Engineering group at NASA Ames. Previously, she was a PostDoctoral Researcher at the Institute for Software Integrated Systems at Vanderbilt University. She received her PhD in 2016 from Ecole Polytechnique Fédérale de Lausanne (EPFL), Switzerland. Her research interests revolve around formal modeling and analysis of systems with a focus on correct-by-construction techniques.
Joint ECE and CPSRC Seminar:Safety-Critical Control of Dynamic Robotic Systems
Abstract:
Science fiction has long promised a world of robotic possibilities: from humanoid robots in the home, to wearable robotic devices that restore and augment human capabilities, to swarms of autonomous robotic systems forming the backbone of the cities of the future, to robots enabling exploration of the cosmos. With the goal of ultimately achieving these capabilities on robotic systems, this talk will present a unified optimization-based control framework for realizing dynamic behaviors in an efficient, provably correct and safety-critical fashion. The application of these ideas will be demonstrated experimentally on a wide variety of robotic systems, including swarms of rolling and flying robots with guaranteed collision-free behavior, bipedal and humanoid robots capable of achieving dynamic walking and running behaviors that display the hallmarks of natural human locomotion, and robotic assistive devices aimed at restoring mobility. The ideas presented will be framed in the broader context of seeking autonomy on robotic systems with the goal of getting robots into the real-world—a vision centered on combining able robotic bodies with intelligent artificial minds.
Bio:
Aaron D. Ames is the Bren Professor of Mechanical and Civil Engineering and Control and Dynamical Systems at the California Institute of Technology. He received a B.S. in Mechanical Engineering and a B.A. in Mathematics from the University of St. Thomas in 2001, and he received a M.A. in Mathematics and a Ph.D. in Electrical Engineering and Computer Sciences from UC Berkeley in 2006. Dr. Ames served as a Postdoctoral Scholar in Control and Dynamical Systems at Caltech from 2006 to 2008, and began is faculty career at Texas A&M University in 2008. Prior to joining Caltech, he was an Associate Professor in Mechanical Engineering and Electrical & Computer Engineering at the Georgia Institute of Technology. At UC Berkeley, he was the recipient of the 2005 Leon O. Chua Award for achievement in nonlinear science and the 2006 Bernard Friedman Memorial Prize in Applied Mathematics. Dr. Ames received the NSF CAREER award in 2010, and is the recipient of the 2015 Donald P. Eckman Award recognizing an outstanding young engineer in the field of automatic control. His research interests span the areas of robotics, nonlinear control and hybrid systems, with a special focus on applications to bipedal robotic walking—both formally and through experimental validation. His lab designs, builds and tests novel bipedal robots, humanoids and prostheses with the goal of achieving human-like bipedal robotic locomotion and translating these capabilities to robotic assistive devices. The application of these ideas range from increased autonomy in robots to improving the locomotion capabilities of the mobility impaired.
