maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2015-4-563-577mais-273Research ArticleОригинальные статьиArticlesМетод генерации примеров моделей программ в терминах сетей ПетриA Method of Sample Models of Program Construction in Terms of Petri NetsХаритоновД. И.KharitonovD. I.

канд. техн. наук, ст. науч. сотр.

ул. Радио, д. 5, г. Владивосток, Россия, 690041

 PhD, senior researcher

5 Radio str., Vladivostok, Russia, 690041

demiurg@dvo.ruГоленковЕ. А.GolenkovE. A.

канд. физ.-мат. наук, ст. науч. сотр

ул. Радио, д. 5, г. Владивосток, Россия, 690041

 PhD, senior researcher

5 Radio str., Vladivostok, Russia, 690041

golenkov@dvo.ruТарасовГ. В.TarasovG. V.

 науч. сотр. ул. Радио, д. 5, г. Владивосток, Россия, 690041

 науч. сотр. ул. Суханова, д. 8, г. Владивосток, Россия, 690950

 

research officer 5 Radio str., Vladivostok, Russia, 690041

research officer 8 Suhanova st., Vladivostok, Russia

george@dvo.ruЛеонтьевД. В.LeontyevD. V.

 науч. сотр. ул. Радио, д. 5, г. Владивосток, Россия, 690041

 науч. сотр. ул. Суханова, д. 8, г. Владивосток, Россия, 690950

research officer 5 Radio str., Vladivostok, Russia, 690041

research officer 8 Suhanova st., Vladivostok, Russia

devozh@dvo.ruФедеральное государственное бюджетное учреждение науки Институт автоматики и процессов управления Дальневосточного отделения РАНРоссияInstitution of Russian Academy of Sciences Institute of Automation and Control Processes Far Eastern Branch of the RASRussian FederationФедеральное государственное бюджетное учреждение науки Институт автоматики и процессов управления Дальневосточного отделения РАН Дальневосточный Федеральный УниверситетРоссияInstitution of Russian Academy of Sciences Institute of Automation and Control Processes Far Eastern Branch of the RAS Far-Eastern Federal UniversityRussian Federation201520082015224563577Copyright © Харитонов Д.И., Голенков Е.А., Тарасов Г.В., Леонтьев Д.В., 20152015Харитонов Д.И., Голенков Е.А., Тарасов Г.В., Леонтьев Д.В.Kharitonov D.I., Golenkov E.A., Tarasov G.V., Leontyev D.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/273

В данной работе рассматривается с формальной точки зрения метод построения сетей Петри,имитирующих поведение императивных программ. Примеры сетей Петри с заданными характеристиками являются необходимыми в процессе программирования новых алгоритмов анализа моделей программ, в частности, они могут использоваться для разработки и оптимизации алгоритмов композиции и декомпозиции сетей Петри, построения дерева достижимости, проверки инвариантов и т.д. Способ построения состоит из двух стадий. На первой стадии описываются шаблонные конструкции, из которых будет состоять результирующая сеть, и параметры, с которыми будет выполняться построение. С помощью этих параметров можно регулировать конечный размер, а также абсолютное или относительное количество определённых конcтрукций в результирующей сети. На второй стадии с помощью автоматического итерационного процесса может быть сгенерирована сеть Петри любого размера, ограниченного оперативной памятью компьютера. В первом разделе статьи приводится необходимый минимум определений и вводится новый вариант операции композиции сетей Петри по местам. Свойства коммутативности и ассоциативности бинарного вида предложенной операции позволяют сливать несколько сетей Петри в произвольном порядке. Далее вводится понятие шаблонной конструкции в виде маркированной сети Петри, обладающей входным и выходным интерфейсами, а также правилами композиции шаблонных конструкций с использованием этих интерфейсов. Множество шаблонных конструкций объединяются в набор, для которого определяются правила эволюции. Свойство полноты набора гарантирует, что в результате эволюции набора будет получена сеть Петри, имитирующая поведение императивной программы. В статье приводится вариант полного набора шаблонных конструкций и пример генерации сети Петри, имитирующей последовательную императивную программу.

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.

