Java PathFinder a Translator From Java to Promela

Date Added: Jan 2010
Format: PDF

This paper outlines some high level ideas for translating JAVA to the PHOMFLA, the "Programming Language" of the of the SPIN model checker. The purpose is to establish a framework for verification and debugging of JAVA programs based on model checking. This paper shall be seen in a broader attempt to make formal methods applicable "In the Loop" of programming within NASA' s areas such as space, aviation, robotics, and ground control software.