In order to represent the behaviour of a (potentially large) set of concurrent systems, we propose a notion of product line of Petri nets, where presence conditions can be flexibly attached to places, transitions and arcs. To enable an efficient analysis of the whole set of nets, we have lifted several structural analysis methods for Petri nets, to the product line level. This avoids analysing each particular net in isolation. Finally, we propose an extensible tool infrastructure, based on Eclipse and on top of FeatureIDE, which supports the approach and permits adding new analysis methods in a non-intrusive way.
Petri nets is a popular formalism to model concurrent systems [
To facilitate this task, we combine Petri nets with software product lines (SPLs) [
In the following, Section 2 introduces PNPLs, Section 3 proposes lifting the analysis of structural properties to the PNPLs and lifts the marked graph property analysis as an example, Section 4 presents tool support, Section 5 compares with related research, and Section 6 concludes the paper and presents lines of future work.
FlexibleAssemblyLine InParts
Process
OutProducts
Legend mandatory optional This section defines PNPLs, and derivation of concrete Petri nets via feature configurations. We consider a simple notion of Petri net, but the approach can be easily adapted to other more complex versions. In particular, we assume that a Petri net is a tuple P N = (P, T , A) where P and T are disjoint sets of places and transitions, and A ✓ (P ⇥ T ) [ (T ⇥ P ) is the set of arcs connecting either places to transitions or vice versa. Given an arc a 2 A, we use a0 to refer to its source, and a1 to refer to its target.
PNPLs build on the notion of a feature model that defines the variability space of possible configurations.
features F = {f1, ..., fn} and a propositional formula
configurations.
= (F, ) consists of a set of
fixing the allowed feature
Example. As an illustration, we will be using a family of Petri nets describing the
behaviour of a flexible assembly line. Figure 1(a) shows the feature model using a
diagrammatic notation [
A PNPL is a Petri net whose elements can be annotated with boolean formulae over the features of the feature model.
Definition 2 (Petri net product line). A PNPL P N L = (F M, P N, ) is made of a feature model F M , a Petri net P N (called the 150% Petri net), and a tuple = ( P , T , A) of mappings. Each mapping X (for X 2 { P, T , A}) consists of pairs hx, xi mapping an element (a place, a transition, an arc) x 2 X to a propositional formula x (called the presence condition (PC) of x) over the features in F M .
P N L is well-formed if 8 a 2 A • a ) a0 ^ a ) a1 .
As noticed, we use an annotative approach to facilitate the analysis. The approach
relies on the definition of a 150% Petri net that contains all variants of the PNPL, and
the assignment of PCs to its elements, so that a particular Petri net can be obtained
by removing the elements with false PC (so-called negative variability). Instead, other
approaches to SPLs use positive variability [
In Def. 2, the well-formedness condition requires the PC of an arc to be stronger than the PC of its source and target elements. This ensures that, if the arc is present in a product Petri net, its source and target elements will be present as well. Example. Figure 1 shows the PNPL of the flexible assembly line. The 150% Petri net in Figure 1(c) uses dashed regions as a shortcut to assign the same formula to all the elements in the region. For example, formula PartB is attached to transition genB, to place cnvB, and to the arcs from/to place cnvB.
The way to obtain a particular Petri net from a PNPL is by selecting a subset of the features in its feature model. This is called a feature configuration.
with feature model F M = (F, ) is a subset of its features satisfying , i.e., evaluates to true when each variable f 2 is substituted by true when f 2 ⇢ , and by false otherwise. We use P (F M ) = {⇢ i}i2 I for the set of all valid configurations of P N L.
Given a feature configuration, we obtain the corresponding Petri net by removing from the 150% Petri net those elements whose PC is false.
with feature model F M using configuration ⇢ 2 P (F M ) if P N⇢ contains exactly those elements (places, transitions, arcs) from the 150% Petri net whose PCs are satisfied for the features in ⇢ .
We write Prod(PNL) for the set of all derivable Petri nets from the PNPL P N L. Example. Figure 1 admits 36 configurations, each one producing a different Petri net.
Analysing each derivable Petri net of a PNPL one by one can be time-consuming, as the number of Petri nets can be exponential in the number of features in the worst case. Hence, the next section proposes a method to lift the analysis of structural properties to the product line level. 3
In this paper, we focus on the analysis of structural properties of the set of nets that can
be derived from a PNPL P N L. Structural properties depend only on the net topology
and are independent of the initial marking [
As an example, next we provide the definition of the marked graph (MG) property.
In a MG Petri net, each place has exactly one input transition and one output transition,
whereas each transition may have multiple input and output places. Therefore, a MG
allows concurrent and synchronization structures with no conflict.
Definition 5 (Marked graph, from [
This definition permits analysing a Petri net, but we have a product line of them. To improve the efficiency of their analysis, we do not examine each derivable Petri net in P rod(P N L) separately. Instead, we work at the product line level by analysing the PCs in the 150% Petri net to determine if a particular element (place, transition or arc) is in P rod(P N L). For this purpose, first we lift the definition of the MG property to the product line level. A PNPL is a MG if all its derivable nets are MGs. Definition 6 (MG product line). A Petri net product line P N L is a marked graph iff 8 P N⇢ 2 P rod(P N L) • P N⇢ is a marked graph.
In other words, if we can derive from the product line P N L a net that is not a MG, then P N L is not a MG product line. In particular, given a feature configuration ⇢ , a Petri net derivation P N⇢ is not a MG if it has a place p with more than one input transition or more than one output transition. To analyse this without explicitly generating P N⇢ , we extend the elements of the pre- and post-sets of each place p with the PCs of its incoming and outgoing arcs.
Definition 7 (Lifted pre-/post-sets of a place). Given a PNPL P N L = (F M, P N = (P, T , A), ), and a place p 2 P , the lifted pre-set of p is p = {(t, (t,p)) | (t, p) 2 A}, while its lifted post-set is p = {(t, (p,t)) | (p, t) 2 A}.
Remark. In the previous definition, we can use the PC of the arc a instead of the PC of the transition a1 because, according to Def. 2, in a well-formed PNPL, a ) a0 ^ a ) a1 , and so, a ^ a0 ⌘ a ⌘ a ^ a1 .
The size of the lifted pre-set p = {(t0, (t0,p)), ..., (tn, (tn,p))} of a place p will depend on the feature configuration ⇢ . To analyse the MG product line property, we require that its size is one for every possible configuration. This is the case if the following formula is true: p , ( (t0,p) ^ ¬ (¬ (t0,p) ^ ... (¬ (t0,p) ^ ¬ (t1,p) ^ ... ^ ¬ (t1,p) ^ ... ^ ¬ (t1,p) ^ ... ^ (tn,p)) _ (tn,p)) _ (tn,p)) (1)
The formula is made of a disjunction of conjunctions, where only one term in each conjunction can be true. This ensures that, regardless of the configuration, the pre-set of the place will have size one. The lifted post-set of a place p is defined similarly.
This way, a PNPL includes some Petri net that is a MG if there is a feature configuration ⇢ such that for every place p in the PNPL P N L: – p is not in P N⇢ , therefore – p is in P N⇢ , and therefore p is false; or
p and p need to be true. FEATUREIDE
Composer Feature Feature model configuration Property
Analysis
PETRINETS VAR We can express these conditions as the logical formula = (^ p2 P [¬ p _ ( p ^ p ^ p )]. This way, if SAT ( ^ ) (with SAT a predicate that holds if the formula is satisfiable, and the formula of the feature model), then some Petri net in the PNPL is a MG. We can use a constraint solver to obtain a feature configuration that satisfies the formula, if such a configuration exists. The Petri net derived using this feature configuration is ensured to be a MG.
Conversely, the feature configurations that yield nets which are not MGs are those making the formula = (^ p2 P [¬ p _ ( p ^ (¬ p _ ¬ p ))] true.
Example. In the PNPL of Figure 1, the interesting cases are those for places in and ctrl. In the latter case, any Petri net that contains either both transitions inc1 and inc2, or both transitions prod and fix, is not a MG because place ctrl would have either two incoming or two outgoing arcs. This is the case for the Petri nets derived from configurations that select the features Parallel or QualityControl. Similarly, place in will have two incoming arcs for configurations that select the feature QualityControl, and two outgoing arcs for configurations that select the feature Parallel, resulting in nets that are not MGs.
The analysis of other structural properties, like state-machine, free-choice or asymmetric choice, can be lifted in a very similar way. 4
In this section we present a prototype realization of our approach (Section 4.1), and assess the efficiency gain of our analysis w.r.t. an enumerative approach (Section 4.2). 4.1
We have implemented an Eclipse plugin, called Petrinets var, which supports the
presented approach. Figure 2 shows its architecture. Our tool provides two dedicated
editors: one to specify the 150% Petri net, and another to assign PCs to its elements in a
socalled variability mapping model. We use the Eclipse Modeling Framework (EMF) [
3
We rely on FeatureIDE [
Figure 3 shows a screenshot of our tool. The Eclipse project explorer (label 1) contains the FeatureIDE project with the definition of the PNPL used as a running example. This project is configured with our composer and declares the 150% Petri net (file 150mm.petrinets), the feature model (file model.xml that is being edited in the window labelled 2), and the variability model (file annotation.vrb that is being edited in the window labelled 3). As the figure shows, there are dedicated editors for each kind of file. A popup menu on the variability model allows selecting the lifted analysis to perform.
Note that, as a proof of concept, our current implementation uses its own EMF
meta-model to represent 150% Petri nets. This meta-model supports a simple notion
of net like the one we have used in the paper. However, we are planning to use the
standard Petri Net Markup Language (PNML) [
Next, we report on a small-scale experiment to assess the efficiency gain of our lifted analyses, compared to generating all derivable nets in a PNPL and analysing each net separately. In particular, we measure the time for analysing the MG and state-machine (SM) properties.
The experiment uses the example of Structural Lifted analysis Analysis of Figure 1, for which the analyses report analysis of PNPL all products that some Petri nets in the PNPL are nei- Marked graph 38 3356 ther MGs nor SMs. Table 1 shows the State machine 41 4603 average analysis time in milliseconds of running 10 times each analysis, where we Table 1. Analysis time (ms) for MG and SM. discarded the first execution to avoid warmup effects. As it can be observed, both lifted analyses are two orders of magnitude faster than the time to generate and analyse each net in isolation. We expect further efficiency gains with bigger PNPLs (with more features), but performing more experiments is up to future work. 5
The main analysis techniques for Petri nets can be classified into three groups [
There are several mechanisms to model variability for SPL. Most of them can be
classified into annotation-based and composition-based techniques [
Just like us, some works have added variability to Petri nets using SPL techniques.
Feature Petri nets(FN) [
In addition to SPL methods, other techniques to handle variability in Petri nets have
been proposed. Conditional Petri nets [
Concerning SPL analysis of temporal properties, Legay et al. [
Altogether, to the best of our knowledge, there are no previous works on the analysis of structural properties of PNPLs. Our work is a first step in this direction, which we have realized in practice through extensible tooling. 6
In this paper, we propose the notion of Petri net product line, show how to analyse structural properties (specifically the marked graph property) at the product line level, and presented an extensible prototype on top of FeatureIDE.
In the future, we plan to support more types of static analysis techniques, exploit
compositionality of Petri nets in these analyses, and perform more thorough
experiments. Moreover, our idea is to develop a domain-specific language to express such
analyses, which then can be compiled into standard SAT solving procedures. At the
technical level, we will use the PNML meta-model, to ease the connection of our
approach with Petri net tools like CPN Tools [
Work funded by the Spanish Ministry of Science (project MASSIVE, RTI2018-095255B-I00) and the R&D programme of Madrid (project FORTE, P2018/TCS-4314). We thank the anonymous referees for their useful comments.