Category Archives: Laboratory Collaborations

Dagstuhl Seminar 17071 on “Computer-Assisted Engineering for Robotics and Autonomous Systems” combined the research communities of formal methods, robotics, and autonomous systems, such as Unmanned Aerial Systems (UAS), automated control systems, and rovers. The seminar combined foundational talks, formal methods techniques, industrial needs for enabling development of autonomous systems, challenge problems, and many discussions between the research communities.

From the seminar description, “In the absence of external control, it is highly important to make sure that autonomous systems are functionally safe. The more critical system safety is, the more important is to introduce standardized certifications to assure their correct functioning. However, though autonomous systems are increasingly involved in our everyday life, both exact formalizations of safe functionality (standards, what we want to be confident in), and methods to achieve confidence (methodologies, how we get confident in the properties we want to assure) are still scarce and not well integrated.

To move towards the initiation of such standards and the development of such technologies, in this seminar we want to discuss at an abstract level (1) what are general safety requirements for autonomous systems, (2) what are potential key technologies that could be employed to assure that those safety requirements hold, and (3) what are the obstacles on the way to the application of those technologies.”

The seminar was organized by Erika Abraham (RWTH Aachen, DE),
Hadas Kress-Gazit (Cornell University – Ithaca, US),
Lorenzo Natale (Italian Institute of Technology – Genova, IT), and
Armando Tacchella (University of Genova, IT). Slides from the talks, a seminar report, and notes from the presentations are all available online.

Professor Kristin Yvonne Rozier contributed a foundational talk on “Specification: the Biggest Bottleneck in Formal Methods and Autonomy.” The content of the talk was largely based on the VSTTE paper of the same name.

---

Abstract:
Advancement of autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. An aircraft cannot operate autonomously unless it has design-time reasoning to ensure correct operation of the autopilot and runtime reasoning to ensure system health management, or the ability to detect and respond to off-nominal situations. Formal methods are highly dependent on the specifications over which they reason; there is no escaping the “garbage in, garbage out” reality. Specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of autonomous systems.

We examine the outlook for formal specification, and highlight the on-going challenges of specification, from design-time to runtime. We exemplify these challenges for specifications in Linear Temporal Logic (LTL) though the focus is not limited to that specification language. We pose challenge questions for specification that will shape both the future of formal methods, and our ability to more automatically verify and validate autonomous systems of greater variety and scale. We call for further research into LTL Genesis.

 

Software Challenges in Aerospace at AIAA SciTech 2017 featured a panel on “Verification versus Certification for Software Intense Systems” on January 9, 2017. The panel consisted of Ella Atkins (University of Michigan), Natasha Neogi (NASA Headquarters), Andre Platzer (CMU), and Kristin Yvonne Rozier (ISU). The panel was chaired by Misty Davies (NASA Ames), and Christoph Torens (DLR).

The Laboratory for Temporal Logic is particularly concerned with both design time verification to enable certification and “Adding Runtime Verification without Losing Certification,” which was the topic of the presentation by Prof. Kristin Yvonne Rozier. Today, there is a big push to quickly deploy many new types of small and cheap systems, including UAS, small satellites, helper technologies like software to suggest conflict resolutions to air traffic controllers, and automated co-pilot procedures in aircraft cockpits. Also, rovers on Earth may be small and cheap, or even disposable such as if they are meant to be deployed to hazardous environments unsafe for humans. These (semi-) autonomous systems require verification but are often composed of COTS or similarly already-certified components, eliminating the opportunity to utilize design-time verification as an enabler to certification. Also, the nature of the missions of small and cheap systems like these may not be amenable to full formal verification due to limited time, limited cost, and their expendability. Therefore, it is important to ask how do we verify an certify small and cheap systems? How are verification and certification different for autonomous systems? And how can verification enable, or at least not hinder, certification? This talk proposed some ideas for addressing these questions via the R2U2 framework and pointed to important areas for future research.

R2U2, the Realizable, Responsive, Unobtrusive Unit for on-board system and software health management was featured in two presentations this week.

---

At the Spacecraft Flight Software Workshop (FSW’16), Prof. Kristin Yvonne Rozier delivered a talk on “R2U2 in Space: System and Software Health Management for Small Satellites.”

Abstract:
In order for small but complex systems like rovers, SmallSats, or Unmanned Aircraft (UAS) to operate autonomously, they must have a real-time solution for assessing their own system health. System ans Software Health Management (SHM) enables better detection of faulty sensors and software problems, and enables better fault management including mitigation of unpredicted fault scenarios in the absence of a human on-board. In recent work, we have developed a Responsive, Realizable, Unobtrusive Unit (R2U2) for on-board SHM of autonomous UAS and demonstrated its ability to detect faults during flight time. These faults, from sensor failures, to software problems, to malicious security attacks, can present as transient temporal faults that even humans are challenged to find. An R2U2 configuration is a modular combination of multiple types of temporal logic runtime observers with fault-specific Bayesian Nets and sensor filters. R2U2 reasons about both on-board hardware and software components; R2U2 itself can be instantiated as an independent FPGA-based configuration or as a software component running independently from other software on-board.

Small satellites, such as CubeSats, also require on-board SHM and failure mitigation, as limited telemetry bandwidth does not allow the transmission of the entire system state for ground-based health management. However, the autonomous operation of satellites brings a set of challenges different from UAS, including the effects of radiation on non-rad-hard, low-cost components, and the harsher environment of space. We surmise that a new extension of R2U2 could be adapted to help better detect, for example, radiation errors in cheaper COTS (not rad-hard) components often used in small space systems. Since small satellites often operate in coordination, we will also examine new ways of distributed monitoring of their communication and cooperation and real-time detection of off-nominal situations utilizing multiple satellites. This talk will discuss preliminary work and ideas for building on terrestrial success of system and software health management for the harsher, and differently challenging, environment of space.

NASA Jet Propulsion Laboratory, in conjunction with The Aerospace Corporation and The Johns Hopkins University Applied Physics Laboratory, hosted FSW’16 at the Beckman Institute Auditorium, California Institute Technology, December 12-15, 2016. The workshop featured a LiveStream YouTube Channel where videos of all sessions can be viewed online.

Workshop Background:
“With the advent of faster processors and advanced hardware architectures, the modern spacecraft is highly reliant upon flight software for mission success. Software is integral to most of the spacecraft subsystems ranging from power to propulsion to instrument operations. Additionally, spacecraft developers are moving beyond providing only infrastructure to creating applications that can revolutionize how these vehicles are operated and how data is processed on-board. This workshop provides an opportunity to present current flight architectures, novel approaches to mission solutions, and techniques for flight software development, integration, test and verification in an informal and open setting that facilitates communication across organizations and agencies.”

---

On December 16, the NASA JPL Mobility and Robotics Section Seminar talk was “R2U2: Formal System Health Management for Autonomous Systems,” delivered by Prof. Kristin Yvonne Rozier, hosted by Dr. Amir Rahmani.

A survey poster on the research from the Laboratory for Temporal Logic De Lange Conference X on “Humans, Machines, and the Future of Work” showcased many of the lab’s current projects. The poster, titled “An Airspace Abundant with Automation” features current research on automated air traffic control for both manned and unmanned aircraft, intelligent sensor fusion for automated reasoning, system health management for Unmanned Aerial Systems (UAS) and beyond, and the formal techniques required for verification required for enabling autonomy of these safety-critical systems. Thanks to all of the students and collaborators of the Laboratory for Temporal Logic for your contributions!