informИнформатикаInformatics1816-03012617-6963UIIP NASBinform-740Research ArticleЛОГИЧЕСКОЕ ПРОЕКТИРОВАНИЕLOGICAL DESIGNМОРФИЗМЫ МОДЕЛЕЙ ПОВЕДЕНИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМЧеремисиновД. И.Объединенный институт проблем информатики НАН БеларусиBelarus20051001201901(5)7688Copyright © Черемисинов Д.И., 20192019Черемисинов Д.И.Черемисинов Д.И.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://inf.grid.by/jour/article/view/740

Анализируются ключевые формализмы теории распределенных систем: обобщенные автоматы, сети Петри, временная логика и язык ПРАЛУ. В результате анализа известных способов описания поведения вычислительных систем, построенных как набор взаимодействующих компонентов, показана перспективность языка ПРАЛУ в проектировании протоколов. Рассматриваются морфизмы интерпретации языков. Морфизм интерпретации часто используется, чтобы задать семантику языков описания процессов. По критерию богатства возможных интерпретаций язык ПРАЛУ можно считать более предпочтительным по сравнению с остальными.

ReferencesЧеремисинов Д.И. Формальные методы анализа поведения распределенных систем // Информатика. – 2004. – № 3. – С. 17–28.Черемисинов Д.И. Формальные методы анализа поведения распределенных систем // Информатика. – 2004. – № 3. – С. 17–28.Букур И., Деляну А. Введение в теорию категорий и функторов. – М.: Мир, 1972. – 260 с.Букур И., Деляну А. Введение в теорию категорий и функторов. – М.: Мир, 1972. – 260 с.Sassone V., Nielsen M., Winskel G. A classification of models for concurrency // 4th International conference on concurrency theory. – Hildesheim, Germany, 1993. – P. 82–96.Sassone V., Nielsen M., Winskel G. A classification of models for concurrency // 4th International conference on concurrency theory. – Hildesheim, Germany, 1993. – P. 82–96.Börger E. High level system design and analysis using abstract state machines // Current trends in applied formal methods (FM–Trends 98). Lecture notes in computer science. – Vol. 1641. – Springer Verlag, 1999. – P. 1–43.Börger E. High level system design and analysis using abstract state machines // Current trends in applied formal methods (FM–Trends 98). Lecture notes in computer science. – Vol. 1641. – Springer Verlag, 1999. – P. 1–43.Зандере Л.Я., Мартинсонс К.Я., Фрицнович Г.Ф. Автоматизация разработки протоколов сетей ЭВМ и их реализаций (библиография с комментариями) // Вычислительные сети: логическое проектирование протоколов. – Рига: Зинатне, 1988. – Вып. 2. – С. 200–273.Зандере Л.Я., Мартинсонс К.Я., Фрицнович Г.Ф. Автоматизация разработки протоколов сетей ЭВМ и их реализаций (библиография с комментариями) // Вычислительные сети: логическое проектирование протоколов. – Рига: Зинатне, 1988. – Вып. 2. – С. 200–273.Котов В.Е. Сети Петри. – М.: Наука, 1984.Котов В.Е. Сети Петри. – М.: Наука, 1984.Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984.Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984.Бандман О.Л. Сети Петри и корректность протоколов передачи данных // Вычислительные системы: Математическое и архитектурное обеспечение параллельных вычислений. – Новосибирск, 1985. – Вып. 109. – С. 29–51.Бандман О.Л. Сети Петри и корректность протоколов передачи данных // Вычислительные системы: Математическое и архитектурное обеспечение параллельных вычислений. – Новосибирск, 1985. – Вып. 109. – С. 29–51.Bochman G.V. Hardware specification with temporal logic: An example // IEEE trans. on comp. – 1982. – Vol. 31. – № 73. – P. 222–231.Bochman G.V. Hardware specification with temporal logic: An example // IEEE trans. on comp. – 1982. – Vol. 31. – № 73. – P. 222–231.Emerson E.A., Halpern J.Y. «Sometimes» and «Not never» revisited: On branching versus linear temporal logic // JACM. – 1986. – Vol. 33. – № 1. – P. 151–178.Emerson E.A., Halpern J.Y. «Sometimes» and «Not never» revisited: On branching versus linear temporal logic // JACM. – 1986. – Vol. 33. – № 1. – P. 151–178.Закревский А.Д., Василенок В.К. Описание алгоритмов логического управления. – Мн.: Ин-т техн. кибернетики АН БССР, 1985. – 68 с.Закревский А.Д., Василенок В.К. Описание алгоритмов логического управления. – Мн.: Ин-т техн. кибернетики АН БССР, 1985. – 68 с.Clarke E.M., Emerson E.A., Systla A.P. Automatic verification of finite-state concurrent systems using temporal-logic specifications // ACM Transactions on Programming Languages and Systems. – 1986. – Vol. 8. – № 2. – P. 244–263.Clarke E.M., Emerson E.A., Systla A.P. Automatic verification of finite-state concurrent systems using temporal-logic specifications // ACM Transactions on Programming Languages and Systems. – 1986. – Vol. 8. – № 2. – P. 244–263.Закревский А.Д. Параллельные алгоритмы логического управления. – Мн.: Ин-т техн. кибернетики НАН Беларуси, 1999. – 202 с.Закревский А.Д. Параллельные алгоритмы логического управления. – Мн.: Ин-т техн. кибернетики НАН Беларуси, 1999. – 202 с.Menasche M., Berthomieu B. Time Petri nets for analyzing and verifying time dependent communication protocols // Protocol specification, testing, and verification. Vol. 3. – North-Holland: Elsevier Science, 1983. – P. 161–172.Menasche M., Berthomieu B. Time Petri nets for analyzing and verifying time dependent communication protocols // Protocol specification, testing, and verification. Vol. 3. – North-Holland: Elsevier Science, 1983. – P. 161–172.Zakrevskii A.D. The analysis of concurrent logic control algorithms // Lecture Notes in Computer Science, Fundamentals in Computation Theory. – Springer Verlag. – Vol. 278. – 1987. – P. 497–500.Zakrevskii A.D. The analysis of concurrent logic control algorithms // Lecture Notes in Computer Science, Fundamentals in Computation Theory. – Springer Verlag. – Vol. 278. – 1987. – P. 497–500.Черемисинов Д.И. Визуализация поведения алгоритмов управления. – Мн., 1988. – 28 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 27).Черемисинов Д.И. Визуализация поведения алгоритмов управления. – Мн., 1988. – 28 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 27).Черемисинов Д.И. Кросс-транслятор ПРАЛУ для контроллеров на базе микропроцессора К580. – Мн., 1987. – 46 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 13).Черемисинов Д.И. Кросс-транслятор ПРАЛУ для контроллеров на базе микропроцессора К580. – Мн., 1987. – 46 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 13).Система ЛОГИКА-М синтеза управляющих устройств в базисе ПЛМ и микропроцессоров /А.Д. Закревский, П.H. Бибило, В.К. Василенок и др. // УСиМ. – 1987. – № 3. – С. 31–35.Система ЛОГИКА-М синтеза управляющих устройств в базисе ПЛМ и микропроцессоров /А.Д. Закревский, П.H. Бибило, В.К. Василенок и др. // УСиМ. – 1987. – № 3. – С. 31–35.

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