NASA is auctioning 5 software patents in the area of software development of control systems using formal methods. The patents were filed 2004–2006 and issued in 2009 and 2010.

Each patent includes the following statement:

ORIGIN OF THE INVENTION

The invention described herein was made by a employees of the United States Government and may be manufactured and used by or for the Government of the United States of America for governmental purposes without the payment of any royalties thereon or therefor.

The patents were scheduled to be sold at auction, 11 November 2010 by ICAP Ocean Tomo, who described the lot as follows:

Exclusive License Related to an Improved Methodology for Formally Developing Control Systems

This patented invention relates to an improved methodology for developing formal models for control systems where systems failure would have catastrophic implications.

In traditional systems development, the control of a process is based on complete knowledge of the process, as documented in a model. The mathematical model is assumed to be known, and the inputs to the process are deterministic functions of time. In some cases, there may be unknown components, but these portions of the model assume that the characteristics of the uncertainties are known (i.e., distributions of events). However, in many situations, the assumptions made regarding the uncertainties may be insufficient – there may be gaps or conflicts within the model, which may lead to failures in the model or control system. For non-critical control applications, this failure will prompt a redesign of the model, improving its performance in the future. However, in applications where failure would be disastrous (i.e., control systems failure would cause irreparable damage), another approach is necessary.

The present invention proposes leveraging automata learning and formal methods to create potential scenarios for models to ensure that the developed formal model is complete and free of any internal conflicts. By using automata learning, this scenario-generation process creates the most robust set of potential situations possible, and with the input of the developer, ensures that the formal model completely meets the formal requirements. This process results in a formal model that will not fail. The patented invention further takes the complete, formal model and generates the code required to implement the model.

The expected value of this lot exceeds $250,000.

The titles, patent numbers and links to the full patents are below.

Automata learning algorithms and processes for providing more complete systems requirements specification by scenario generation, CSP-based syntax-oriented model construction, and R2D2C system requirements transformation. [7,668,796]

Swarm autonomic agents with self-destruct capability. [7,627,538]

Systems, methods and apparatus for verification of knowledge-based systems. [7,752,608]

Systems, methods and apparatus for implementation of formal specifications derived from informal requirements. [7,739,671]

System and method for deriving a process-based specification. [7,543,274]