Verifiable MDS Architecture (VMA) is a software architecture that facilitates the construction of highly verifiable flight software for NASA's Mission Data System (MDS), especially for smaller missions subject to cost constraints. More specifically, the purpose served by VMA is to facilitate aggressive verification and validation of flight software while imposing a minimum of constraints on overall functionality. VMA exploits the state-based architecture of the MDS and partitions verification issues into elements susceptible to independent verification and validation, in such a manner that scaling issues are minimized, so that relatively large software systems can be aggressively verified in a cost-effective manner.

This work was done by William Reinholtz and Daniel Dvorak of Caltech for NASA's Jet Propulsion Laboratory. For further information, access the Technical Support Package (TSP) free on-line at www.techbriefs.com/tsp under the Software category.

This software is available for commercial licensing. Please contact Karina Edmonds of the California Institute of Technology at (818) 393- 2827. Refer to NPO-40842.

Topics:
Architecture Computer software and hardware Logistics Software
This Brief includes a Technical Support Package (TSP).
Document cover
Architecture for Verifiable Software

(reference NPO-40842) is currently available for download from the TSP library.

Don't have an account?

Magazine cover
NASA Tech Briefs Magazine

This article first appeared in the December, 2005 issue of NASA Tech Briefs Magazine (Vol. 29 No. 12).

Read more articles from the archives here.

Overview

The document is a New Technology Reporting Form from the California Institute of Technology's Jet Propulsion Laboratory (JPL), detailing an innovation related to the "Architecture for Verifiable Software" under the NPO-40842 project. The primary focus of this technology is to enhance the development of mission flight software for spacecraft, particularly emphasizing the need for rigorous verification and validation processes.

The innovation, referred to as the Verifiable MDS Architecture, aims to address the challenges associated with creating highly reliable software for space missions, especially those that are cost-constrained. The technology is designed to facilitate the construction of mission data systems (MDS) that can be verified independently, minimizing the interactions between different system components. This separation of concerns allows for the application of formal verification methods, which are crucial for ensuring the reliability and safety of software used in aerospace applications.

The document outlines the motivation behind the development of this technology, which stems from the need to create a software architecture that supports aggressive verification while maintaining system functionality. The solution proposed involves a state-based architecture that partitions verification issues, thereby reducing scaling problems commonly encountered in rigorous verification approaches.

The report also includes details about the funding source, which is NASA, and mentions that the technology is still under development, with a prototype already created. It highlights the potential commercial applications of the technology, particularly in sectors where verifiability is critical, such as aerospace and possibly other high-stakes industries.

Additionally, the document notes that the technology has not yet been published or used outside of JPL, but there are plans for future disclosures, including a presentation at the ISORC conference. The contributors to this innovation are identified, with specific roles in the conception and implementation of the technology.

Overall, the document serves as a formal disclosure of a significant advancement in software architecture for aerospace applications, emphasizing its potential to improve the reliability of mission-critical systems through enhanced verification processes. It reflects JPL's commitment to innovation in space technology and its broader implications for commercial and governmental applications.