Communications of the ACM
Home/Magazine Archive/June 2015 (Vol. 58, No. 6)/Colored Petri Nets: A Graphical Language For Formal.../Full Text
Contributed articles
Colored Petri Nets: A Graphical Language For Formal Modeling and Validation of Concurrent Systems
Credit: xtremetips.com
The vast majority of IT systems today can be characterized as concurrent and distributed in that their operation inherently relies on communication, synchronization, and resource sharing between concurrently executing software components and applications. This development was accelerated first through the pervasive presence of the Internet as a communication infrastructure and more recently by cloud- and Web-based services, mobile applications, and multicore computing architectures.
Colored Petri Nets, or CPNs, combine Petri nets with a programming language to obtain a scalable modeling language for concurrent systems. Petri nets provide the formal foundation for modeling concurrency and synchronization; a programming language provides the primitives for modeling data manipulation and creating compact and parameterizable models. In this article, we offer an example-driven introduction to the core syntactical and semantical constructs of the CPN modeling language and survey how quantitative and qualitative behavioral properties of CPN models can be validated through simulation-based performance analysis and explicit state-space exploration. We also give an overview of CPN Tools that provide software-tool support for the practical use of CPNs and pointers to projects where CPN technology has been put to practical use in an industrial setting. As we proceed, we give a historical perspective on the research contributions that led to development of CPN technology.
Key Insights
History of Colored Petri Nets
Development of CPNs was initiated in the early 1980s when distributed systems were becoming a major paradigm for future computing systems. The goal of the CPN modeling language has been to develop a formally founded modeling language for concurrent systems that would make it possible to formally analyze and validate concurrent systems and that, from a modeling perspective, scale to industrial systems. A main motivation behind the research into CPNs (and many other formal modeling languages) was that the engineering of correct concurrent systems is a challenge due to their complex behavior that could result in subtle bugs if not designed with care. As concurrent systems become still more pervasive and critical to society, formal techniques for concurrent systems were (and still are) a highly relevant technology to support engineering of reliable concurrent systems. Many formal modeling languages for concurrent systems have been developed, including Statecharts,10 Timed Automata,1 and Promela.11
At their origin, CPNs build on Petri nets (see the first sidebar "Petri Nets") as introduced by Carl Adam Petri in his doctoral thesis published in 196221 as a formalism for concurrency and synchronization. Petri's introduction of Petri nets was far ahead of the time distributed systems would be invented and computers begin to have parallel processes. At that time, programs and processing were considered sequential and deterministic. It was thus extremely visionary of Petri to predict the importance of being able to understand and characterize the basic concepts of concurrency. In Petri nets, actions are (implicitly) concurrent unless (explicitly) synchronized; this is in contrast to many other modeling formalisms where concurrency must be introduced explicitly using parallel composition operators. A further advantage of Petri nets is they rely on few basic concepts yet are still able to model a range of communication and synchronization concepts and patterns.
In the decade following their introduction, Petri nets were widely accepted as one of the most well-founded theories to describe important behavioral concepts, including concurrency, conflict, nondeterminism, synchronization, and resource sharing. Petri nets were also used to model and analyze smaller concurrent systems. However, practical use soon revealed a serious shortcoming: Petri nets (in their basic form) do not scale to large systems unless the system is modeled at a very high level of abstraction. The primary reason for this lack of scalability is that basic Petri nets are not well suited for modeling systems in which data and manipulation of data play a crucial role. Furthermore, Petri nets did not provide concepts that would make it easy to scale models according to some system parameter (such as increase the number of servers in a modeled system) without having to make major changes to the model. This trade-off implied the use of Petri nets for practical modeling was declining. As a remedy, many researchers proposed ad hoc extensions to Petri nets. These extensions created a large variety of Petri net modeling languages. Many ad hoc extensions were not well defined and, even when they were, often had fundamental theoretical problems. Whenever a new ad hoc extension was introduced, all the basic concepts and analysis methods had to be redefined to apply for the extended Petri net language (with ad hoc extension). With the invention of the first (text-based) computer tools to support analysis of Petri net models, the situation became prohibitive. Whenever a new ad hoc extension was introduced (to handle a modeling shortcoming) all existing computer tools became void and could be used only after time-consuming and error-prone reprogramming. Hence, there was an urgent need to develop a class of Petri nets general enough to handle a large variety of different application areas without having to make ad hoc extensions.
The first successful step toward a common more-powerful class of Petri nets was taken by Hartmann Genrich and Kurt Lautenbach in 1979 with the introduction of predicate/transition, or PrT, nets.8 Their work was inspired by earlier work on transition nets with "colored tokens" by Michael Schiffers and Horst Wedde23 and transition nets with "complex conditions" by Robert M. Shapiro.24 The basic idea behind PrT nets was to introduce a set of colored tokens that can be distinguished from one another, unlike the indistinguishable black tokens in basic Petri nets. It was thus possible to model different processes in a single subnet. PrT nets used arc expressions to define how transitions can occur in different ways (occurrence modes) depending on the colors of input and output tokens. The invention of colored distinguishable tokens in PrT nets was a significant step forward but still involved limitations. PrT nets had only one set of token colors, and all places had to use this set (or Cartesian products based on this set).
The second step toward a more general class of Petri nets was taken by Kurt Jensen in his Ph.D. thesis in 1980 with the introduction of the first kind of CPNs.14 This Petri net model allowed the modeler to use a number of different color sets, making it possible to represent data values in a more intuitive way instead of having to encode all data into a single shared set. It later turned out to be convenient to define the color sets by means of data types known from programming languages (such as products, records, lists, and enumerations). Use of data types had three implications: Token colors became structured (and hence much more powerful); type checking became possible (making it much easier to locate modeling errors); and color sets, arc expressions, and guards could be specified by the well-known and powerful syntax and semantics known from programming languages. Use of data types gave the modeler a convenient way to handle complex data and specify the often-complex interaction between data and system behavior.
A third step forward was taken by Huber et al. in 1990 with the introduction of hierarchical CPNs,12 work heavily inspired by the hierarchy concepts in the Structured Analysis and Design Technique (SADT) developed by Marca and McGowan.18 It was Shapiro of Huber et al. who proposed to port the SADT hierarchy concepts to CPNs. Introduction of hierarchical CPNs allowed the modeler to structure a large CPN model into a number of interacting and reusable modules in a way that is similar to how modules are used in programming languages. Development of hierarchical CPNs implied that Petri net models of large systems became much more tractable, as they could be split into modules of reasonable size, and the model could be viewed at different levels of abstraction.
The CPN Language
To give an informal introduction to the concepts of CPNs, we use a CPN model of a distributed two-phase commit transaction system; for more on the formal definition of CPNs, see the CPN lecture book by Jensen and Kristensen.16 The CPN model of the two-phase commit system consists of four modules hierarchically organized into three levels; Figure 1 outlines the top-level module, which consists of two "substitution transitions" (drawn as rectangles with double-lined borders) representing the Coordinator and the Workers in the system. Each substitution transition has an associated "submodule" that models the detailed behavior of the coordinator and the workers, respectively. Substitution transitions constitute a purely syntactical structuring mechanism and do not occur (execute) when CPN models are executed.
The two substitution transitions are connected via directed "arcs" to the four places: CanCommit, Votes, Decision, and Acknowledge (drawn as ellipses). Places connected to substitution transitions are called "socket places" and are linked to "port places" in the associated submodules (to be discussed shortly). The coordinator and the workers interact by producing and consuming "tokens" on the places. These tokens carry data values; the type of tokens that may reside on a place is determined by the "type" of the place (written in text below the place). For historical reasons, the types of places are called "color sets"; Figure 2 lists the definitions of the color sets used for the four places in Figure 1. These color sets are defined using the CPN ML programming language, which is based on the functional language Standard ML.19
The symbolic constant W is used to specify the number of worker processes considered. The Worker color set is an indexed type consisting of the values wrk(1),wrk(2) ... wrk(W) used to model the identity of the worker processes. The color set Vote is an enumeration type containing the values Yes and No and used to model that a worker may vote yes or no to commit the transaction. The color set WorkerxVote is a product type containing pairs consisting of a worker and its vote. The color set Decision is an enumeration type used to model whether the coordinator decides to Abort or Commit the transaction; only if all workers vote yes will the transaction be committed. Note that in addition to the type constructors introduced here, CPN ML supports union, list, and record types. The variables w and vote declared in Figure 2 are discussed later.
The state of a CPN model is called a "marking" and consists of a distribution of "tokens" on the places of the model. Each place may hold a (possibly empty) "multi-set" of tokens with data values (colors) from the color set of the place. The "initial marking" of a place is specified above each place (omitted if the initial marking is the empty multi-set). For the places in Figure 1, all places are empty in the initial marking. Initially, the "current marking" of a CPN model equals the initial marking. When a CPN model is executed "occurrences" of "enabled" transitions consume and produce colored tokens on the places changing the current marking of the CPN model.
The Coordinator module (see Figure 3) is the submodule associated with the Coordinator substitution transition in Figure 1. The places CanCommit, Votes, Decision, and Acknowledge are "port places," as indicated by the rectangular In and Out tags positioned next to them. These places are linked to the identically named socket places in the top-level module in Figure 1 via a "port-socket association," implying any tokens added (removed) from a port place by transitions in the Coordinator module will also be added (removed) in the marking of the associated socket place in the top-level module.
The places Idle, WaitingVotes, and WaitingAcknowledgements are used to model the states of the coordinator when executing the two-phase commit protocol. The places Idle and WaitingVotes have the color set UNIT containing just a single value ()(denoted unit). Initially, the coordinator is in an idle state, as modeled by the initial marking of place Idle, which consists of a single token with the color unit. In CPN ML this is written as 1'( ) specifying one (1) occurrence of (') the unit color (()). The number of tokens on a place in the current marking is indicated with a small circle positioned next to a place, and the details of the colors of the tokens are provided in an associated text box.
The transitions SendCanCommit, CollectVotes, and ReceiveAcknowledgements model the events/actions that cause the coordinator to change state. The coordinator will first send a can commit message (transition SendCanCommit) to each worker asking whether the workers can commit the transaction. It will then collect the votes from all workers and send a decision to the workers that voted yes indicating whether the transaction is to be committed or not (substitution transition CollectVotes). Finally, the coordinator will receive an acknowledgment from each worker that voted yes, confirming the worker received the decision (transition ReceiveAcknowledgements). Note CollectVotes is a substitution transition, meaning the details of how the coordinator collects votes are modeled by the associated CollectVotes submodule. This illustrates the mixed use of ordinary and substitution transitions within a module. We omit the details of CollectVotes in this article.
In the current marking in Figure 3, only the transition SendCanCommit is enabled, as indicated by the thick border of that transition. The requirements for a transition to be "enabled" are determined from the "arc expressions" associated with the incoming arcs of the transition. In this case, only a single incoming arc is from place Idle containing the expression (). This expression specifies that for SendCanCommit to be enabled, there must be at least one ()-token present on Idle. When the SendCanCommit transition occurs, it consumes a ()-token from place Idle and produces tokens on places connected to output arcs, as determined by "evaluating" the arc expressions on output arcs. In this case of the SendCanCommit transition, the expression () on the arc to WaitingVotes evaluates to a single ()-token. The expression Worker.all() on the arc to CanCommit is a call to the function Worker.all that takes a unit value (()) as parameter and returns all colors of the color set Worker. The use of Worker.all() as arc expression illustrates how complex calculations can be encapsulated within function calls. The calculations within functions may use complex data values and involve multi-sets of tokens such that several tokens can be added/removed by a single transition occurrence without introducing intermediate states.
Figure 4 outlines the marking of the surrounding places of transition SendCanCommit after the occurrence of SendCanCommit, showing the place CanCommit contains two tokens—one for each worker in the system—representing messages going to the two worker processes. The coordinator has now entered a state in which it is waiting to collect votes from the worker processes.
Figure 5 is the Workers module, which is the submodule of the Workers substitution transition in Figure 1. The places CanCommit, Votes, Decision, and Acknowledge constitute the port places of this module and are linked to the identically named socket places in Figure 1. The places Idle and WaitingDecision model the two states of worker processes. Each place has the color set Worker. A wrk(i)-token on, say, the place Idle reflects that the i-th worker is in state idle. This modeling approach makes it possible to model the states of all workers in a compact manner within a single module without having to have a place for each worker or a module instance for each worker. All workers are initially in the idle state, as represented by corresponding tokens on place Idle in the initial marking. The transition ReceiveCanCommit models the reception of can-commit messages from the coordinator and the sending of a vote. The transition ReceiveDecision models the reception of a decision message from the coordinator and the sending of an acknowledgment.
The current marking of place CanCommit in Figure 5 is 1'wrk (1) ++ 1'wrk(2) modeling a marking where the coordinator has sent a can-commit message to each worker. The arc expressions on the surrounding arcs of the ReceiveCanCommit transition are more complex than the arc expressions of the SendCanCommit transition in the Coordinator module considered earlier in that they contain the "free variables" w and vote defined in Figure 2. This means in order to talk about the enabling and occurrence of transition ReceiveCanCommit, values must be bound (assigned) to w and vote in order to evaluate the input and output arc expressions. This is done by creating a "binding" that associates a value to each of the free variables occurring in the arc expressions of the transition. Bindings can be considered different "modes" in which a transition may occur. As w is of type Worker and vote is of type Decision, this yields the bindings listed in Figure 6, reflecting that each of the two workers may vote Yes or No to committing the transactions.
A binding of a transition is enabled if evaluating each input arc expression in the binding results in a multi-set of tokens, which is a subset of the multi-set of tokens present on the corresponding input place; as an example, consider the binding b1Y for transition ReceiveCanCommit. Evaluating the input arc expression w on the input arc from Idle results in the multi-set containing a single token with the color wrk(1) contained in the multi-set of tokens present on place Idle in the marking in Figure 5, similarly for the input arc expression on the arc from place CanCommit. This means that binding b1Y is enabled and may occur. In fact, all four bindings listed in Figure 6 are enabled in the marking in Figure 5.
The tokens produced on output places when a transition occurs in an enabled binding are determined by evaluating the output arc expressions of the transition in the given binding. Consider again the binding b1Y for transition ReceiveCanCommit. The output arc expression (w,vote) evaluates to (wrk(1),Yes), and this token will be added to place Votes to inform the coordinator that worker one votes yes to committing the transaction. The arc expression on the arc from ReceiveCanCommit to WaitingDecision is an if-then-else expression that in the binding b1Y evaluates to the multi-set 1'wrk(1) that will be added to the tokens on place WaitingDecision. The if-then-else expression on the arc from ReceiveCanCommit to Idle evaluates to the empty multi-set; hence, no tokens will be added to place Idle in this case. Figure 7 outlines the marking resulting from an occurrence of the b1Y binding.
The occurrence of the binding b1N representing that worker one votes no would have the effect of removing a wrk(1)-token from Idle, adding a (wrk(1),No)-token to Votes, adding no tokens to place WaitingDecision, and adding a wrk(1)-token to place Idle. This models the fact that if a worker votes no to committing the transaction, it then goes back to Idle; whereas if it votes yes, it will then go to WaitingDecision. As this is a distributed system, a worker cannot know the vote of another worker without exchanging messages.
All four bindings listed for transition ReceiveCanCommit are enabled in the marking shown in Figure 5. Enabled bindings may be "concurrently enabled" if each binding can get its required tokens from each input place independently of the other enabled bindings in the set. As an example, the bindings b1Y and b2Y are concurrently enabled since each binding can get its tokens from the input places without sharing with each other. Such access to tokens reflects that the workers are executing concurrently and may simultaneously send a vote back to the coordinator. In contrast, the bindings b1Y and b1N are not concurrently enabled. These two bindings are in "conflict" because they each need the single wrk(1)-token on Idle (and also the single wrk(1)-token on place CanCommit). The notion of concurrency and conflicts of bindings extends to bindings of different transitions. A concurrently enabled set of bindings can be executed in any interleaved order, and the resulting marking will be the same, independent of the interleaved execution considered, a property inherited from basic Petri nets.
So far, we have used relatively simple arc expressions. In general, arc expressions can be any expression that can be written in Standard ML as long as they have types that match the corresponding places. In particular, arc expressions may apply functions, including higher-order functions.
Unfolding and Folding
By adding data types, a programming language, and modules, CPNs improve practical modeling power, making it feasible to create models of complex real systems. PTNs extended with inhibitor arcs allowing a test for zero tokens on a place can already simulate Turing machines; hence, the CPN extensions do not add expressive power, from a theoretical perspective. Moreover, any hierarchical CPN model can be unfolded to a nonhierarchical CPN model that in turn can be unfolded to a behaviorally equivalent PTN model. In the other direction, any PTN model, including one with inhibitor arcs, can be folded into a CPN model with a single module consisting of a single place and a single transition. In practice, such folding is not interesting, as the arc expressions will be extremely complex and not interpretable by a human. However, the fact that the unfolding and folding exist shows hierarchical CPNs have the same behavioral properties as basic Petri nets, and hence constitute a solid model for concurrency, conflict, synchronization, and resource sharing.
The unfolding of a hierarchical CPN to a nonhierarchical CPN consists of recursively replacing each substitution transition with its associated submodule such that associated port and socket places are merged into a single place. The unfolding of a nonhierarchical CPN to a PTN consists of unfolding each CPN place to a PTN place for each color in the color set of the CPN place and unfolding each CPN transition to a PTN transition for each possible binding of the CPN transition. To illustrate the unfolding, consider the subnet in Figure 4. To represent this CPN subnet as a PTN, the CPN place CanCommit must be unfolded to two PTN places corresponding to wrk(1) and wrk(2). The places Idle and WaitingVotes do not need to be unfolded, as the unit color set contains only a single value. Figure 8 shows the equivalent PTN; arc expressions are replaced by arc weights, and the initial marking is replaced by a single token initially in Idle.
To show the unfolding of a CPN transition, consider the CPN subnet in Figure 7. To represent it as a PTN, the places must be unfolded, as explained in the previous paragraph and, in addition, the transition ReceiveCanCommit must be unfolded to a PTN transition for each of the four bindings listed in Figure 6. Figure 9 outlines the equivalent PTN; arc weights have been omitted, as all are 1; the marking shown is the initial marking.
We have outlined how to unfold two CPN subnets into PTN subnets. For larger color sets, the unfolding yields an explosion in size, since there will be a PTN place for each color of a CPN place and a PTN transition for each binding of a CPN transition. For our CPN model the modeler just needs to change the symbolic constant W (defined in Figure 2) to configure the model to handle, say, five workers. With basic Petri nets the modeler would need to add places, transitions, and arcs and hence change the net structure. This example shows CPNs—unlike basic Petri nets—provide the means for creating compact parameterizable models.
Tools and Applications
The construction and analysis of CPN models are supported by two generations of software tools: Design/CPN6 and CPN Tools.28 They have been instrumental in CPN success, as they enable the practical use in a broad range of domains, including distributed software systems, communication protocols, embedded systems, and process and workflow modeling. Design/CPN and CPN Tools both work directly on the high-level representation of CPN models and do not perform unfolding to the underlying PTN model, as discussed earlier. For a comprehensive list of more than 100 papers describing practical applications and domains see the web-pages of the CPN group at Aarhus University, Denmark.13
The Design/CPN tool6 was created by Meta Software, Cambridge, MA, starting in 1988. Kurt Jensen, Robert M. Shapiro, and Peter Huber were the main architects, and the implementation was carried out with an international group of researchers. The first version of Design/CPN supported modeling, syntax checking, and interactive simulation. Introduction of hierarchical CPNs supported by the Design/CPN tool advanced the practical use of Petri nets. The new modeling language and its tool support were general and powerful enough to eliminate the need for making ad hoc extensions, as discussed earlier. A common platform for practical modeling was established and used by most Petri net practitioners, as supported by Jensen's three-volume monograph on CPNs, 1992–1997.15
Starting in 2000, a second generation of tool support, called CPN Tools,28 was designed and implemented at Aarhus University. The main architects were Kurt Jensen, Søren Christensen, and Michael Westergaard. The design was based on empirical studies of the use of Design/CPN, making the new tool much easier and more efficient to use when constructing CPN models. In 2010, CPN Tools had 10,000 licenses in 150 countries. At the time, development and maintenance of the tool set were transferred to the group of Wil van der Aalst at the Technical University of Eindhoven, the Netherlands.28 New updates with improved functionality continue to be distributed on a regular basis.
CPN Tools supports editing and construction of CPN models, interactive and automatic simulation, state space-based model checking (see the second sidebar "State Spaces and Model Checking"), and simulation-based performance analysis (see the third sidebar "Timed Models and Performance Analysis"). CPN Tools is based on a much faster simulation engine developed by Bisgaard et al.20 With this simulation engine, many models run more than 1,000 times faster compared to Design/CPN, allowing complex automatic simulations to be executed within seconds instead of hours.
Figure 10 is a screenshot of CPN Tools with the CPN model of the two-phase commit transaction system. The modeler works directly with the graphical representation of the CPN model through a user interface based on such interaction techniques as "tool palettes" and "marking menus." The rectangular area to the left is an "index" that includes the Tool box for the user to manipulate the declarations and modules. The rest of the screen is the "workspace," which, in this case, contains two "binders" (the rectangular windows) and a circular pop-up menu. The binder to the left contains the Commit module, and the binder to the right contains the Coordinator module. In addition are two tool palettes: one—Sim—containing the tools that can be used for simulation of the model, the other—Create—containing the tools for creating CPN model elements. A circular marking menu appears on top of a transition to provide the operations that can be performed on a transition.
The modeler works directly with the graphical representation of the CPN model through a user interface based on such interaction techniques as "tool palettes" and "marking menus."
CPN Tools performs syntax and type checking, and contextual error messages are provided to the user. The syntax check and code generation are incremental and performed in parallel with editing. This means it is possible to execute parts of a CPN model even if the model is not complete and that when parts of a CPN model are modified a syntax check and code generation are performed only on the elements that depend on the parts that were modified. CPN Tools supports two types of simulation: interactive and automatic. In an "interactive" simulation, the user is in complete control and determines the individual steps in the simulation, selecting among the enabled bindings in the current state. CPN Tools shows the effect of executing a selected binding in the graphical representation of the CPN model. In an "automatic simulation," the user specifies the number of steps to be executed and/or sets a number of stop criteria and breakpoints. The simulator then automatically executes the model without user interaction by making random choices among the enabled bindings in the states encountered. Only the resulting state is shown, but information about the executed steps can be collected in various ways. CPN Tools also includes support for domain-specific graphical feedback from simulations developed by Westergaard and Lassen.30
Conclusion
Research into CPNs is driven by simultaneous focus on theoretical development, design, and implementation of software-tool support, as well as practical application and case studies and their mutual influence on one another. A theoretical foundation is needed to develop semantically sound software tools that are in turn needed for practical applications that reveal limitations of the theoretical foundation.
Creation of the CPN language can be divided into four steps reflecting many similarities with developments in programming languages. The first, from the black tokens of basic Petri nets to colored tokens in PrT nets, corresponds to the step from bit representation to simple data types. The second, from PrT nets to CPNs, corresponds to the introduction of structured data types and type checking. The third, with the introduction of hierarchical CPNs, corresponds to the introduction of structuring concepts like modules, procedures, functions, and subroutines. The fourth, represented by development of Design/CPN and CPN Tools, corresponds to the implementation of compilers and runtime systems that are essential for practical applications.
In addition to CPNs, several other variants of high-level Petri nets and supporting computer tools have been developed based on the idea of extending Petri nets with data types. One example is Well-Formed Nets (WFNs),4 as supported by the CosyVerif tool. WFNs put rather strong restrictions on the color sets and associated operations to facilitate space-efficient exploration of state spaces in which the nodes correspond to equivalence classes of states instead of single states. Concurrent Object-Oriented Nets,2 as implemented in the COOPNBuilder tool, incorporate object-oriented concepts into Petri nets and rely on Algebraic Petri Nets (APNs)22 for specification of data types and inscriptions. APNs are high-level Petri nets in which algebraic abstract data types are used for giving semantics to the inscriptions. Reference Nets (RNs)25 are high-level Petri nets targeting agent-oriented object systems in which the tokens themselves may constitute references to other Petri net models. RNs are supported by the Renew tool, using Java as the inscription language. Stochastic Well-formed Nets,5 as supported by the GreatSPN tool, enable performance evaluation based on Markov chains. Billington3 developed an international standard for high-level Petri nets that was approved in 2004. The high-level Petri net standard was heavily based on CPNs that conform to the standard.
Here, we have provided an overview and introduction to the CPN language and its tool support and discussed the research development that led to the CPN modeling language as it exists today. The most recent monograph on CPNs was published by Jensen and Kristensen in 2009,16 providing an in-depth but compact introduction to modeling and validation of concurrent systems through CPNs. It introduced the constructs of the CPN modeling language, presented its analysis methods, and provides a comprehensive road map to the practical use of CPNs. Moreover, it presented selected industrial case studies illustrating the practical use of CPNs for design, specification, simulation, and verification in a variety of application domains. It was aimed at use in university courses17 and self-study.
Acknowledgments
We are indebted to the many colleagues and researchers who have contributed to the development of CPNs. In addition to those mentioned here, Jawahar Malhotra had the idea to use the Standard ML language, Ole Bach Andersen implemented the graphical interface of Design/CPN, and Søren Christensen implemented the binding inference algorithms. Hartmann Genrich contributed to Design/CPN with knowledge and experience from PrT nets. The graphical user interface of CPN Tools was designed together with Michel Beaudouin-Lafon and Wendy McKay.
References
1. Alur, R. and Dill, D. A Theory of timed automata. Theoretical Computer Science 126, 2 (Apr. 1994), 183–235.
2. Biberstein, O., Buchs, D., and Guelfi, N. Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism. In Concurrent Object-Oriented Programming and Petri Nets - Advances in Petri Nets, Lecture Notes in Computer Science 2001. Springer-Verlag, Berlin-Heidelberg, 2001, 73–130.
3. Billington, J. ISO/IEC 15909-1:2004, Software and System Engineering - High-Level Petri Nets - Part 1: Concepts, Definitions and Graphical Notation. ISO/IEC, Switzerland, Dec. 2004; http://www.iso.org/iso/home/store/catalogue_tc/catalogue_detail.htm?csnumber=38225
4. Chiola, G., Dutheillet, C., Franceschinis, G., and Haddad, S. On well-formed coloured nets and their symbolic reachability graph. Chapter 13 in High-Level Petri Nets, Springer-Verlag, Berlin-Heidelberg, 1991, 373–396.
5. Chiola, G., Dutheillet, C., Franceschinis, G., and Haddad, S. Stochastic well-formed coloured nets and symmetric modelling applications. IEEE Transactions on Computers 42, 11 (Nov. 1993), 1343–1360.
6. Christensen, S., Jørgensen, J.B., and Kristensen, L.M. Design/CPN: A computer tool for coloured Petri nets. In Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems (Enschede, the Netherlands, Apr. 2–4) Lecture Notes on Computer Science 1217. Springer-Verlag, Berlin-Heidelberg, 1997, 209–223.
7. Christensen, S., Kristensen, L.M., and Mailund, T. A sweep-line method for state space exploration. In Proceedings of the Seventh International Conference on Tools and Algorithms for Construction and Analysis of Systems (Genova, Italy, Apr. 2–6) Lecture Notes on Computer Science 2031. Springer-Verlag, Berlin-Heidelberg, 2001, 450–464.
8. Genrich, H. and Lautenbach, K. System modelling with high-level Petri nets. Theoretical Computer Science 13, 1 (1981), 109–136.
9. Girault, C. and Valk, E., Eds. Petri Nets for Systems Engineering. Springer-Verlag, Berlin-Heidelberg, 2003.
10. Harel, D. Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 3 (June 1987), 231–274.
11. Holzmann, G. The SPIN Model Checker. Addison-Wesley, 2003.
12. Huber, P., Jensen, K., and Shapiro, R. Hierarchies in coloured Petri nets. In Advances in Petri Nets 1990, Lecture Notes on Computer Science 483. Springer-Verlag, Berlin-Heidelberg, 1991, 313–341.
13. Jensen, K. et al. Industrial Use of Coloured Petri Nets. CPN group at Aarhus University, Denmark; http://www.cs.au.dk/CPnets/industrialex/
14. Jensen, K. Coloured Petri nets and the invariant method. Theoretical Computer Science 14, 3 (1981), 317–336.
15. Jensen, K. Coloured Petri Nets. Vols. 1–3: Basic Concepts, Analysis Methods, Practical Use. Monographs in Theoretical Computer Science. Springer-Verlag, Berlin-Heidelberg, 1992–1997.
16. Jensen, K. and Kristensen, L.M. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer-Verlag, Berlin-Heidelberg, 2009; http://www.cpnbook.org
17. Kristensen, L.M. and Jensen, K. Teaching modelling and validation of concurrent systems using coloured Petri nets. In Transactions on Petri Nets and Other Models of Concurrency I, Lecture Notes in Computer Science 5100 (Aug. 2008), 19–34.
18. Marca, D. and McGowan, C. SADT: Structured Analysis and Design Technique. McGraw-Hill, New York, 1988.
19. Milner, R., Tofte, M., Harper, R., and MacQueen, D. The Definition of Standard ML. MIT Press, Cambridge, MA, 1997.
20. Mortensen, K.H. Efficient data structures and algorithms for a coloured Petri nets simulator. In Proceedings of the Third Workshop and Tutorial on Practical Use of Colored Petri Nets and CPN Tools (Aarhus, Denmark, Aug. 29–31). Department of Computer Science, University of Aarhus, Denmark, 2001, 57–74.
21. Petri, C.A. Kommunikation mit Automaten, Schriften des Instrumentelle Mathematik (IIM) 2, Technical Report. Institut für Instrumentelle Mathematik, Bonn, Germany, 1962.
22. Reisig, W. Petri nets and algebraic specifications. Theoretical Computer Science 80, 1 (Mar. 1991), 1–34.
23. Schiffers, M. and Wedde, H. Analyzing program solutions of coordination problems by CP-nets. In Proceedings of Seventh Symposium of Mathematical Foundations of Computer Science (Zakopane, Poland, Sept. 4–8), Lecture Notes in Computer Science 64. Springer-Verlag, Berlin-Heidelberg, 1978, 462–473.
24. Shapiro, R. Towards a Design Methodology for Information Systems, Technical Report. In Petri, C.A.: Ansätze zur Organisationstheorie rechnergestützter Informationssysteme, 1978.
25. Valk, R. Object petri nets: Using the nets-within-nets paradigm. In Advances in Petri Nets, Lecture Notes on Computer Science 3098. Springer-Verlag, Berlin-Heidelberg, 2004, 819–848.
26. van der Aalst, W. Interval timed coloured Petri nets and their analysis. In Proceedings of the 14th International Conference on Application and Theory of Petri Nets (Chicago, June 21–25), Lecture Notes on Computer Science 691. Springer-Verlag, Berlin-Heidelberg, 1993, 453–472.
27. Wells, L.M. Performance analysis using CPN tools. In Proceedings of the First International Conference on Performance Evaluation Methodologies and Tools (Pisa, Italy, Oct. 11–13), Vol. 180 of ACM Conference Proceeding Series. ACM Press, New York, 2006, article no. 59.
28. Westergaard, M. et al. CPN tools for editing, simulating, and analysing coloured Petri nets. In Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (Eindhoven, the Netherlands, June 23–27) Lecture Notes on Computer Science 2679. Springer-Verlag, Berlin-Heidelberg, 2003, 450–462; see also http://www.cpntools.org
29. Westergaard, M., Evangelista, S., and Kristensen, L.M. ASAP: An extensible platform for state space analysis. In Proceedings of 30th International Conference on Application and Theory of Petri Nets (Paris, June 22–26) Lecture Notes on Computer Science 5606. Springer-Verlag, Berlin-Heidelberg, 2009, 303–312.
30. Westergaard, M. and Lassen, K. The BRITNeY suite animation tool. In Proceedings of the 27th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Turku, Finland, June 26–30) Lecture Notes on Computer Science 4024. Springer-Verlag, Berlin-Heidelberg, 2006, 431–440.
Figures
Figure 1. The top-level module of the CPN model.
Figure 2. Definition of color sets used in Figure 1.
Figure 3. The Coordinator module.
Figure 4. Current marking after SendCanCommit.
Figure 6. Bindings of transition ReceiveCanCommit.
Figure 7. Current marking after ReceiveCanCommit.
Figure 8. PTN representation of the CPN in Figure 4.
©2015 ACM 0001-0782/15/06
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and full citation on the first page. Copyright for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or fee. Request permission to publish from [email protected] or fax (212) 869-0481.
The Digital Library is published by the Association for Computing Machinery. Copyright © 2015 ACM, Inc.
Comments
Dmitry Zaitsev
In CPN Tools, we built models for manifold networking technologies: Provider Backbone Bridge, Ethernet, IP, MPLS, Bluetooth, E6, Dynamic Routing etc which are delivered via the tools website http://cpntools.org/documentation/examples/start We use CPN Tools as GPSS for performance evaluation. Undoubtable benefits consist in vivid graphical language enriched with the functional programming language ML. For modeling new networking technologies we find CPN Tools even more flexible than ns. For processing of statistical information on-fly we supplement models with special measuring subnets.
Dmitry Zaitsev
http://member.acm.org/~daze
Displaying 1 comment