A method of sample models of program construction in terms of Petri nets

D. I. Kharitonov ; E. A. Golenkov ; G. V. Tarasov ; D. V. Leontyev

Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 4, pp. 563-577.

Résumé

In the article a method of automated construction of Petri nets simulating the behaviour of imperative programs is considered from the formal point of view. Petri net samples with certain characteristics are necessary in programming new algorithms for program analysis; in particular, they can be used for developing or optimizing algorithms of Petri nets compositions and decompositions, building the reachability tree, checking invariants and so on. The generation process consists of two stages. At the first stage, construction templates for a resulting net and parameters for construction are described. With the help of these parameters it is possible to regulate the final size and the absolute or relative amount of certain structures in the resulting net. At the second stage, iterative process of automated net construction is used for Petri net generation of any size, limited only by an available computer memory. In the first section of the article the minimum necessary definitions are given and a new version of Petri nets composition operation by places is introduced. Commutative and associative properties of introduced binary operation allow to synchronize any number of Petri nets in arbitrary order. Then construction template is defined as a marked Petri net with input and output interfaces and rules for templates composition using this interfaces. A number of construction templates can be united in a collection, for which the evolution rules are defined. The completeness property of a collection guarantees that the collection evolution results in a Petri net that simulates the imperative program behavior. The article provides a version of the construction templates complete collection and an example of Petri net simulating sequential imperative program construction. The article is published in the author's wording.

Détail

Keywords: program model, control flow model, Petri net object.

Bibliographie

[1] Peterson J. L., Petri Net Theory and the Modeling of Systems, Prentice Hall, 1981, 290 pp. | MR

[2] Anisimov N. A., Kovalenko A. A., “Towards Petri Net Calculi based on Synchronization via Places”, Proc. of the 1995 IEEE Symposium on Parallel Algorithms/Architecture Synthesis (Aizu-Wakamatsu, Japan, March 1995), IEEE Press, 1995, 264–270

[3] Best E., Devillers R., Koutny M., Petri Net Algebra, Springer-Verlag New York, Inc., USA, 2001 | MR

[4] Investigation of an Accidental Exposure of Radiotherapy Patients in Panama, Report of a Team of Experts (26 May–1 June, 2001), International Atomic Energy Agency, Vienna, Austria, 2001 (PDF)

[5] Anisimov N. A., Golenkov E. A., Kharitonov D. I., “Kompozitsionnal'nyy podkhod k razrabotke parallel'nykh i raspredelennykh sistem na osnove setey Petri”, Programmirovanie, 2001, no. 6, 30–43 (in Russian) | MR | Zbl

[6] Denaro G., Pezzè M., “Petri nets and software engineering”, Lectures on Concurrency and Petri Nets, 3098, Springer-Verlag, 2004, 439–466 | DOI | Zbl

[7] Golenkov E. A., Sokolov A. S., “Metod avtomaticheskogo postroeniya modeli parallel'noy programmy v terminakh setey Petri”, Vychislitel'nye metody i programmirovanie, 6:2 (2005), 77–82 (in Russian)

[8] Mueller R. et al., “Automatic Generation of Simulation Models for Semiconductor Manufacturing”, Proceedings of the 39th Conference on Winter Simulation: 40 Years! The Best is Yet to Come, WSC '07, IEEE Press, Piscataway, NJ, USA, 2007, 648–657

[9] Desel J., “Controlling Petri Net Process Models”, Web Services and Formal Methods, 4th International Workshop, WS-FM (2007, Brisbane, Australia, September 28–29), eds. M. Dumas, R. Heckel, Springer, 2008, 17–30 | DOI

[10] Petrucci L., “Aggregating views for Petri net model construction”, Proc. workshop on Petri Nets and Distributed Systems, PNDS08, associated with Petri Nets 2008, 2008, 17–31

[11] Abdelghani G., Chaabane D., “Modelling Multimedia Synchronization using a Time Petri Net Based Approach”, Advances in Petri Net: Theory and Applications, eds. Tauseef A., Intech, 2010 http://www.intechopen.com/books/advances-in-petri-net-theory-and-applications/modeling-multimedia-synchronization-using-a-time-petri-net-based-approach-

[12] Chen Ming et al., “Petri net models for the semi-automatic construction of large scale biological networks”, Natural Computing, 10:3 (2011), 1077–1097, Springer Netherlands | DOI | MR

[13] Ballarini P. et al., “Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems”, 7th Annual IEEE Conference on Automation Science and Engineering, CASE 2011 (2011)

[14] Alekseyev A. et al., “Improved Parallel Composition of Labelled Petri Nets”, ACSD, eds. Caillaud B., Carmona J., Hiraishi K., IEEE Computer Society, 2011, 131–140

[15] Petko I., Hudák S., “General composition for high level Petri nets and its properties”, Central Europ. J. Computer Science, 2:3 (2012), 222–235 | DOI | Zbl

[16] Durmus M. S., Yildirim U., Soylemez M. T., “Automatic Generation of Petri Net Supervisors for Railway Interlocking Design”, Control Conference (AUCC), 2012 2nd Australian, IEEE, 2012, 180–185

[17] Tarasov G. V., Kharitonov D.I, Golenkov E. A.., “Ob odnom predstavlenii funktsii v modeli imperativnoy programmy, zadannoy setyami Petri”, Modelirovanie i analiz informatsionnykh sistem, 18:2 (2011), 18–38 (in Russian)

[18] Kharitonov D., Tarasov G., “Modeling function calls in program control flow in terms of Petri Nets”, ACSIJ Advances in Computer Science: an International Journal, 3:6, No 12 (November 2014), 82–91

[19] Sunanda B. E., Seetharamaiah P., “Modeling of Safety-Critical Systems Using Petri Nets”, SIGSOFT Softw. Eng. Notes, 40:1 (2015), 1–7 | DOI

[20] Kordon F. et al., Complete Results for the 2015 Edition of the Model Checking Contest, , 2015 http://mcc.lip6.fr/2015/results.php