Monthly Archives: August 2016

Prof. Kristin Yvonne Rozier Wins NASA Early Career Faculty (ECF) Award

nasa-ecf-frontpage

 

NASA’s Space Technology Mission Directorate (STMD) announced today that the proposal by Prof. Kristin Yvonne Rozier entitled “Multi-Platform, Multi-Architecture Runtime Verification of Autonomous Space Systems” was selected for funding under the call for Verification and Validation of Autonomous Systems.

According to NASA: “The Early Career Faculty (ECF) component of the Space Technology Research Grants Program awards grants to accredited U.S. universities on behalf of outstanding faculty researchers early in their careers. ECF challenges early career faculty to examine the theoretical feasibility of ideas and approaches that are critical to making science, space travel, and exploration more effective, affordable, and sustainable. Awards result from successful proposals to the ECF Appendix to the SpaceTech-REDDI NASA Research Announcement. The ECF Appendix is expected to be released at least biannually and will feature specific topics. Awards are expected to be a maximum of three years in duration and the typical award amount is $200K/year.”


kyr-revisedoverviewchart


Abstract:
Autonomous systems are only capable of effective self-governing if they can reliably sense their own faults and respond to failures and uncertain environmental conditions. We propose to design a real-time, onboard runtime verification and system health management (SHM) framework called R2U2, to continuously monitor essential system components such as sensors, software, and hardware for detection and diagnosis of failures and violations of safety or performance rules during the mission of autonomous space systems, such as rovers, small satellites, or Unmanned Aerial Systems (UAS) flying in the skies of other planets. R2U2 is multi-platform and multi-architecture to address the requirements and capabilities of these embedded systems. R2U2 stands for Responsive, Realizable, Unobtrusive Unit; it is named after its three crucial properties that are currently absent from state-of-the-art SHM capabilities. Responsiveness means evaluating system health in real time, with provable timing and performance guarantees. Realizability involves being adaptable, extensible, and scalable to multiple platforms and architectures. Unobtrusiveness requires R2U2 to operate without altering crucial properties of the system: functionality, certifiability, timing, or tolerances for size, weight, power, telemetry bandwidth, software overhead. A full-scale version of R2U2, with options for hardware- and software-based implementations would have tremendous impact on the ability of autonomous space systems to perform real-time system-level reasoning about their health.


Congratulations to the seven fellow NASA ECF Award Winners: Necmiye Ozay (University Of Michigan), Seok Woo Lee (University of Connecticut), SungWoo Nam (University of Illinois at Urbana-Champaign), Sonia Chernova (Georgia Institute of Technology), Dimitra Panagou (University Of Michigan), Daniel Szafir (University Of Colorado, Boulder), and Stefanie Tellex (Brown University).

Leave a Comment

Filed under Awards, 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.




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