Application of Petri component nets in the checking task of parallel distributed systems

E.A. Lukyanova

Abstract


The paper discusses the Kripke structures of two mathematical models of parallel distributed systems that are presented by Petri detailed net and its component net. Bisimularity of these Kripke structures is displayed. The possibility for checking the validity of the logical formula of temporal logic is established, which gives the desired property of investigated parallel distributed system, using reduced Kripke structure of component Petri net.

 Prombles in programming 2014; 2-3: 93-98

References


Карп P.M., Миллер Р.Е. Параллельные схемы программ // Кибернетический сборник. – М.: Мир, 1976. – Т. 13. – С. 5–61.

Котов В.Е. Сети Петри. – М.: Наука, 1984. – 157 с.

Котов В.Е., Нариньяни А.С. Асинхронные вычислительные процессы над памятью // Кибернетика. – 1966. – № 3. – С. 64–71.

Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // Lect. Notes Comput Sci. – 1981. – Vol. 131. – P. 52–71.

Jaffe J. The use of queues in parallel dataflow evaluation of 'if-then-while' programs // MIT, Laboratory for Computer Science. Tech. Rep. TM104, May 1978.

Roux J.-L., Berthomieu B. Verification of local area network protocol with Tine, a software package for time Petri nets // Proc. 7th Europ.

Workshop on Application and Theory of Petri Nets. – 1986. – P. 183–205.

Zuberek W.M. Timed Petri nets and preliminary performance evaluation // Proc. 7th Annual Symp. on Сотр. Archit. – 1980. – P. 88–96.

Davis A.L. A data flow evaluation system based on the concept of recursive locality // Proc. Nat. Comput. Conf., New York, June 4-7, 1979. Arlington: AFIPS Press. – 1979. – Vol. 48. – P. 1079–1086.

Лук’янова О.О. Про компонентне моделювання систем з паралелізмом // Наукові записки НаУКМА. Комп’ютерні науки. – 2012. – Т. 138. – C. 47–52.

Лукьянова Е.А. О компонентном анализе параллельных распределенных систем // ТВИМ. – 2011. – № 2. – С. 71–81.

Лук’янова О.О. Пробісимуляційну еквівалентність детальної моделі Петрі та її CN-моделі досліджуваної паралельної розподіленої

системи // Вісник КНУ імені Тараса Шевченка. Серія: фізико-математичні науки. – 2013.– Спецвипуск.

Лукьянова Е.А. О гомоморфизме компонентной сети Петри // Кибернетика и системный анализ. – 2014. – № 1.

Лук’янова О.О. Про зв’язок мови CN-моделі з компонентами-переходам і мови детальної моделі Петрі паралельної розподіленої

системи // Вісник КНУ імені Тараса Шевченка. Серія: фізико-математичні науки. – 2012. – № 4. – С. 145–150.

Lukyanova E. Component modeling: on connections of detailed Petri model and component model of parallel distributed system // ITHEA. –

– Vol. 2, № 1. – P. 15–22.

Лукьянова Е.А. О языке компонентной сети Петри с компонентами-местами и компонентами-переходами // ТВИМ. – 2011. – № 2. – С. 71–81.

Clarke E.M., Grumberg O., Peled D. Model Checking // The MIT Press, 1999. – 314 p.

Kenneth L. McMillan Symbolic Model Checking. – CMU-CS-92-131. – 1992.

Лукьянова Е.А., Дереза А.В. Исследование однотипних структурних элементов CN-сети в процессе компонентного моделирования и анализа сложной системы с параллелизмом // Кибернетика и системный анализ. – 2012. – № 6. – С. 20–29.

Лукьянова Е.А. Метод верификации свойств реактивной системы на модели // ТВИМ. – 2006. – № 2. – C. 60–68.


Refbacks

  • There are currently no refbacks.