NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

NASA Centers Host NASA Formal Methods Symposium 2014

Dr. Kristin Y. Rozier (Ames Intelligent Systems Division) and Dr. Julia Badger (Johnson Space Center) served as Program Committee Chairs for the sixth annual NASA Formal Methods Symposium (NFM), held April 29 - May 1, 2014, at the Gilruth Center at NASA’s Johnson Space Center (JSC) in Houston, Texas. Dr. Michael Hinchey (Goddard Space Flight Center) served as General Chair. JSC gave NFM a warm welcome, sending Steve Stich (Deputy Director of Engineering) to deliver a welcome address on the Center's behalf.

NFM is a selective, fully peer-reviewed publication venue that attracts high-quality original research. The Symposium is the result of a collaboration between formal methods researchers at six NASA centers: Ames Research Center (ARC), the Jet Propulsion Laboratory (JPL), Langley Research Center (LaRC), Goddard Space Flight Center (GSFC), Armstrong Flight Research Center (AFRC), and JSC.

NFM 2014 received 107 abstract submissions, 83 of which resulted in full papers: 50 regular papers describing fully developed work and complete results, and 33 short papers describing tools, experience reports, and descriptions of work in progress with preliminary results. Out of these, 20 regular papers and 9 short papers were accepted, giving an overall acceptance rate of 35% (a 40% rate for regular papers and a 27% rate for short papers). All submissions went through a rigorous review process, where each paper was read by at least three reviewers.

In addition to the refereed papers, the Symposium featured three invited talks and a panel feature. NASA provided a special guest talk on "NASA Future Challenges in Formal Methods," delivered by Bill McAllister (Chief, Safety and Mission Assurance, International Space Station Safety Panels, Avionics and Software Branch, JSC). Professor Lawrence C. Paulson (University of Cambridge) gave a keynote talk on "Theorem Proving and the Real Numbers: Overview and Challenges." Professor Moshe Y. Vardi (Rice University) gave a keynote talk on "Compositional Temporal Synthesis."

The NFM 2014 panel feature entitled, "Future Directions of Specifications for Formal Methods," featured panelists Matt Dwyer (University of Nebraska), Hadas Kress-Gazit (Cornell University), and Moshe Y. Vardi (Rice University). Specifications are required for all applications of formal methods, yet extracting specifications for real-life safety-critical systems often proves to be a huge bottleneck, or even an insurmountable hurdle to the application of formal methods in practice. This is the state for safety-critical systems today, and as these systems grow more complex, more pervasive, and more powerful in the future, there is not a clear path for even maintaining the bleak status quo. Therefore, NFM 2014 highlighted this issue in the home of an important critical system, the Mission Control Center of NASA's most famous critical systems, and asked our panelists where we can go from here.

NFM 2014 was attended by over a hundred formal methods researchers from around the world. Springer published the NFM Symposium proceedings as a volume in the Lecture Notes of Computer Science (LNCS) series:

http://link.springer.com/book/10.1007/978-3-319-06200-6

The international Program Committee (PC) for NFM 2014 consisted of some of the most prominent researchers in the field of formal verification. In total, the PC consisted of 44 members from NASA, academia, industry, and other government labs who were aided in completing the extensive peer reviews by 53 additional expert external reviewers. The PC included TI team members Guillaume Brat, Ewen Denney, Kristin Y. Rozier, Neha Rungta, Johann Schumann, Oksana Tkachuk, and Arnaud Venet. Additional reviewers included TI team members Ganesh Pai and Sarah Thompson. The NFM Steering Committee also included Code TI members Ewen Denney, Corina Pasareanu, and Kristin Y. Rozier.

BACKGROUND: The widespread use and increasing complexity of mission and safety-critical systems requires advanced techniques that address their specification, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission and safety-critical systems. Within NASA such systems include autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms, such as property-based design, code generation, and safety cases, are bringing with them new challenges and opportunities. The focus of the Symposium was on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems in all design lifecycle stages. We encouraged work on cross-cutting approaches marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying through system development.

The NASA Formal Methods Symposium is an annual event that was created to highlight the state-of-the-art in formal methods, both in theory and practice. The series is a spinoff of the original Langley Formal Methods Workshop (LFM). LFM was held six times in 1990, ‘92, ‘95, ‘97, 2000, and ‘08 near LaRC in Virginia. In 2009, the first NASA Formal Methods Symposium was organized by ARC at Moffett Field, CA. In 2010, the Symposium was organized by LaRC and GSFC, and held at NASA Headquarters in Washington, D.C. The third NFM Symposium was organized by the Laboratory for Reliable Software at JPL/California Institute of Technology, and held in Pasadena, CA in 2011. NFM returned to LaRC in 2012; the Symposium was organized by the LaRC Formal Methods Group in nearby Norfolk, Virginia. ARC organized and hosted NFM 2013, the fifth Symposium in the series. This year's Symposium was organized via a collaboration between GSFC, JSC, and ARC.

Topics covered by NFM 2014 include, but are not limited to: model checking; theorem proving; static analysis; model-based development; runtime monitoring; formal approaches to fault tolerance; applications of formal methods to aerospace systems; formal analysis of cyber-physical systems, including hybrid and embedded systems; formal methods in systems engineering, modeling, requirements, and specifications; requirements generation, specification debugging, formal validation of specifications; use of formal methods in safety cases; use of formal methods in human-machine interaction analysis; formal methods for parallel hardware implementations; use of formal methods in automated software engineering and testing; correct-by-design, design for verification, and property-based design techniques; techniques and algorithms for scaling formal methods, e.g., abstraction and symbolic methods, compositional techniques, and parallel and distributed techniques; and application of formal methods to emerging technologies.

TEAM: Guillaume Brat, Ewen Denney, Ganesh Pai, Corina Pasareanu, Kristin Y. Rozier, Neha Rungta, Johann Schumann, Sarah Thompson, Oksana Tkachuk, and Arnaud Venet

NASA PROGRAM FUNDING: Various (multi-center team)

Contact: Kristin Y. Rozier

First Gov logo
NASA Logo - nasa.gov