Category Archives: Research Talks

Rozier Gives Invited Talk at AAAI 2023 Spring Symposium Series

On the Effectiveness of Mission-time Linear Temporal Logic (MLTL) in AI Applications

Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the temporal operators of LTL, enabling unit-agnostic specification over finite traces. It is arguably the most-used variation of MTL, and the most-used subset of STL in industrial and AI applications. MLTL optimizes the trade-off between expressibility of a wide range of realistic requirements and the ability to author generic, easy-to-validate formulas. We highlight successful AI applications centered around MLTL requirements, including Robonaut2 and the NASA Lunar Gateway Vehicle System Manager. We overview advances in analyzing MLTL, explain the motivation driving these developments, and point out the gaps in the state of the art where there are needs for future work.

https://ltlf-symposium.github.io/invited/

Leave a Comment

Filed under Research Talks

PhD Student Rohit Dureja Presents at NSF:CPS PI Workshop

PhD student Rohit Dureja presents his research, funded by NSF CAREER Award Number 1664356 “Theoretical Foundations of the UAS in the NAS Problem (Unmanned Aerial Systems in the National Air Space)” [Photo credit: Taskin Padir]

Leave a Comment

Filed under Research Talks

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.



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.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

Adding Runtime Verification without Losing Certification

Verification-Certification-Panel

 

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.


stacerboom_cropped

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


nasajpllogo

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.

jpl2016

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

An Airspace Abundant with Automation

delangex_banner20160526

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!

kyr_delangeposter

kyr_delangeposterpresentation

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

2016 NSF Cyber-Physical Systems Principal Investigators’ Meeting

PI Prof. Kristin Yvonne Rozier presented a poster on current grant “CAREER: Theoretical Foundations of the UAS in the NAS Problem (Unmanned Aerial Systems in the National Air Space)” at the 2016 NSF Cyber-Physical Systems Principal Investigators’ Meeting October 31-November 1, 2016. This seventh annual Cyber-Physical Systems (CPS) PI meeting gathered researchers and collaborators from around the world!

According to the NSF, “The CPS Principal Investigators’ Meeting provided a forum for a wide range of stakeholders in academia, industry, and Federal agencies to review new developments in CPS foundations, to identify new, emerging applications, and to discuss technology gaps and barriers. The program of the meeting included presentations about projects funded by NSF and other agencies, keynotes, panels, discussion groups, and poster & demonstration sessions.”

nsf-cps_pi-meeting_2016_poster

This year’s NSF CPS PI meeting was held at the Renaissance Arlington Capital View (RACV) Hotel located in the Crystal City Community of Arlington, Virginia at 2800 South Potomac Avenue, Arlington, Virginia 22202. The RACV is 0.9 miles from the Reagan Washington National Airport (DCA). Watching the planes land that will someday fly our research is an exciting experience!

nationalairport

Leave a Comment

Filed under Awards, Research Talks

Rohit Dureja Presents Poster at FMCAD’16

Ph.D. Student Rohit Dureja presented a poster at Formal Methods in Computer-Aided Design (FMCAD’16) on “Comparative Safety Analysis of Wireless Communication Networks in Avionics.”

student-forum


Abstract: Comparative Safety Analysis of Wireless Communication Networks in Avionics

Existing wired networks add weight and complexity to current aircraft design. To reduce weight of aircraft, it is essential to decrease the number of wired components and move them to wireless. However, migration of wired to wireless needs to be supported by a thorough analysis of the complexities and failure aspects of the two mediums. The wireless network needs to be at least as reliable and fault tolerant as the existing wired network. This paper proposes a formal framework for a comparative safety analysis of wired and wireless networks. Due to the plug-and-play nature of the framework, it is adaptable to a wide variety of network protocols. It facilitates identification of the minimum set of events that lead to system failure, and using quantified failure probabilities recommends fault tolerant mechanisms that increase system reliability. Designers can then compare candidates for wireless protocols among each other, as well as the wired network, and make informed design decisions.


poster


Slides from the presentation are available here (BibTeX).

Leave a Comment

Filed under Research Talks

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.




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.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

Layered Assurance Workshop: Prof. Kristin Yvonne Rozier Gives Keynote Talk

The Ninth Layered Assurance Workshop (LAW) brought together academic and industrial researchers to push the bleeding edge of Compositional Trustworthiness.

LAW is affiliated with the Annual Computer Security Applications Conference (ACSAC).

Layered assurance encompasses “diverse manifestations of combined assurance, including composition (of assured components), incremental certification (incremental cost for incremental change), abstraction layers (building upon assurance of lower layers), and polymorphism (common assurance of variants, such as among members of a product line).”

https://www.acsac.org/2015/workshops/law/Rozier-Keynote-LAW2015.pdf

TITLE:
Layers of Formal Verification for Full-Scale NextGen Automated Air Traffic Control

ABSTRACT:

We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that is more scalable while also proving at least as safe. Now that we have the chance to redefine air traffic control from scratch, the question arises: how do we do it safely?

We explore new frontiers in symbolic model checking to scalably answer the functional allocation question: instead of analyzing one design, or comparing a pair of designs, we now need to take into account a large number of permutations and combinations of functions that comprise a large set of possible designs. We compositionally model and comparatively analyze this set with regard to safety on multiple levels, considering the full space of possible system designs both in nominal conditions and in the presence of faults. Our analysis helps NASA narrow the possible design space, saving time and cost of later-phase evaluations, identifying both novel and known problematic design configurations. We look to the future, where a componsitional approach layering different verification techniques at multiple levels will be required to build up a safety case for the final design.

Leave a Comment

December 8, 2015 · 6:00 pm