The Architecture of Pda
Figure * 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 architecture
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.
Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage
