Category Archives: Laboratory Collaborations

Computer-Assisted Engineering for Robotics and Autonomous Systems

Researchers in Computer-Assisted Engineering for Robotics and Autonomous Systems

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.

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.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

A 12 year Dormant Error found in just 1.474 seconds!

The Applied Formal Methods course featured an excellent guest talk by Dr. Yogananda Jeppu of Honeywell on February 9, 2017. For illustration purposes, Dr. Jeppu demonstrated using CBMC to analyze a flight control system with a bug in it that could be triggered by a normal sequence of actions by the pilot, and showed how a 12-year dormant error was found in just 1.4 seconds. Thanks to Yoga Jeppu for contributing yet another compelling example of how formal analysis could have easily and efficiently prevented an error that later disrupted a critical avionics system during flight.

Leave a Comment

Filed under Laboratory Collaborations

Visit to SRI

SRI Robotics continues to push the state of the art in autonomy and unmanned systems. It was wonderful to meet Gordon Kirkwood and see some of the amazing innovations in person! We are looking forward to future opportunities for collaboration.

Leave a Comment

Filed under Laboratory Collaborations

Adding Runtime Verification without Losing Certification



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.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

R2U2 at Spacecraft Flight Software Workshop and NASA JPL!

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.”

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.


Leave a Comment

Filed under Laboratory Collaborations, Research Talks

An Airspace Abundant with Automation


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!



Leave a Comment

Filed under Laboratory Collaborations, Research Talks

Patrick Moosbrugger Wins 2016 Kapsch Award


Congratulations to Ph.D. student Patrick Moosbrugger, recipient of the 2016 Kapsch Award for the best Masters thesis from the University of Applied Sciences, Technikum Wien! The Kapsch Award is given for the combination of the innovations and contributions of the MS thesis, outstanding academic performance of the student in coursework, and completing the MS degree exam with honors. Patrick was one of seven awardees across 18 MS degree programs. His MS thesis advances system health management for both safety and security requirements using R2U2.

The story is covered in several places:

Leave a Comment

Filed under Awards, Laboratory Collaborations, News Features

Theoretical Foundations of SATisfiability Solving

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.

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.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

Parallella flies with NASA (and the Laboratory for Temporal Logic)

Parallella has found our research and featured us on their website with the headline Parallella Flies with NASA!

Parallella has featured our NASA Technical Memorandum::

  • Kristin Yvonne Rozier, Johann Schumann, and Corey Ippolito. “Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS.” Technical Memorandum NASA/TM-2015-218817, May, 2015. PDF BibTeX

However, the Parallella FPGA is actually featured in several of our publications, including:

Leave a Comment

Filed under Laboratory Collaborations, News Features

Formal Methods and Data Science at the World Bank!

Professor Kristin Yvonne Rozier teamed up with Dr. Jeff Alstott of MIT and Singapore University of Technology to give a forward-looking presentation on “Company Network Analysis” for the World Bank Group’s “Teams Working on Corruption, Procurement, & Data Analysis: a ‘Hands-on Workshop’ on progress and future planning on using data to identify and address corruption in procurement” in Washington, D.C. on October 5, 2015. The presentation highlighted the analysis completed at the Data Science for Social Good (DSSG) program at the University of Chicago in the years 2014-2015 and a vision for increasing precision and effectiveness of the analysis using a formal methods solution.


Presentation on Company Network Analysis at the World Bank Group Workshop



Kristin Y. Rozier presenting a Formal Methods vision for the future of World Bank procurement efforts to better combat corruption.


Kristin Y. Rozier and Jeff Alstott answer questions on their proposed data pipeline.


Members of the teams from two years of Data Science for Social Good were reunited with their World Bank collaborators at the meeting. Presenters included Eric Rozier and Jeff Alstott from the 2014 DSSG fellowship and Emily Grace, Elissa Redmiles, and Kristin Y. Rozier from the 2015 fellowship, and long-time DSSG Research Fellow Matt Gee.


Data Scientists at the World Bank: {L->R]: Matt Gee, Betsy Wiramidjaja, Wolfgang Koehling, Jeff Alstott, Alexandra Habershon, Emily Grace, Elissa Redmiles, Eric Rozier, Kristin Y. Rozier, Mihaly Fazekas

Leave a Comment

Filed under Laboratory Collaborations, Research Talks