← Back to NASA Technology Projects
Completed TRL 3 (started at 2, targeting 3)
Model Checking is a powerful technique used to verify that a system does not violate its intended behavior. While this is very useful in proving the robustness of a system, one drawback is that as the system grows in complexity or the number of properties being checked increases the time it takes to complete the model checking process grows exponentially larger. General-Purpose computing on Graphics Processor (GPGPU) architecture allows for programs to be rapidly executed on thousands of threads as a cheap alternative to supercomputing clusters. The goal of this project is to utilize CUDA and OpenCL GPGPU frameworks in order to parallelize the SPIN model checker to the greatest extent possible.
General-Purpose computing on Graphics Processor (GPGPU) architecture allows for programs to be rapidly executed on thousands of threads as a cheap alternative to supercomputing clusters. The goal of this project is to utilize CUDA and OpenCL GPGPU frameworks in order to parallelize the SPIN model checker to the greatest extent possible.
Listed on TechPort itself — the most direct way to ask about this specific project.
This is early/mid-stage (TRL 3) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.
None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.