Cristian Mattarei presents at FMCAD 2015: “Comparing Different Functional Allocations in Automated Air Traffic Control Design

FMCAD 2015

FMCAD 2015

PhD candidate Cristian Mattarei gave a wonderful presentation of our work on “Comparing Different Functional Allocations in Automated Air Traffic Control Design” by Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier today at Formal Methods in Computer-Aided Design (FMCAD) 2015 at the University of Texas at Austin. Our paper stems from a fruitful collaboration with the Embedded Systems Laboratory at the Fondazione Bruno Kessler (FBK) in Trento, Italy.

The slides are available here.

FMCAD 2015

FMCAD 2015

ABSTRACT:
In the early phases of the design of safety-critical
systems, we need the ability to analyze the safety of different
design solutions, comparing how different functional allocations
impact the overall reliability of the system. To achieve this
goal, we can apply formal techniques ranging from model
checking to model-based fault-tree analysis. Using the results
of the verification and safety analysis, we can compare different
solutions and provide the domain experts with information on
the strengths and weaknesses of each solution.
In this paper, we consider NASA’s early designs and functional
allocation hypotheses for the next air traffic control system for
the United States. In particular, we consider how the allocation of
separation assurance capabilities and the required communication
between agents affects the safety of the overall system. Due
to the high level of details, we need to abstract the domain while
retaining all of the key properties of NASA’s designs. We present
the modeling approach and verification process that we adopted.
Finally, we discuss the results of the analysis when comparing
different configurations including both new, self-separating and
traditional, ground-separated aircraft.

Leave a Comment

Filed under Laboratory Collaborations, Publication Highlights, Research Talks

Aerospace Engineering and Data Science!

CEAS News features the Laboratory for Temporal Logic today with a story about Professor Kristin Yvonne Rozier and friend of the Lab, Professor Eric W. D. Rozier: “UC Power Couple Uses Data Science for Social Good.”

Data Science for Social Good, Day 1

As Faculty Fellows at the Eric and Wendy Schmidt Data Science for Social Good (DSSG) Fellowship, the Professors Rozier serve as Technical Mentors for projects aimed at using data science to make a difference.

Leave a Comment

Filed under Awards, News Features

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

NASA Group Achievement Award

The announcement featuring Dr. Rozier’s Group Achievement Award from NASA has been posted to CEAS Homepage News and University of Cincinnati news.

CEAS Welcomes NASA Award Winner, Kristin Yvonne Rozier, PhD, University of Cincinnati As one of the several new faculty members added to the UC College of Engineering and Applied Science, Kristin Yvonne Rozier continues to prove her excellence with her Group Achievement Award from NASA. Read more…

 

NASAGroupAchievementAward2014

Leave a Comment

Filed under Awards, News Features

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

Reproducibility, Correctness, and Buildability: the Three Principles for Ethical Public Dissemination of Computer Science and Engineering Research

ReproducibilityCorrectnessBuildability

Our paper has been published in IEEE Ethics 2014! This is the first collaboration with the Trustworthy Data Engineering Lab: Reproducibility, Correctness, and Buildability: the Three Principles for Ethical Public Dissemination of Computer Science and Engineering Research.

Leave a Comment

Filed under Laboratory Collaborations, Publication Highlights, Reproducibility

NASA Ames Research Center Receives Society for Women Engineers’ Above and Beyond’ Award

SWE Plaque Presentation_050814

The Society for Women Engineers (SWE) Above and Beyond Award recognizes the year’s most outstanding outreach partner institution. For the award year of 2013-2014 SWE chose NASA Ames as the recipient and asked Dr. Kristin Yvonne Rozier to accept the award on NASA Ames’ behalf at the annual SWE awards ceremony on May 4, 2014. Dr. Rozier was selected to accept the award because of her contributions to SWE, including most recently designing and running a set of workshops on mathematical logic aimed at middle school girls. The workshop utilized the logic and knowledge reasoning skills of fun and games to introduce the girls to the formal verification techniques applied to life-critical systems at NASA; the students gave it the highest rating of all of the workshops at SWE’s 2014 “Wow! That’s Engineering!” event.

The Above and Beyond Award is addressed to NASA Ames in appreciation of all of the efforts of three women engineers at this center. Dr. Rozier presented the Above and Beyond award to NASA Ames Center Director Pete Worden on May 8, 2014; the award is now on display in the awards case at the MegaBites Cafe.

Other volunteers from NASA Ames whose work contributed to the Center receiving this award include Ali Guarneros Luna, who volunteered at SWE’s ‘Designing Women’ event in 2013; and Dr. Erika Rodriguez, who serves on the Executive Committee for the SWE Santa Clara Valley section.

Leave a Comment

Filed under Awards, Outreach