maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-6-21-33mais-136Research ArticleОригинальные статьиArticlesВерификация вычислительных решеток с особыми краевыми условиями бесконечными сетями ПетриVerification of Computing Grids with Special Edge Conditions by Infinite Petri NetsЗайцевДмитрий АнатольевичZaitsevD. A.

доктор технических наук, профессор,

г. Одесса, Украина, 

сайт: http : //member.acm.org/∼daze, http : //daze.ho.ua .

Основные научные результаты: универсальная сеть Петри; анализ бесконечных сетей Петри с регулярной структурой; кланы систем линейных алгебраических уравнений (функциональные подсети); композиционный анализ сетей Петри; функциональная эквивалентность, передаточная функция и эквивалентные преобразования временных сетей Петри; временные сети Петри с многоканальными переходами, уравнение состояний, частичные инварианты; синтез функций непрерывной (нечеткой) логики, заданных таблично.

доктор технических наук, профессор

г. Одесса, Украина,

cайт: http : //member.acm.org/∼daze, http : //daze.ho.ua.

Основные научные результаты: универсальная сеть Петри; анализ бесконечных сетей Петри с регулярной структурой; кланы систем линейных алгебраических уравнений (функциональные подсети); композиционный анализ сетей Петри; функциональная эквивалентность, передаточная функция и эквивалентные преобразования временных сетей Петри; временные сети Петри с многоканальными переходами, уравнение состояний, частичные инварианты; синтез функций непрерывной (нечеткой) логики, заданных таблично.

zsoftua@yahoo.comМеждународный гуманитарный университетРоссияМеждународный гуманитарный университетRussian Federation2012120320151962133Copyright © Зайцев Д.А., 20152015Зайцев Д.А.Zaitsev D.A.Данная работа распространяется под лицензией 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/136

Представлена методика верификации вычислительных решеток с помощью нахождения инвариантов бесконечных сетей Петри. Построены модели структур квадратных решеток в форме параметрических сетей Петри для таких краевых условий, как соединение краев и усеченные устройства. По параметрическим сетям Петри построены бесконечные системы линейных алгебраических уравнений для вычисления p-инвариантов и получены их параметрические ре- шения. P-инвариантные сети Петри являются структурно консервативными и ограниченными, что, вместе с живостью, является свойствами моделей идеальных систем. Исследование живости модели на основе анализа сифонов и ловушек может быть выполнено с помощью p-инвариантов модифицированных сетей.

A technique of the computing grid verification using invariants of infinite Petri nets was presented. Models of square grid structures in the form of parametric Petri nets for such edge conditions as connection of edges and truncated devices were constructed. Infinite systems of linear algebraic equations were composed on parametric Petri nets for calculating p-invariants; their parametric solutions were obtained. P-invariant Petri nets are structuraly conservative and bounded that together with liveness are the properties of ideal systems. Liveness investigation based on siphons and traps can be implemented by using p-invariants of modified nets.

