Where Formal Methods Might Find Application on Future NASA Missions
In many cases, formal methods are a solution looking for a problem. NASA recently released the 2015 NASA Technology Roadmaps that describe numerous possible future missions. Within these descriptions are capabilities that need to be matured in order for mission success. Many of these future capabilities could be accomplished through the use of formal methods. The future capabilities identified by NASA in these roadmaps may just be the problems formal methods have been seeking. Think of these roadmaps as “on-ramps” for engineering using formal methods.
These missions include joint robotic and human exploration of Mars, robotic probes of the icy moons of the outer planets where there is evidence of organic chemistry. Sophisticated earth-orbiting satellites to advance earth science, and possible robotic refueling and maintenance missions of these satellites.
One of the predominant cross-cutting challenges is autonomy and its verification: the capability of automation to make and execute decisions in-situ; necessitated in part by the long light-time delays from Earth for deep space spacecraft. Another challenge is the high expense of achieving high assurance for software intensive systems.
And then there are the overarching issues of budget, schedule, and design. It is highly unlikely these system-of-systems will be implemented and interfaced, tested and verified, before deployment. How could formal methods define the requirements for these systems such that the protocols and interfaces, functions and fault management execute as intended for integration that may occur for the first time off-planet?
In my experience, NASA can accept new techniques where it can be demonstrated that current practices are not sufficient. For these future system-of-systems, formal methods may prove to be not only sufficient but necessary.
Currently, Mr. Aguilar works at the NASA Langley Research Center (LaRC) as the NASA Technical Fellow in Software Engineering, and the NASA Engineering and Safety Center (NESC) Discipline Expert in Software.
He received his Master’s Degree in Software Engineering from Carnegie Mellon, specializing in real-time systems, and Bachelor’s Degree in Computer Science from CSUN, specializing in robotic automation.
Mr. Aguilar has developed embedded systems his entire career, acting as Project Manager, Configuration Manager, Real-time Performance Engineer, HW API Developer, Test Driver Developer, HW Installation and Integration Engineer, and SW Installation and Integration Engineer. In addition to spacecraft command and control systems, he worked software development on flight simulators, NATO communications systems, RADAR Command and Control Centers, and Marine Special Forces robotics. As the Safety Engineer for the Interim Control Module (ICM), a reboost and attitude control system for the International Space Station (ISS), Mr. Aguilar performed the analysis and assessment, both in hardware and software, of the ICM quad-processor autonomous Fault, Detection, Isolation, and Recovery (FDIR) capabilities.
After joining NASA in 2003, Mr. Aguilar acted as the James Webb Space Telescope (JWST) Science Instrument Flight Software Manager, managing the interface and integration of the JWST C&DH Core Flight Software development at the Goddard Space Flight Center (GSFC) and the Science Instrument flight software applications developed externally by the European Space Agency, the Canadian Space Agency and EMS Technologies, the University of Arizona and Lockheed Martin ATC, and the JPL/European Consortium.
Mr. Aguilar is currently the NESC Discipline Expert in Software, leading assessments in software architectures, interface modeling, software defects, software static analysis, abort systems, fault tolerance, flight termination systems, software reuse, and flight software code generation. He is currently very involved in the verification of the software being developed for the future NASA crewed missions.