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:
- Load a protocol specification file, previously written following the Maude-NPA syntax.
- Execute the backwards reachability analysis step by step, representing graphically the search space tree generated by Maude-NPA.
- View both, the graphical and textual visualization of a Maude-NPA state.
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 , in the Documentation section.
 Maude-NPA GUI installation and user manual
 S. Santiago, C. Talcott, S. Escobar, Catherine Meadows, J. Meseguer
A Graphical User Interface for Maude-NPA.
In IX Jornadas sobre Programación y Lenguajes (PROLE 2009).
Electronic Notes in Theoretical Computer Science, 2009, to appear.
 Maude-NPA manual v2.0.
Here are the installation packages of the Maude-NPA GUI prototype version:
- Maude-NPA GUI for Mac OS 10.4 Tiger (Intel)
- Maude-NPA GUI for Mac OS 10.5 Leopard (Intel)
- Maude-NPA GUI for Mac OS 10.6 Snow Leopard (Intel)
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 email@example.com.
(*) 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.