Abstract
Aviation and aerospace systems are complex and concurrent and require special tools for their specification, verification, and performance evaluation. The tool in demand should be easily integrated into the standard loop of model-driven development. Colored Petri nets represent a combination of a Petri net graph and a functional programming language ML that makes it powerful and convenient tool for specification of real-life system and solving both tasks: correctness proof i.e. verification and performance evaluation. This chapter studies basic and advanced features of CPN Tools – a powerful modeling system which uses graphical language of colored Petri nets. Starting with a concept of colored hierarhical timed Petri net, it goes through declaration of color sets and functions to peculiarities of hierarchical design of complex models and specification of timed characteristics. The authors accomplish the chapter with a real-life case study of performance evaluation for switched Ethernet network.
TopBackground
Petri nets represent a unification of a graphical language introduced by Frank and Lillian Gilbreth for production processes specification. Their most significant advantage consists in the possibility of applying formal methods for their analysis. Though, general Petri nets are too abstract to be a convenient tool for a specialist in some application area. Developed by Jensen and Kristensen (2009) colored Petri nets are loaded by a functional programming language that makes their application less laborious and more concise. A colored Petri net represents a computationally universal system that allows their wide application not only for specification and modeling but for programming and control as well.
Dodd (2006) started a professional application of colored Petri nets for modeling in an avionics mission computer. Then a few works appeared which develop the application of colored Petri nets in the aviation and aerospace industries with modeling a landing detector (Kordon, 2016), auto flight control system (Bourdil et al, 2016) and others.
The authors of this chapter have gained a strong experience in colored Petri nets with teaching them for more than a decade, developing enterprise-level models, and applying them in research projects. The first paper (Zaitsev, 2004) that develops a switched Ethernet model represents a personal record of citation. Note that, the modern avionics protocol AFDX (ARINC, 2009) represents a specialization of a general switched Ethernet technology. Then a series of papers have been published which present models of MPLS networks (Zaitsev & Sakun, 2008), develop a new parametric modeling paradigm (Zaitsev & Shmeleva, 2009), and analyze threats in modern computing grids (Zaitsev et al, 2014) and (Zaitsev et al, 2016). Supplied with the measuring fragments, the technique was presented for the first time in (Zaitsev, 2004) and further developed with recent works, our library of models represents a condensed experience and is distributed via official site of CPN Tools http://cpntools.org.
Key Terms in this Chapter
Multiset: A set of elements supplied with their multiplicities (for example, two books and three pencils).
Altitude Switch (ASW): A facility to wake up a device of interest in case the altitude value is less than a given threshold.
Measuring Fragment: A part of a colored petri net which calculates statistical characteristics directly in the process of simulation.
Avionics Full-Duplex Switched Ethernet Network (AFDX): A modern standard for avionics data transmission based on switched Ethernet technology.
Airlines Electronic Engineering Committee (ARINC): ARINC-429 is a standard for avionics data transmission based on a point-to-point one-way connection via twisted pair.
Meta Language (ML): A functional programming language.
State Space: A set of valid marking of a petri net and transitions between them.
Colored Petri Net (CPN): A combination of a petri net graph and a functional programming language ML.
Petri Net: A directed bipartite graph with a dynamic process defined on it.