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.
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.
Dr. Kristin Y. Rozier (NASA ARC), in collaboration with Dr. Julia Badger (NASA JSC), served as Programme Committee chairs of the sixth annual NASA Formal Methods Symposium (NFM), held April 29 through May 1, 2014. Dr. Michael Hinchey (NASA GSFC) served as General Chair. NFM 2014 was held in the Gilruth Center at NASA JSC in Houston, Texas; 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: ARC, JPL, LaRC, JSC, GSFC, and AFRC.
NFM 2014 received 107 abstract submissions, 83 of which resulted in full papers: in total 50 regular papers describing fully developed work and complete results; and 33 short papers describing tools, experience reports, or 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 reviewing 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, NASA Johnson Space Center. Professor Lawrence C. Paulson from the University of Cambridge gave a keynote talk on “Theorem Proving and the Real Numbers: Overview and Challenges.” Professor Moshe Y. Vardi from Rice University gave a keynote talk on “Compositional Temporal Synthesis.”
The NFM 2014 panel feature, titled “Future Directions of Specifications for Formal Methods,” featured panelists Matt Dwyer of the University of Nebraska, Hadas Kress-Gazit of Cornell University, and Moshe Y. Vardi of 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 even for 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 ARC team members Guillaume Brat, Ewen Denney, Kristin Y. Rozier, Neha Rungta, Johann Schumann, Oksana Tkachuk, and Arnaud Venet. Additional reviewers included ARC team members Ganesh Pai and Sarah Thompson.
Plans are already underway for NFM 2015, which will be hosted by NASA JPL.
For more information, including the accepted papers, see the official NFM website: http://www.NASAFormalMethods.org
BACKGROUND:
The widespread use and increasing complexity of mission- and safety-critical systems require 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 life-cycle 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 carrying throughout 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 in practice. The series is a spinoff of the original Langley Formal Methods Workshop (LFM). LFM was held six times in 1990, 1992, 1995, 1997, 2000, and 2008 near NASA Langley in Virginia, USA. In 2009 the first NASA Formal Methods Symposium was organized by NASA Ames Research Center in Moffett Field, CA. In 2010, the Symposium was organized by NASA Langley Research Center and NASA Goddard Space Flight Center, and held at NASA Headquarters in Washington, D.C. The third NFM symposium was organized by the Laboratory for Reliable Software at the NASA Jet Propulsion Laboratory/California Institute of Technology, and held in Pasadena, CA in 2011. NFM returned to NASA Langley Research Center in 2012; the Symposium was organized by the NASA Langley Formal Methods Group in nearby Norfolk, Virginia. NASA Ames Research Center organized and hosted NFM 2013, the fifth Symposium in the series. This year’s Symposium was organized via a collaboration between NASA Goddard Space Flight Center, NASA Johnson Space Center, and NASA Ames Research Center.
The 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, parallel and distributed techniques; application of formal methods to emerging technologies.
