Category Archives: Research Talks

Dagstuhl Seminar: Theory and Practice of SAT Solving

Dagstuhl Seminar 15171 on the “Theory and Practice of SAT Solving” tackled one of the most fundamental computational questions: proving logic formulas. The seminar brought together the fields of SAT solving and proof complexity to explore questions of both theoretical and practical interest in designing real-world complex systems, citing examples from hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and railway signalling systems. The seminar explored this interdisciplinary space, considering questions like, “Can Proof Complexity Shed Light on Crucial SAT Solving Issues?”

Professor Kristin Yvonne Rozier contributed a seminar on “Linear Temporal Logic Satisfiability Checking,”

Abstract:
Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware. Techniques such as requirements-based design and model checking have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, logic designs, medical devices, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability.

In 2007, we 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, such as property-based system design or system verification via model checking. We demonstrated that LTL satisfiability checking reduces to model checking; an extensive experimental evaluation proved that for LTL satisfiability checking, the symbolic approach is superior to the explicit approach. However, the performance of the symbolic approach critically depends on the encoding of the formula. Since 1994, there had been essentially no new progress in encoding LTL formulas as symbolic automata for BDD-based analysis. We introduced a set of 30 symbolic automata encodings, demonstrating that a portfolio approach utilizing these encodings translates to significant, sometimes exponential, improvement over the standard encoding for symbolic LTL satisfiability checking. In recent years, LTL satisfiability checking has taken off, with others inventing exciting new methods to scale with increasingly complex systems. We revisit the benchmarks for LTL satisfiability checking that have become the de facto industry standard and examine the encoding methods that have led to leaps in performance. We highlight the past and present, and look to the future of LTL satisfiability checking, a sanity check that now has an established place in the development cycles of safety-critical systems.

Leave a Comment

Filed under Laboratory Collaborations, Research Talks

Dagstuhl Seminar Challenge: Net-Enabled Aircraft

Dagstuhl Seminar 15071 on “Formal Foundations for Networking” brought together researchers and practitioners from the fields of networking, formal methods, programming languages, and security, to investigate key questions relating to the acute need for methods and tools that can provide rigorous guarantees about the behavior, performance, reliability, and security of networked systems. This productive workshop combined talks on challenges and solutions; Prof. Kristin Yvonne Rozier issued a monumental challenge to the community in the talk “Formal Methods Challenge: Efficient Reconfigurable Cockpit Design and Fleet Operations using Software Intensive, Networked, and Wireless-Enabled Architecture (ECON)“.

ABSTRACT: We are at the dawn of a new generation of aircraft! Current aircraft are consistently built over-weight and over-budget and suffer from limitations that cannot carry forward into our increasingly digital age. In order to meet the demands placed on future aircraft, we need to design a new type of *net-enabled* aircraft by reducing aircraft weight, increasing automation and modularity, moving from hardware to software systems, moving from on-board/aircraft-based systems to cloud/fleet-based systems, and thereby facilitating easier and more responsive maintenance and system health management procedures.

For example, the wiring alone on the A-380 weighs approximately six tons, while each ton of weight in the aircraft infrastructure costs an estimated $7.2 billion in fuel across a fleet in the U.S. each year. We ask the question: can we replace some of these wires with wireless systems? Can we add wireless backup systems for wired systems that don’t currently have backups due to weight constraints? But then how do we design these new hybrid systems in a way that allows us to rigorously reason about their safety, reliability, availability, and security? For another example, can we replace heavy, customized, and therefore hard-to-maintain cockpit systems by lighter, more modular, alternatives using wireless, software, or cloud-based technologies? We have not solved the formal verification problem for current cockpits; how will we scale to net-enabled cockpits?

We must reason about an aircraft as a network of avionics sub-systems, about a fleet as a network of aircraft, and about both of these being located in the cloud. What restrictions do we need to make to enable formal verification, from design-time to runtime? Join this NASA-lead team of government, academia, and industry experts as we attempt to answer the ultimate question: how can we design and verify a new class of net-enabled aircraft that are *lighter*, *cheaper*, and *safer* than ever before?

 

Leave a Comment

Filed under Research Talks

2015 NARI LEARN/Seedling Technical Seminar

https://ac.arc.nasa.gov/p8rh8dsei1p/?launcher=false&fcsContent=true&pbMode=normal

Our team presented the final report for our 2014 Seedling grant project on Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS at the 2015 NARI LEARN/Seedling Technical Seminar. Thanks to our moderators Doug Rohn and Mike Dudley, to our technical reps Colin Theodore and Alwyn Goodloe, and to our audience for many interesting questions.

Leave a Comment

Filed under Research Talks

CMU Cyber-Physical Systems Industrial Challenge: “Integration of Formal Methods into Design and Implementation of Aerospace Systems”

The Logical Systems Laboratory at Carnegie Mellon University hosted an NSF-sponsored workshop on Cyber-Physical System Verification & Validation: Industrial Challenges & Foundations December 11-12, 2014. This productive workshop combined talks on challenges and solutions for analyzing industrial cyber-physical systems with lively panel discussions. The mixed audience included a wide range of representatives from academia and industry, from both the aerospace and automotive industries. Dr. Kristin Yvonne Rozier had the honor of giving the opening talk on “Integration of Formal Methods into Design and Implementation of Aerospace Systems,” issuing challenges compiled from years of industrial experience.


ABSTRACT: The value of formal methods in aerospace system design and verification has been demonstrated increasingly frequently, leading to more widespread acknowledgment of the essentialness of incorporating these methods into any safety-critical project. However, the success stories have mainly demonstrated the value of the results of formal methods analysis, advancing formal techniques in terms of scalability, efficiency, and adaptability to the range of complex problems in the aerospace domain. While this has gone a long way to winning over the perception of formal methods as a valuable and integral tool, it has not addressed some of the most significant bottlenecks in the process and the original barriers to adaptation. These challenges include creating a formal model and extracting formal specifications from a development process that might never before have created them. This talk will briefly survey the successes and highlight the remaining barriers to adaptation of formal methods in aerospace. Unless we address these challenges in the near future, the progress of formal methods in aerospace may be stalled.

 

Leave a Comment

Filed under Research Talks

NASA Ames Director’s Colloquium, “No More Helicopter Parenting: Intelligent, Autonomous UAS”

By special invitation of the Office of the Chief Scientist, Dr. Kristin Yvonne Rozier had the honor of kicking off NASA Ames’ premier seminar series, the Director’s Colloquium, special edition in honor of NASA Ames’ 75th Anniversary celebration! Her talk features the team’s new runtime system health management tool rt-R2U2. The video is available on the NASA Ames YouTube Channel under “Dr. Kristin Yvonne Rozier – No More Helicopter Parenting: Intelligent, Autonomous UAS.

NASAAmesDirectorsColloquiumPoster2014

Leave a Comment

June 10, 2014 · 6:00 pm

CRA-W Alum News Feature

The CRA-W Newsletter featured Dr. Rozier in their “Alum News” for the Winter-Spring 2014 edition (page 4). The goal of the Computing Research Association‘s Committee on the Status of Women in Computing Research (CRA-W) is to take positive action to increase the number of women participating in Computer Science and Engineering (CSE) research and education at all levels. Their efforts include hosting the Grad Cohort since 2004, which aims to increase the ranks of senior women in computing by building and mentoring nationwide communities of women through their graduate studies.

Dr. Rozier was a member of the 2005 Grad Cohort and returned to give the talk on “Career Life Balance” at the 2008 Grad Cohort.

Leave a Comment

Filed under News Features, Research Talks