In this paper we examine ways to verify reference nets, a class of high level Petri nets supported by the Renew tool. We choose to restrict reference nets to hypernets, another nets-with in-nets model more suitable for verification purposes thanks to an expansion toward 1-safe Petri nets. The contribution of the paper is the imple mentation of such analysis techniques by means of a Renew plugin. With this plugin it is now possible to draw, and to analyze a hypernet. The work is demonstrated by means of a simple example.
The verification of properties of a software system has become an important part of software engineering. Especially specifications critical to the correct execution of a software system need to be verified in order to guarantee them after deployment. The problem of verification is its complexity and the effort required for it. Without proper methods the verification itself is difficult, costly and time-consuming.
In this paper we approach the general problem of verification with the help of Petri nets. The formalism is deeply rooted within established theoretical and formal methodologies, as well as being supported by a multitude of tools and analysers. Petri nets have been studied in detail and contain properties, for which established verification techniques exist. Using Petri nets the general approach is to map and translate specific software issues and properties to these Petri ⋆
Partially supported by MIUR, and DAAD net properties. These properties can then be verified using the known Petri net techniques. Assertions made for these can then be translated back for the software behind it.
High level nets, Petri net models enriched with additional abstraction constructs, are well suited to represent complex systems due to their high abstraction constructs. One of their problems is that verification of their properties is difficult. Properties which are computable with low-level formalisms become undecidable, and thus cannot be verified anymore in some high-level models. However, high-level formalisms can be restricted in some wa y so that they can be translated into low-level formalisms, which in turn can b e verified again. In particular, the interest of this paper is on high level nets which use the netswithin-nets paradigm, formalisms in which the tokens of a Pe tri nets can be structured themselves as Petri net. The two formalisms analyzed are reference nets, the formalism used as a basis for the Renew tool, and hypernets, another nets-within-nets formalism with particular restrictions that allow the expansion toward an equivalent 1-safe Petri nets. In this paper we will show how to translate a subset of the high-level reference net formalism into hypernets, which in turn can be easily translated into 1-safe nets. These can the n be analysed by existing toolsets. The main result of our work is the implementation of a Renew hypernet plugin which incorporates features for computing S-invariants, and features for model checking a hypernet. As far as we know, this is the first time that analysis techniques typical of Petri nets has been implemented in a tool which support the nets-within-nets paradigm, and it is mature enough to be used in a real application context. In the rest of the paper when we will talk about invariants we are always referring to S-invariants.
The paper is structured into the following sections. Following this introduction the theoretical and technical background is shortly discussed in section 2. This section will focus on the reference net and hypernet formalisms. In section 3 we will show how to translate reference nets into hypernets and determine the prerequisites for analysis. Section 4 describes the Hypernet plugin created for Renew. Section 5 gives a short example how these different tools are incorporated and used to analyse a given net. The conclusion of the paper is found in section 6. 2
In this section we will introduce by means of examples the basic theoretical
formalisms used in this paper, as well as motivate why we have chosen them as
our means of verification and modelling. The interested reader can find them
in the cited references. In general Petri nets offer a simple way of modelling
concurrent behaviour of a system. Higher level nets often introduce abstractions
from the simple net models, which offer structures and methods not available to
or difficult to model in low-level Petri nets. One major such ab straction is the idea
of nets within nets, introduced in [
In the following subsections we will describe the reference and hypernet
formalisms.
2.1
The reference net formalism serves as the starting point of our examinations. It
was described in [
Communication between different net instances within the reference net
formalism is handled via synchronous channels, based on the concepts proposed
in [
Figure 1 shows a simple example of a reference net system. The example was modelled using the Renew tool, which will be described later. It models a producer/consumer system, which holds an arbitrary number of producers and consumers. The system consists of three kinds of nets: the system net, the producer nets and the consumer nets. The producer and consumer nets both possess the same basic structure, but use different channels. The system net serves as a kind of container for the other nets. The transitions labeled manual initiate the creation of new producers and consumers by creating new tokens when a user manually fires them during simulation3. The transitions labeled C and P actually create new producer or consumer nets when firing. These new nets are put onto the places below the transitions. The transition labeled I synchronises the firing of a transition in one consumer and one producer each (labeled I1 and I2 in the other nets). In this way it is possible to simulate the behaviour in such a way, that whenever a producer produces a product an arbitrary consumer consumes it. It is of course possible to enhance this model by, for example, adding an intermediary storage, which can store items from arbitrary producers until consumers need them. Another way of making the model more realistic is to explicitly model the products as nets as well. That way they would not just be simple tokens but actual objects being exchanged via the synchronous channels between the producers and consumers. In this case the parameters of the channels would be the nets, which would be transmitted from within the producer nets into the consumer nets.
The Petri net editor and simulator Renew (The REference NEt Workshop)
was developed alongside the reference net formalism, and is also described in [
Hypernets
As we will discuss later in section 3, we introduce hypernets in this paper
because they have been used as a restriction of the reference nets formalism to
allow property verification in Renew. Hypernets are a nets-within-nets
formalism introduced to model systems of mobile agents [
Due to technical limitations in the Renew tool only the basic version of
the formalismi [
The system evolves moving agents from place to place. A peculiar characteristic of hypernets is that the hierarchical structure is not static, but an agent can be moved from a place p belonging to an agent Ai, to a place q belonging to a distinct agent Aj . Another characteristic of hypernets is that agents cannot be created or destroyed. To ensure this ”law of conservation of tokens” each net representing an agent is structured as a set of modules which have the structure of synchronised state machines, enriched with some communication places that allow the exchange of tokens between two agents close in the hierarchy. Agents and modules have a sort, and an agent can only travel along modules of the same sort.
In Figure 2, and Figure 3 the hypernet modelling a slightly modified version
of the one seater plane case of study is drawn. This case of study has been
introduced in [
To keep the example simple we considered a version with a plane which has only one seat. We choose to illustrate this example to show in an informal way how hypernets works. Moreover, in Section 5 we will show how it is possible to prove some properties of this simple example using the Renew plugin we developed.
The agent in Figure 2 models the behaviour of the airport. It has three modules, one for handling passengers, one for handling planes and one for synchronisation purposes. Transition board belongs to both module passenger and module plane, and can only be executed synchronously. The same applies for transitions deplane and to_rf. Communication places are the dashed half circles. They can either be up-communication places , used for communicating with the net at the level immediately above in the hierarchy (such as the two communicating places of the module plane in the airport agent), or down-communication places , used to communicate with an agent located in another module of the current net (such as the communication places in the synch, and passenger modules of the airport). In the latter case, a name of a module is provided. In this module there must be an agent ready to provide the traveling token which will be moved in the hierarchy, otherwise the transition is not enabled.
For example, transition deplane of the passenger module in Figure 2 has an input communication place which indicates that a token is expected. Since this communication place is marked with the plane annotation, the traveling token which is being moved to place l must be provided by a plane agent. This plane agent must be located in the input place of transition deplane in module plane of the airport, namely lg. In the example the only agent which can provide a token is P 1. The traveling token, which must be a passenger, is then selected and taken from the seat place of the plane agent (Figure 3), and moved to l.
Transition to_rf is another example of use of communication places. From the airport perspective it is only required that an agent located in the plane module has a module synch containing with a transition to_rf preceeded and followed by two up-communication places. This requirement is fulfilled by agent P 1, but from the P 1 perspective it is also required the enabledness of the synchronized to_rf transition in the module check-passenger. Therefore this c onfiguration to_rf is not enabled because freePlaces is not marked.
Hypernet being a high level net model means that the execution of a
transition, like deplane, has several firing-modes [
One of the most important features of hypernets is that they have a straightforward expansion towards a behaviourally equivalent 1-sa fe nets. This expansion not only gives hypernets a precise semantics in terms of a well known Petri nets basic model, but also guarantees the possibility to reinterpret on hypernet all the analysis techniques developed for the basic model. The 1-safe net is built in the following way: – For each agent A, and for each place p in the hypernet a place named hA, pi is added in the corresponding 1-safe net. A token in this plac e means that A is located in p, – For each consortium Γ in the hypernet a transition named tΓ is added in the 1-safe net, – An arc is added from a place hA, pi, to a transition tΓ if A is a passive agent in Γ , and p is the input place from which the agent A comes. – An arc is added from a transition tΓ , to a place hA, pi if A is a passive agent in Γ , and p is the output place where the agent A is going to.
Finally, a place hA, pi of the 1-safe net is marked if in the initial configuration of the hypernet agent A is located in place p.
For example, the one seater plane case of study we just discussed is translated in the 1-safe net shown in Figure 4. Plane P 1 can be in places lg, rf, bg in the hypernet, thus the 1-safe net contains places hP 1, lgi, hP 1, lgi,hP 1, lgi. The same must be done for traveler agents, and for the CHK check agent. Since transition deplane in the hypernet has two firing-modes, in the 1-safe net two tra nsitions which models each of the firing modes of deplane are added (for simplicity both called deplane). The same has been done for transition board. The firing of a transition in the 1-safe net exactly models what happens whe n a consortium fires in the hypernet.
As already mentioned, it can be demonstrated that this net is 1-safe, and
has a reachability graph isomorphic to the one of the corresponding hypernet.
Details, formal definitions, and proofs discussed can be found here for hypernets
in [
deplane <P1,lg> deplane board
The main motivation for using high level nets is that, given a system, it is
possible to obtain a model of the system with an high level net which is smaller
compared to the model obtained using basic Petri nets. However, if you are not
careful, the increase of the modelling power decreases the decision power of the
model. For example, in [
It is in this perspective that the implementation of the hypernet formalism as a plugin of the Renew tool has been made. Restricting reference net is probably the most intuitive way to use verification techniques in Renew. In particular, the use of a nets-within-nets formalism like hypernets as a r estriction permits the use of the nets-within-nets paradigm, which is probably the most intresting feature in Renew. The original contribute of the paper is to show how this plugin allows the use of verification techniques, like invariants and CTL model checking, to check properties of systems which are suitable to be modeled with the the nets-within-nets paradigm. 4
From a technical point of view the implementation of a new formalism in Renew is done using a plugin mechanism. The most important method contained in the classes implementing the plugin is a compile method which takes as input a shadow net, a set of Java objects containing all the information about the net the user has drawn in the graphical editor of Renew, and transform it in a set of Java objects used by the simulator engine to simulate the net. This compile method is responsible for checking that the net drawn by the user is an actual hypernet in our case. In particular, in order to be able to use Renew as a hypernet simulator, the arc and transition inscriptions used in the modeling process must be restricted in such a way that the drawn net is a hypernet. Therefore the restrictions applied in the plugin are the following: – Inscriptions (tokens) inside places can only be in the following forms: identifier or identifier:netType. In the first case the identifier represent the name of an empty net, and will be treated by the simulator engine as an black token; in the second case a new instance of the net netType will be created and placed inside the place. – Inscriptions on arcs are restricted to single variables only. Each arc must contain exactly one variable inscription. – The inscriptions of input (output) arcs must not be duplicated. In this way it is possible to preserve the identity of nets: duplication of tokens is forbidden. – Balancing of transition has to be checked, i.e.: the set of variable names used to inscribe input arcs must coincide with the set of variable names used to inscribe output arcs. – Communication places are deleted, and are simulated by means of synchronous channels. These channels are counted when checking transition balance.
For example, the airport agent shown in Figure 2 can be drawn as a hypernet in Renew using the net shown in Figure 5. The traveler empty tokens are place inscriptions T 1 and T 2, and the plane net instance is created by the P 1 : place inscription. Each transition is balanced. For example transition deplane in the airport has a bidirectional arc labelled pl, and an output arc labelled pa for which there is a correspondant downling, namely pl : deplane(pa). Each communication place is deleted, and it is replaced with a synchronous channel. Land and takeoff transitions are equipped with two uplink because they were connected to two up-communication places. Deplane and board transitions contain two downlinks because they were connected to down-communicating places. The module name used to label communicating places is used to retrieve the variable name used in the downlink.
The P 1 agent of Figure 3 is drawn in the hypernet plugin of Renew with the net in Figure 6. Again, up-communication places are repl aced by channels, and transition to_rf must synchronise with the corresponding transition in the airport agent.
pa pl pl:to_rf() to_rf seat T1 pa chk CK numPass chk
T2 l rf pa pl :land(pl) land pl pl:deplane(pa) pl pl lg P1:plane
As we already mentioned, thanks to the expansion to 1-safe ne ts it is possible to use verification techniques defined for this class of net to analyse system modelled with a hypernet. Two of the most useful techniques are invariants analysis, and model checking. We explored two possibilities of using them in the plugin we implemented: internal implementation in Renew, or exporting the 1-safe net in a format understandable by other tools. Sin ce implementing these analysis techniques in an efficient way is a difficult task (some tools are very elaborated, and have been implemented over several years), and since very efficient open source tools are available for free, we decided to use external tools to implement invariant analysis, and model checking of a hypernet.
In the following sections we will show how the extensions and incorporation can be used in a practical example. 5
The invariant analysis, and the model checking extensions we implemented in Renew can be used to prove properties of a system. We have chosen the external tools LoLA (see http://www2.informatik.hu-berlin.de/top/lola/ lola.html) and INA (see http://www2.informatik.hu-berlin.de/~starke/ ina.html) for analysing purposes. Starting from the hypernet example of Section 2.2, we will prove using invariants that there is never more than one passenger on the plane, and we will prove using the model checker that a plane never refuels if there are a passenger on board.
By running the invariant analysis we get the following invariants: The first four invariants are those which guarantee the truth of “law of conservation of agents”, achieved thanks to the state machine d ecomposition in the formalism. For each agent there is a corresponding invariant indicating the places in which that agent can be located. Since the places of each invariant contains only one token in the initial marking, it is mathematically proved that each agent can be only in certain places: the places which are of the same sort of the agent itself. Moreover, these four invariants can also be used to prove that the net is 1-safe: they cover all places of the net, and contain only one token in the initial marking.
The fifth invariant is {h T 2, li, hCHK, numP assi, hT 1, li} and contains two tokens in the initial marking. Together with the second and the fourth invariants it can be used to prove that if the place hCHK, numP assi is marked then one of the two passenger is seated on the plane. The place is not marked only if both passenger are in the airport.
The sixth invariant is the counterpart of the fifth, and states that only one of the following places can be marked: {h T 2, seati, hCHK, f reeplacesi, hT 1, seati} . The information is clear: only one passenger can be in the seat place of the plane. If none of them is in the plane hCHK, f reeplacesi is marked.
In Figure 7 a screenshot of Renew after the computation of invariants is shown.
While invariants analysis can be launched, and the computed invariants can be analysed to extract information about the system, in order to analyze the system using model checking a formula specified in a temporal logic is needed. Since we choose LoLA, which is a CTL model checker, we need to specify the property we want to verify using this logic. For example, checking the property “if the plane is located in the place representing the refuel ing station then no passenger is on board” can be done by entering as input of the Renew plugin we implemented the following CTL formula:
ALLP AT H ALW AY S
N OT ((T 1.seat = 1 AN D P 1.rf = 1) OR (T 2.seat = 1 AN D P 1.rf = 1)) The formula checks that in every reachable state (ALLP AT H ALW AY S) the situation in which both placed hT 1, seati and hP 1, rf i are marked never occurs (and the same for places hT 2, seati and hP 1, rf i). The analysis performed confirms that the truth value of the formula is true, which is enough to guarantee that the property is true for the system.
As it can be seen in this simple example, the advantage of using model checking is that it is possible to express, and consequently to verify, more properties compared to invariant analysis. In our example, the information that a plane never refuels if a passenger is on board is not present in the computed invariants, but can be verified using the model checking. However, the drawback is that it is necessary to explore the whole state space of the system in order to verify a property. Invariants are computed on the static structure of the net, which is usually exponentially smaller compared to the state space of the system. In general, in real huge application both the techniques are useful: invariants give a quick overview of some properties of the system, model checking take more time and it can be used to verify specific properties of the system. 6
In this paper we discussed the verification of high-level Pet ri nets which use the nets within nets paradigm, with particular attention to the reference nets and the hypernets formalisms. We examined them, and we showed how to transform a subset of reference nets into hypernets, which in turn can be transformed into 1-safe nets. We then proceeded to describe the hypernet plugin created for Renew in the course of our work. With the help of this plugin and external tools we can analyse the transformed low-level nets, and in this wa y verify properties of the high-level net.
The contributions, and the results of this paper are the implementation of a plugin for Renew with which it is possible to draw of a hypernet, to compute its invariants, and to model check it. With this approach it is now possible to verify properties of systems modelled with net within nets oriented formalisms, such as reference nets and hypernets.
The results of this paper will make it possible to automatically analyse a hypernet, instead of first transforming it by hand, and then analysing the equivalent low-level nets. This will make the verification simpler and more user-friendly, which in turn will make it easier for software engineers to use these techniques in practical use cases. We plan to use these approaches to verify the model of an actually adopted Grid tool for High Energy Physics data analysis, and in the context of the HEROLD project. Future work will also focus on extending the possibilities of the verification, automating the process as far as possible and extending the toolset to other high-level Petri nets formal isms. The flexibility and adaptability of the Renew tool will be a large asset in this endeavour. Finally, the definitions of analysis techniques directly on the high level model, without the need of converting it to a low-level one, is a subj ect for future investigations, because it will avoid the conversion to low-l evel nets, which is an expensive operations in term of computational resources.