JPF-AWT: Model checking GUI applications

Verification of Graphical User Interface (GUI) applications presents many challenges. GUI applications are open systems that are driven by user events. Verification of such applications by means of model checking therefore requires a user model in order to close the state space. In addition, GUIs rely extensively on complex and inherently concurrent framework libraries such as AWT/Swing, for which the application code merely provides callbacks. Software model checking of GUI applications therefore needs abstractions of such frameworks that faithfully preserve application behavior. This paper presents JPF-AWT, an extension of the Java PathFinder software model checker, which addresses these challenges. JPF-AWT has been successfully applied to a GUI front end of a NASA ground data system.