JPF-AWT: Model checking GUI applications

Peter C. Mehlitz, Oksana Tkachuk, Mateusz Ujma

DOI 10.1109/ase.2011.6100131 dblp

Abstract

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.

BibTeX

@inproceedings{Mehlitz-al:ASE11,
  author    = {Peter C. Mehlitz and
               Oksana Tkachuk and
               Mateusz Ujma},
  title     = {{JPF-AWT:} Model checking {GUI} applications},
  booktitle = {ASE},
  pages     = {584--587},
  publisher = {{IEEE} Computer Society},
  year      = {2011},
}

JPF-AWT: Model checking GUI applications

Abstract

Related papers