The Maude-NPA GUI

In this webpage you will find information about the Graphical User Interface of the Maude-NPA (Maude-NRL Protocol Analyzer) and instructions for its installation and use.

The aim of this graphical user interface is to give the user a complete animation of the Maude-NPA search tree generation process which she can control at will. In general, this GUI allows the user to:

  1. Load a protocol specification file, previously written following the Maude-NPA syntax.
  2. Execute the backwards reachability analysis step by step, representing graphically the search space tree generated by Maude-NPA.
  3. View both, the graphical and textual visualization of a Maude-NPA state.
There is more detailed information about these features in the installation and user manual provided below.

Related to implementation details, the interactions between this graphical user interface and the Maude-NPA tool have been achieved using the InterOperability Platform (IOP) framework and its associated IMaude library. The graphical part of the GUI has been implemented using the JLambda programing language, another component of the IOP framework. We provide a more specific information about this issue at [2], in the Documentation section.

Here are the installation packages of the Maude-NPA GUI prototype version:

If you have any question about using the Maude-NPA GUI or if you would like to report any problem you experience with Maude or make any suggestion for enhancements and improvements, please, send an e-mail to

(*) This work has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grants TIN 2007-68093-C02-02 and TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052.

"Una manera de hacer Europa"

Last modified on 30th of January of 2012