This work should be seen in a broader attempt to make formal methods applicable within NASA's areas such as space, aviation, and robotics.
Hence, the Java program must have a finite and tractable state space. Jpf generates a Promela model with the same state space characteristics as the Java program. The Spin model checker will then look for deadlocks and violations of any stated assertions. The Java program may contain assertions, which are translated to similar assertions in the Promela model. Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. This paper describes a translator called Java PathFinder (Jpf), from Java to Promela, the modeling language of the Spin model checker.
0 kommentar(er)
