The Architecture of PDA

The Figure below sketches the architecture of the Pda tool. The user enters protocol definitions and derivations in the graphical editor, which has a rich set of features to ensure the scalability of the approach. Most prominently, the graphical nodes representing protocols, agents, rules, etc. can be collapsed and expanded as needed, which greatly improves the readability of complex derivation diagrams. While drawing the nodes and edges that make up protocols or derivations, the user gets some live feedback that prevents him/her from adding nodes and edges that are not permitted. For instance, if one side of a send/receive edge has been attached to a state in an agent node, then the user interface makes it impossible to attach the other end of the edge to a state within the same agent. The labels attached to protocols, internal actions, send/receive term, agents and other elements of the derivation are subject to corresponding syntax and semantics rules that are implemented in the parser and static analyzer. If the user makes an error on one of these labels, the graphical editor displays a visual feedback next to the place where the error has been detected. The derivation engine is responsible for performing instantiations and transformation operations, and for providing the result of these operations to the user as new nodes in the graphical editor pane. For example,for an instantiation, the user only enters the definition term for the refined protocol, the process graph of the instance is created automatically by the derivation engine component. All objects involved in the protocol derivations are stored in a database in order to allow for efficient access and update operations. In its current version, the database is built into Pda, but future versions will provide the possibility to use server-based databases.

Pda is also designed to be an integration platform for security-protocol related tools.Pda provides an API that allows Java developers to write plugins for Pda. The API gives access to the internal data structures of the protocols specified by the user and/or loaded into the Pda-database. In order to make Pda also available for extension on a non-Java basis, Pda comes with an S-expression generator that translates the graphics of the protocols and the attached specifications into an S-expression format. The Specware-plugin mentioned earlier makes use of this interface and provides itself a user interface that allows the user to attach model descriptions to protocols. Other code generators can be defined as needed, for instance one for generating executable agent code from the protocol descriptions. Other tools can plug into Pda by either using one of the code generators or by directly using the Java API.

---