вычислительная решеткабесконечная сеть Петриинвариантограниченностьконсервативностьживостьcomputing gridinfinite Petri netinvariantboundednesssafenesslivenessReferencesGrid Computing: Towards a Global Interconnected Infrastructure / Ed. Preve N.P. Springer, 2011. 312 p.Grid Computing: Towards a Global Interconnected Infrastructure / Ed. Preve N.P. Springer, 2011. 312 p.Murata T. Petri Nets: Properties, Analysis and Applications // Proc. of the IEEE. 1989. Vol. 77, no. 4. P. 541–580.Murata T. Petri Nets: Properties, Analysis and Applications // Proc. of the IEEE. 1989. Vol. 77, no. 4. P. 541–580.Silva M., Colom J. M. On the Computation of Structural Synchronic Invariants in P/T Nets // Springer. LNCS. 1988. Vol. 340. P.387–417.Silva M., Colom J. M. On the Computation of Structural Synchronic Invariants in P/T Nets // Springer. LNCS. 1988. Vol. 340. P.387–417.Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. М.: Наука, 1990. 253 с.Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. М.: Наука, 1990. 253 с.Berthelot G., Terrat R. Petri Nets Theory for the Correctness of Protocols // IEEE Trans. on Communications. 1982. Vol. 30, № 12. P. 2497–2505.Berthelot G., Terrat R. Petri Nets Theory for the Correctness of Protocols // IEEE Trans. on Communications. 1982. Vol. 30, № 12. P. 2497–2505.Diaz M. Modelling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Model // Computer Networks. 1982, №6. P. 419–441.Diaz M. Modelling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Model // Computer Networks. 1982, №6. P. 419–441.Z. W. Li, M. C. Zhou Deadlock Resolution in Automated Manufacturing Systems. Springer, 2010. 234 p.Z. W. Li, M. C. Zhou Deadlock Resolution in Automated Manufacturing Systems. Springer, 2010. 234 p.Zaitsev D.A., Zaitsev I.D. Verification of Ethernet protocols via parametric composition of Petri net // INCOM’2006: 12th IFAC/IFIP/IFORS/IEEE/IMS Symposium Information Control Problems in Manufacturing, May 17–19 2006, SaintEtienne, France. P. 261–267.Zaitsev D.A., Zaitsev I.D. Verification of Ethernet protocols via parametric composition of Petri net // INCOM’2006: 12th IFAC/IFIP/IFORS/IEEE/IMS Symposium Information Control Problems in Manufacturing, May 17–19 2006, SaintEtienne, France. P. 261–267.Шмелева Т.Р. Верификация протоколов коммутируемой Ethernet бесконечными сетями Петри // Труды ДУIКТ: Особливий випуск. Київ, 2007. С. 96–102.Шмелева Т.Р. Верификация протоколов коммутируемой Ethernet бесконечными сетями Петри // Труды ДУIКТ: Особливий випуск. Київ, 2007. С. 96–102.Shmeleva T.R., Zaitsev D.A., Zaitsev I.D. Analysis of Square Communication Grids via Infinite Petri Nets // Збiрник Наукових праць ОНАЗ iм. О.С. Попова. 2009, № 1. С. 27–35.Shmeleva T.R., Zaitsev D.A., Zaitsev I.D. Analysis of Square Communication Grids via Infinite Petri Nets // Збiрник Наукових праць ОНАЗ iм. О.С. Попова. 2009, № 1. С. 27–35.Зайцев Д.А., Шмелева Т.Р. Верификация коммуникационных структур гиперкуба параметрическими сетями Петри // Кибернетика и системный анализ. 2010. №1. С. 119–128.Зайцев Д.А., Шмелева Т.Р. Верификация коммуникационных структур гиперкуба параметрическими сетями Петри // Кибернетика и системный анализ. 2010. №1. С. 119–128.Shmeleva T.R. Proving Consistency of Petri Net Grid Models // Book of Abstracts of the International Scientific Conference on Computer Algebra and Information Technology, August 20-26, 2012. Odessa, Ukraine, 2012. P. 83–86.Shmeleva T.R. Proving Consistency of Petri Net Grid Models // Book of Abstracts of the International Scientific Conference on Computer Algebra and Information Technology, August 20-26, 2012. Odessa, Ukraine, 2012. P. 83–86.Зайцев Д.А., Лi Ж.В., Лiтвiн Д.О., Хоу I.Ф. Обчислення сифонiв сiтей Петрi через композицiю кланiв // Науковий вiсник Мiжнародного гуманiтарного унiверситету: серiя IТтаУП. 2012. Вип. 4. С. 32–44.Зайцев Д.А., Лi Ж.В., Лiтвiн Д.О., Хоу I.Ф. Обчислення сифонiв сiтей Петрi через композицiю кланiв // Науковий вiсник Мiжнародного гуманiтарного унiверситету: серiя IТтаУП. 2012. Вип. 4. С. 32–44.Berthomieu B., Ribet O.-P., Vernadat F. The tool TINA - construction of abstract state space for Petri nets and Time Petri nets // International Journal of Production Research. 2004. Vol. 42, №14. P. 2741–2756 (http://www.laas.fr/tina).Berthomieu B., Ribet O.-P., Vernadat F. The tool TINA - construction of abstract state space for Petri nets and Time Petri nets // International Journal of Production Research. 2004. Vol. 42, №14. P. 2741–2756 (http://www.laas.fr/tina).

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