модель программымодель потока управлениятеория сетей Петриобъект сети Петриprogram modelcontrol flow modelPetri net objectReferencesPeterson, James Lyle, Petri Net Theory and the Modeling of Systems, Prentice Hall, 1981, 290 pp.Peterson, James Lyle, Petri Net Theory and the Modeling of Systems, Prentice Hall, 1981, 290 pp.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, IEEE Press, Japan, 1995, 264–270.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, IEEE Press, Japan, 1995, 264–270.Best, Eike and Devillers, Raymond and Koutny, Maciej, Petri Net Algebra, Springer-erlag New York, Inc., USA, 2001.Best, Eike and Devillers, Raymond and Koutny, Maciej, Petri Net Algebra, Springer-erlag New York, Inc., USA, 2001.International Atomic Energy Agency, A Panel of Experts (2001), Investigation of an Accidental Exposure of Radiotherapy Patients in Panama/Report of a Team of Experts, 26 May – 1 June, 2001 (PDF), Austria: International Atomic Energy Agency, Vienna, 2001.International Atomic Energy Agency, A Panel of Experts (2001), Investigation of an Accidental Exposure of Radiotherapy Patients in Panama/Report of a Team of Experts, 26 May – 1 June, 2001 (PDF), Austria: International Atomic Energy Agency, Vienna, 2001.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, № 6, 30–43, (in Russian).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, № 6, 30–43, (in Russian).Denaro G. and M. Pezze`, “Petri nets and software engineering”, Lectures on Concurrency and Petri Nets, 3098, Springer-Verlag, 2004, 439–466.Denaro G. and M. Pezze`, “Petri nets and software engineering”, Lectures on Concurrency and Petri Nets, 3098, Springer-Verlag, 2004, 439–466.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).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).Mueller Ralph 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.Mueller Ralph 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.Desel J., “Controlling Petri Net Process Models”, Web Services and Formal Methods, 4th International Workshop, WS-FM (2007, Brisbane, Australia, September 28-29, ed. Marlon Dumas and Reiko Heckel), 2008, 17–30.Desel J., “Controlling Petri Net Process Models”, Web Services and Formal Methods, 4th International Workshop, WS-FM (2007, Brisbane, Australia, September 28-29, ed. Marlon Dumas and Reiko Heckel), 2008, 17–30.Laure Petrucci, “Aggregating views for Petri net model construction”, In Proc. workshop on Petri Nets and Distributed Systems (PNDS08, associated with Petri Nets 2008), 2008, 17–31.Laure Petrucci, “Aggregating views for Petri net model construction”, In Proc. workshop on Petri Nets and Distributed Systems (PNDS08, associated with Petri Nets 2008), 2008, 17–31.Abdelghani Ghomari, Chaabane Djeraba, “Modelling Multimedia Synchronization using a Time Petri Net Based Approach”, Advances in Petri Net: Theory and Applications, eds. Tauseef Aized, Intech, 2010, http://www.intechopen.com/books/advances-in-petri-net-theory-and-applications/modeling-multimedia-synchronization-using-a-time-petri-net-based-approach-.Abdelghani Ghomari, Chaabane Djeraba, “Modelling Multimedia Synchronization using a Time Petri Net Based Approach”, Advances in Petri Net: Theory and Applications, eds. Tauseef Aized, Intech, 2010, http://www.intechopen.com/books/advances-in-petri-net-theory-and-applications/modeling-multimedia-synchronization-using-a-time-petri-net-based-approach-.Chen Ming et al., “Petri net models for the semi-automatic construction of large scale biological networks”, Natural Computing, 10:3 (2011), 1077–1097.Chen Ming et al., “Petri net models for the semi-automatic construction of large scale biological networks”, Natural Computing, 10:3 (2011), 1077–1097.Ballarini P. et al., “Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems”, In 7th Annual IEEE Conference on Automation Science and Engineering (CASE 2011), 2011.Ballarini P. et al., “Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems”, In 7th Annual IEEE Conference on Automation Science and Engineering (CASE 2011), 2011.Alekseyev Arseniy et al., “Improved Parallel Composition of Labelled Petri Nets”, ACSD, eds. Caillaud, Benoıˆt and Carmona, Josep and Hiraishi, Kunihiko, IEEE Computer Society, 2011, 131–140.Alekseyev Arseniy et al., “Improved Parallel Composition of Labelled Petri Nets”, ACSD, eds. Caillaud, Benoıˆt and Carmona, Josep and Hiraishi, Kunihiko, IEEE Computer Society, 2011, 131–140.Ivan Petko and Stefan Hudґak, “General composition for high level Petri nets and its properties”, Central Europ. J. Computer Science, 2:3 (2012), 222–235.Ivan Petko and Stefan Hudґak, “General composition for high level Petri nets and its properties”, Central Europ. J. Computer Science, 2:3 (2012), 222–235.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.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.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).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).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 12 (November 2014), 82–91.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 12 (November 2014), 82–91.B. Esther Sunanda, P. Seetharamaiah, “Modeling of Safety-Critical Systems Using Petri Nets”, SIGSOFT Softw. Eng. Notes, 40:1 (2015), 1–7.B. Esther Sunanda, P. Seetharamaiah, “Modeling of Safety-Critical Systems Using Petri Nets”, SIGSOFT Softw. Eng. Notes, 40:1 (2015), 1–7.Kordon F. et al., “Complete Results for the 2015 Edition of the Model Checking Contest”, 2015, http://mcc.lip6.fr/2015/results.php.Kordon F. et al., “Complete Results for the 2015 Edition of the Model Checking Contest”, 2015, http://mcc.lip6.fr/2015/results.php.

The authors declare that there are no conflicts of interest present.