Category Archives: Research Talks

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!

The Fields Institute for Research in Mathematical Sciences hosted an invitation-only Workshop on Theoretical Foundations of SAT Solving August 15-19, 2016. This workshop explored one of the most important problems in all of mathematics and computer science: the Boolean satisfiability (SAT) problem. The workshop focused on the state-of-the-art research developments in Boolean satisfiability, the quintessential NP-complete problem. While SAT is believed to be intractable in general, researchers have contributed dramatic developments in algorithmic techniques in solving SAT during the last two decades. Modern SAT solvers can now solve large real-world instances obtained from wide-ranging applications such as hardware and software verification, electronic design automation, artificial intelligence, bioinformatics, and operations research; these advances were featured in the workshop’s seminars, available online. The workshop was organized by eight of the most prominent researchers in SAT: Vijay Ganesh – University of Waterloo (Lead Organizer); Armin Biere – Johannes Kepler University; Sam Buss – University of California, San Diego; John Franco – University of Cincinatti; Holger Hoos – University of British Columbia; Jakob Nordström – KTH, Royal Institute of Technology; Alasdair Urquhart – University of Toronto; Moshe Vardi – Rice University.

The related topic of Linear Temporal Logic Satisfiability builds on advances in SAT in many ways. Professor Kristin Yvonne Rozier contributed a talk on Linear Temporal Logic Satisfiability Checking exploring this relationship with aerospace domain examples.

---

Abstract:
One of the goals of this workshop is to identify SAT solving techniques essential to application settings. Aerospace operational concepts are often specified with timelines; we find the Boolean variables and propositional clauses of traditional propositional SAT laid out over time. Therefore, we capture these industrial requirements in Linear Temporal Logic; we must efficiently check LTL satisfiability in order to assure correctness of these requirements before we use them for further analysis, such as model checking or runtime monitoring. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability.

We have established LTL satisfiability checking as a sanity check: each system requirement, its negation, and the set of all requirements should be checked for satisfiability before being utilized for other tasks. We demonstrated that LTL satisfiability checking reduces to model checking, and developed new encodings that performed significantly, sometimes exponentially, better than was previously possible. Others then built on our work to create new stand-alone tools for LTL Satisfiability. However, the state of the art leaves many open questions for future applications of LTL satisfiability.

Slides for this presentation on Linear Temporal Logic Satisfiability Checking are available online.