The Paose approach to software engineering combines Petri nets with the paradigm of agent-orientation and utilises th e agent metaphor to structure large software systems and their development. Up until now the Paose approach only exhibited aspects of verification in a rudimentary way. This is due to the complexity of the systems to be verified on the one hand, and the expressiveness of the employed Petri net formalism of reference nets on the other hand. This contribution deals with enhancing the tool support for Paose in this regard. We present how we technically integrate the functionality of LoLA, a sophisticated verification tool, into Renew, the development and runtime environment that backs Paose. Furthermore we sketch how structural aspects of multi-agent systems developed with the agent fra mework of Mulan can be exploited for verification. The results of the integration are applied in the context of distributed network security for the Herold research project.
In order to successfully tackle the challenges of creating large, complex software
systems, the adoption of a development approach is almost mandatory. Paose
(Petri Net-Based Agent- Oriented Software Engineering, [
One aspect that has, up until now, been largely left out of the Paose
approach is the verification of the resulting software systems. The main challenge in
this regard is posed by the highly expressive nature of the Petri net formalism of
reference nets [
Verification of a software system is especially important, when certain
properties of the system need to be guaranteed after deployment. Aspects, like
deadlock-freeness or boundedness, are often not just simpl e inconveniences, but
can endanger critical components. This is especially true in the case of the
Herold project [
The goal of the particular research presented in this contribution is to
enhance the tool support for Paose with regards to verification. The designated
tool for Paose is Renew (Reference net workshop, [
We have chosen to integrate an existing, external tool for verification, instead
of developing this functionality from scratch. This tool is LoLA (Low Level Net
Analyser, [
Concerning related work, we researched other verification tools prior to
choosing LoLA for the integration. These tools included Netlab (see [
The paper is structured in the following way. Section 2 discusses the technical aspects of the integration of LoLA into Renew. Section 3 then discusses, how this integration can conceptually be used within Paose. Finally Section 4 summarises and concludes the paper. 2
Renew, the Reference Net Workshop, is a high-level Petri net editor and
simulator created at the University of Hamburg. It is described in [
LoLA, the Low Level Petri Net Analyser, is a verification tool for
place/transition and coloured nets described, for example, in [
In order to use LoLA within the Renew tool, we implemented an export from Renew nets to the textual net representation that LoLA requires. Figure 1 gives an example of a simple Renew net and the corresponding textual LoLA net file, as generated by the presented Renew plugin.
Renew nets consist of an unsorted set of figure objects, each of which represents one net element1. The figures of a net can be accessed by means of a Java enumeration, which is processed to generate the representation LoLA understands. In order to do so, we have to identify the places, the transitions (together with their pre- and post-set) and the initial mark ing of the net2. These are extracted from the Renew net and written into a new file that complies with the LoLA syntax.
The export of Renew nets is restricted to those concepts that can be expressed within LoLA. Therefore we employ the following projection, which strips some semantic information from the reference net. We first need to ignore all inscriptions on places, transitions and arcs (type declarations, guards, synchronous channels, Java code and variables), except for names of places and transitions. 1 Net elements in this context are not only transitions, places and tokens, but everything in the net drawing, including inscriptions, names and comments. 2 We can restrict ourselves to only these three, because, for now, we are only using the P/T-net functionality of LoLA. However, we continue to work on mapping Renews’ type declarations to LoLAs’ specification format for high-l evel nets, which allows the declaration of sorts and operations. These can later on be referred in the verification requests.
Then we need to treat object and net tokens (i.e. tokens that represent Java objects or itself nets) as black tokens, wherever they appear. Finally we need to replace test arcs (which are bidirectional) with normal arcs leading to and from the elements involved.
Additionally we have implemented the possibility to annotate verification tasks inside a Renew net. The corresponding text figures are written into separate files, since LoLA requires them to be independent from the textual net representation3.
Verification tasks for LoLA can be defined in two ways in the Renew tool. They can either be added directly as unconnected text figures, using the LoLA Syntax (e.g. the “ANALYSE MARKING . . . ” text in Figure 1, whic h corresponds to the task of checking if the specified marking is reachable) or, more comfortably, as a special inscription for the concerning element. For example, the inscription of the place place1 in Figure 1 stating “ASSERT BOUNDED” is automatically translated into a verification task to check the boundedness of the place. The latter is more convenient for the user, since it does not require him to keep track of the names of the net elements for verification. 3 It is also possible to add some verification tasks directly to the net file. Another viable alternative is to provide the tasks to LoLA as streams.
Providing LoLA functionality with the exported nets from within Renew is handled by calling LoLA externally and feeding the results back into Renew. There are other options how to integrate LoLA, however missing insight into the internal workings of LoLA we were not able to implement them yet. The work on this is still ongoing.
Now that we have outlined how LoLA was technically integrated into Renew we can proceed to discuss in which ways the functionality is used. Apart from simply being able to specify nets and manually exporting and verifying them, we have decided to provide a more convenient tool set for the Renew user to access the functionality. Therefore we implemented a plugin for Renew that offers the described export capabilities and aggregates some of the functionality offered by LoLA into a graphical view, which makes it comfortably accessible in the Renew context. The work on this plugin is still ongoing. Some features have already been implemented while others are considered work-in-progress.
The plugin provides the means to check the transitions and places of a net currently being drawn. It will check if transitions are dead and places are bounded. Dead transitions and unbounded places will be marked in the net drawing, so the user can revise the relevant parts of the net.
The plugin offers a kind of checklist for a net. In this checklist the properties of quasi-liveness, reversibility, deadlock freedom, exis tence of home markings and boundedness are displayed. For now, for each of these properties an indicator is given (either positive or negative), but the checklist can be extended to supply additional information, such as concrete home markings or witness paths. In Figure 2 we included a screenshot of the net checklist that shows the result we obtained for the net on the left.
The plugin will provide a window in which the reachability and coverability graphs of the net currently being drawn are displayed. This creation of the graphs is initiated manually by the user.
Marking editor: Work-in-progress
The plugin will provide an editor for entering a specific marking for the current net. The fields of the editor are updated to display all current places. The user can enter the tokens of each place and then check the marking for example for its reachability (from the initial marking or a second marking input into the plugin window), coverability or status as a home state.
Feedback is immediately given to the user within the plugin window.
Similar to the marking editor, the plugin will provide the means to input a CTL formula for the current net, which can then be checked directly from within Renew. 3
Applying Petri nets for software engineering (SE) is a common practice
(see e.g. [
Paose employs concepts from agent-orientation to structure soft ware systems on
four different levels, which together form the Mulan architecture (Multi- agent
nets, see [
Each of the four levels is realised with reference nets, with higher levels embedding the lower ones as net tokens. In this way a platform contains references to agent nets, which, in turn, hold references to protocol nets. Due to the 4 The term does not refer to a communication protocol that encompasses several agents, but rather stands for a specification of a specific behaviour of an agent. operational semantics of reference nets, a modelled multi- agent system can be simulated directly.
Being an exhaustive SE-approach Paose also encompasses techniques for the
specification of interactions between agents, for the definition of ontologies and
for the definition of agent roles and knowledge bases, all of which are fully
supported by internally and externally developed tools. A model for the development
process, as well as an agile method and facilities for the automatic generation of
nets and documentation are available. However, we will not go into detail here,
but refer the reader to [
Up until the research presented here, the Paose approach did not include formal verification, but instead relied on the sophisticated type and syntax checking offered by Renew. Because the ontology of a multi-agent application is transformed into a Java type hierarchy, the Renew tool can provide the developer with type checking for ontology objects. The same is true for the metaontology describing platforms, agents, services and messages among other Mulan-relevant objects.
An additional feature at least partially fills the role of verification. During the
development process the multi-agent application can be sim ulated and inspected
thoroughly, and can even be modified on the fly during a simulation run [
This contribution addresses the afore-mentioned shortcom ing of Paose, by
providing “classical” Petri net verification. However, we t ailor the functionality to
the specific context of Paose. Due to the Turing completeness of reference nets
[
It needs to be examined what assertions can be made about the original net. One can observe that if a transition is activated in the original net, it is also activated in the projection5. On the other hand, if a transition in the projected net is not activated, it will not be activated under any circumstances in the original net. So we can conclude that if a deadlock occurs in the projected net, it also occurs in the original one. The opposite does not hold true however. 5 There is a minor exception to this. In the case where several transitions are connected to the same place with a test arc, they can fire concurrently in the original net. Because test arcs are replaced by usual arcs, this no longer can happen in the projected net.
We will now detail how the LoLA plugin can play an important role in
supporting the development of multi-agent systems by utili sing the structure of
Mulan nets for verification.
We claim that the reference nets used in the Paose context exhibit some
structural features that make them well suited for verification. For this we have to
take a more detailed look at the utilised net systems. Agent and platform nets
are fixed, this means all agents and platforms share a common structure, while
application specific functionality is added through protocol nets and the
knowledge base (and application specific infrastructure). While agent and platform
nets need to be live, it is essential for protocol nets to terminate, i.e. to reach a
terminal state. Some groundwork on this topic has been presented in [
Figure 3 illustrates the typical form of a protocol net used in Mulan.
Structurally speaking, protocol nets start and end with a transition, which
synchronises with the embedding agent net. The initial synchronisation causes the newly
instantiated protocol net to be put on a special place in the agent net, dedicated
for ongoing conversations. Messages an agent receives can be directly passed to
an ongoing conversation, if their type matches the type expected in the protocol
net. The final synchronisation removes the instance of the protocol net from the
conversation place, once it is finished (meaning it reached its terminal state).
In this way, it is essentially a workflow net [
While a conversation is ongoing, agents send and receive messages in their corresponding protocol nets that together form the conversation. The platform net is also involved in the conversation, because it routes the message to its destination. Deadlock-freeness and thus termination can only be verified under the assumption that the communication partners and the message transport service behave well. On the other hand, stripping the inscriptions from the protocol net, one can verify deadlock-freeness of the projected protocol net independently of its environment. Using the LoLA tool in combination with the existing type check we can enhance verification in cases where alternative behaviours are chosen according to message content (which is the standard case).
Some other verification tasks for multi-agent systems sprin g to mind and will be the focus of future work: – Do agents possess matching protocols so that they can communicate? Given two, or more, agents this task can determine if they possess matching protocols. This means that an outgoing message in one agent’ s protocol has to correspond to an incoming message in another agents’ p rotocol. In terms of practical implementation this boils down to matching the outgoing message as a type to the incoming message as a type, possibly by merging the protocol nets. – Does an agent have required protocols to be embedded on a platform? While similar to the previous task, this task is a bit more general. Instead of explicitly matching a number of agents for communication, this task determines if an agent possesses the required functionality (i.e. protocols) needed to be active on a specific platform. This task is more comprehensive and complex, since it addresses further aspects concerning functionality, not just communication. In practical terms, more nets have to be matched and certain assumptions about the content of protocols (for example through type matching) have to be verified. – Is the overall communication structure deadlock-free?
Another related task is to check the overall interaction and communication structure of the multi-agent application for deadlocks. Ta king the agent interactions into account we could generate a simplified net version of the overall communication, assuming that the internal workings of the agents are correct and do not deadlock. The check would then again be confined to the messages and their types, but instead of having a particular set of agents and protocols in the focus, it would examine the overall multi-agent application.
These last points dealing with the orchestration of protocol nets illustrates
the intimate relation between protocol nets in the Mulan architecture and open
nets of [
We have presented a way to make use of an existing tool as a plugin for Renew and how the Paose approach profits from this integration. The technical real6 Available online as open source from http://service-techn ology.org/. isation was easily achieved due to the flexible plugin mechanisms provided by Renew. So far we have used the tool to check for very basic properties, but as was advocated in Section 3, we are working on applying it to multi-agent systems. Conceptually we gain enhanced tool support for Paose, making it easier to develop functioning-as-designed multi-agent applicat ions.
Concerning future work, the efforts of enhancing Renew and Paose with the help of LoLA are still ongoing. We are looking at further ways of extending the functionality of the LoLA plugin for Renew and are researching additional areas of our multi-agent systems for verification, as was out lined in Section 3.3. As for the technical aspects, a promising avenue of work is to also incorporate the support for sorts and operations offered by LoLA into the plugin. This will improve the modelling effort for verification and, in turn, make using LoLA within Renew more comfortable.
From a practical point of view, we will use the results we have obtained
within the Herold research project7. Herold deals with distributed network
security and the management of network security components (see [