The goal of this project is to create a visualization for JPF's statechart model checking extension. This could be useful in tracking bugs when using JPF, especially for newer users. This project could help to make the use of JPF more intuitive.

The project will create UML state machine diagrams out of JPF state machine models, and animate traces of event sequences produced by the model checker.

The project will be implemented in Java and will rely on the JPF Listener API. It will be relatively stand-alone from JPF. The project will be developed under the NASA Open Source Agreement version 1.3.