МОРФИЗМЫ МОДЕЛЕЙ ПОВЕДЕНИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ
Abstract
Анализируются ключевые формализмы теории распределенных систем: обобщенные автоматы, сети Петри, временная логика и язык ПРАЛУ. В результате анализа известных способов описания поведения вычислительных систем, построенных как набор взаимодействующих компонентов, показана перспективность языка ПРАЛУ в проектировании протоколов. Рассматриваются морфизмы интерпретации языков. Морфизм интерпретации часто используется, чтобы задать семантику языков описания процессов. По критерию богатства возможных интерпретаций язык ПРАЛУ можно считать более предпочтительным по сравнению с остальными.
References
1. Черемисинов Д.И. Формальные методы анализа поведения распределенных систем // Информатика. – 2004. – № 3. – С. 17–28.
2. Букур И., Деляну А. Введение в теорию категорий и функторов. – М.: Мир, 1972. – 260 с.
3. Sassone V., Nielsen M., Winskel G. A classification of models for concurrency // 4th International conference on concurrency theory. – Hildesheim, Germany, 1993. – P. 82–96.
4. 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.
5. Зандере Л.Я., Мартинсонс К.Я., Фрицнович Г.Ф. Автоматизация разработки протоколов сетей ЭВМ и их реализаций (библиография с комментариями) // Вычислительные сети: логическое проектирование протоколов. – Рига: Зинатне, 1988. – Вып. 2. – С. 200–273.
6. Котов В.Е. Сети Петри. – М.: Наука, 1984.
7. Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984.
8. Бандман О.Л. Сети Петри и корректность протоколов передачи данных // Вычислительные системы: Математическое и архитектурное обеспечение параллельных вычислений. – Новосибирск, 1985. – Вып. 109. – С. 29–51.
9. Bochman G.V. Hardware specification with temporal logic: An example // IEEE trans. on comp. – 1982. – Vol. 31. – № 73. – P. 222–231.
10. 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.
11. Закревский А.Д., Василенок В.К. Описание алгоритмов логического управления. – Мн.: Ин-т техн. кибернетики АН БССР, 1985. – 68 с.
12. 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.
13. Закревский А.Д. Параллельные алгоритмы логического управления. – Мн.: Ин-т техн. кибернетики НАН Беларуси, 1999. – 202 с.
14. 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.
15. 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.
16. Черемисинов Д.И. Визуализация поведения алгоритмов управления. – Мн., 1988. – 28 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 27).
17. Черемисинов Д.И. Кросс-транслятор ПРАЛУ для контроллеров на базе микропроцессора К580. – Мн., 1987. – 46 с. (Препринт / Ин-т техн. кибернетики АН БССР; № 13).
18. Система ЛОГИКА-М синтеза управляющих устройств в базисе ПЛМ и микропроцессоров /А.Д. Закревский, П.H. Бибило, В.К. Василенок и др. // УСиМ. – 1987. – № 3. – С. 31–35.
Review
For citations:
. Informatics. 2005;(1(5)):76-88. (In Russ.)
Views: 526
Email this article 