Monday October 29 4:00 - 4:50 PM Kelley 1001
Guillaume Brat Automated Software Engineering Group NASA Ames Research Center A Future Look at Software Verification & Validation at NASA In the past decade, design and coding errors in software have cost NASA the loss of several missions (MCO, MPL) or crippled others (MPF, MER) for some period of time preventing NASA from accomplishing important scientific goals. As NASA is trying to implement the President's vision for space exploration (humans will first go back to the Moon before going to Mars), there is a realization that software should be verified and validated more carefully. In this talk, I will describe how the Robust Software Engineering group at NASA Ames Research Center is trying to address this problem. I will summarize the on-going efforts in model checking, compositional verification and advanced testing for both traditional embedded systems (e.g., Guidance, Navigation, and Control systems) and autonomous systems (e.g., planning and scheduling). I will also take a closer look at our efforts in static code analysis and how we implemented a static analyzer for C based on the theory of abstract interpretation. I will also describe how we applied it to the verification of the flight software family for the Mars missions (MPF, DS-1, MER). Biography: Dr. Brat received his M.Sc. and Ph.D. in Electrical & Computer Engineering in 1998 (The University of Texas at Austin, USA). His thesis defined a (max,+) algebra to model and evaluate non-stationary, periodic timed discrete event systems. Since then, he has focused on the application of static analysis to software verification. In June 1999, he joined the Automated Software Engineering group at the NASA Ames Research Center and focused on the application of static analysis to the verification of large software systems. He co-developed and applied static analysis tools based on abstract interpretation to the verification of software for several NASA missions. He leads the formal method task in the ETDP Reliable Software Engineering project as well as the Verification and Validation task in the ETDP A4O project. He also leads the RSE group at RIACS, a division of USRA.
_______________________________________________ Colloquium mailing list [email protected] https://secure.engr.oregonstate.edu/mailman/listinfo/colloquium
