Description: The Next Generation Air Transportation System (NextGen) brings significant advancements to the current management of the National Airspace (NAS). These fundamental changes have significant implications for safety and security, which, in turn, require new, more flexible techniques for the verification and validation of complex, software-intensive systems and systems of systems. To address this need, Barron Associates will develop a demonstration sense-and- avoid application, representative of the kinds of new systems that are possible in NextGen, and a safety case arguing that it is safe to operate in the NAS. The safety case will rely on run-time assurance and formal methods as evidence to support its claims. Run-time assurance continuously monitors system-level safety properties for impending violations to diagnose software faults and allows a simpler, high-criticality reversionary function to provide assurance for a more complex software function; formal methods provide strong design-time assurance of correctness for software that must operate at the highest levels of criticality. A safety-case-based approach citing these two strategies as evidence offers significant cost savings for similar or higher levels of assurance as compared to traditional, process-based approaches.

Benefits: Barron Associates envisions significant near- and far-term uses for the proposed assurance technologies. For medical applications, formal methods and run-time assurance will allow more powerful, complex software to be safely and cost-effectively deployed on monitoring, imaging, and robotic devices. For unmanned systems, potential applications go beyond air vehicles to all classes of unmanned systems, including ground and underwater vehicles. The autonomy required by these poses a significant challenge to traditional verification and validation techniques; a challenge that is mitigated by the proposed approaches. Finally, the nuclear industry depends upon software for the control of its power plants and propulsion systems. Techniques that can affordably increase the level of assurance of safety-critical software will not only allow more complex software to be deployed in nuclear applications, but also go further to ensure the safety of these systems.

Barron Associates anticipates a number of opportunities to apply this SBIR-developed technology to NASA programs. With NASA's ongoing efforts for the development of the NextGen airspace, and their continued progress in both manned and unmanned space exploration, there is renewed emphasis on increased levels of safety, reliability, and affordability for these new and emerging systems and concepts. To address hardware component failures and faults, control and flight operational systems for advanced platforms will need to be intelligent, adaptable, reconfigurable, and often nondeterministic in their behavior in order to provide the required levels of safety and reliability. Current V&V methods cannot address such complex software systems and recent studies have indicated the cost of certifying such applications would clearly be prohibitive. Therefore, along with advanced flight control systems must come advanced V&V methods. Our proposed approach of combining design-time formal methods with run-time assurance directly addresses this need. Finally, the proposed safety assurance technologies will enable cost-effective certification of the assuredly complex software that will be required of the air traffic control system for NextGen.