Proceedings of the First NASA Formal Methods Symposium

摘要

NFM 2009 is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. Within NASA, for example, such systems include autonomous robots, separation assurance algorithms for aircraft, and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as code generation and safety cases are bringing with them new challenges and opportunities. The focus of the symposium is on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. The NASA Formal Methods Symposium is a new annual event intended to highlight the state of formal methods ’ art and practice. It follows the earlier Langley Formal Methods Workshop series and aims to foster collaboration between NASA researchers and engineers, as well as the wider aerospace, safety-critical and formal methods communities. The specific topics covered by NFM 2009 included but were not limited to: formal verification, including theorem proving, model checking, and static analysis; automated testing and simulation techniques; model-based development; techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and/or distributed techniques;