NASA Logo

NTRS

NTRS - NASA Technical Reports Server

The auto‑search feature has been disabled based on user feedback. Enter a search term/phrase and click “Search” to begin.

Back to Results
Java PathFinder: A Translator From Java to PromelaJAVA PATHFINDER, JPF, is a prototype translator from JAVA to PROMELA, the modeling language of the SPIN model checker. JPF is a product of a major effort by the Automated Software Engineering group at NASA Ames to make model checking technology part of the software process. Experience has shown that severe bugs can be found in final code using this technique, and that automated translation from a programming language to a modeling language like PROMELA can help reducing the effort required.
Document ID
20000102373
Acquisition Source
Ames Research Center
Document Type
Other
Authors
Havelund, Klaus
(RECOM Technologies, Inc. Moffett Field, CA United States)
Date Acquired
September 7, 2013
Publication Date
January 1, 1999
Subject Category
Computer Programming And Software
Funding Number(s)
CONTRACT_GRANT: NAS2-14217
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available