abstract: Целью работы является создание методики формального описания алгоритма управления взаимодействующими параллельными процессами при обмене сообщениями между ними, выполняющимися с использованием механизма монитора, кольцевого буфера и типовой задачи «производители-потребители». В основу работы положен метод событийных недетерминированных автоматов (СНДА), позволяющий представить алгоритм управления в простой и компактной форме в виде системы рекуррентных канонических бескванторных уравнений, описывающих все реализуемые в системе управления частные события. Отличительная особенность метода СНДА заключается в том, что система уравнений, представляющая функции переходов в управляющем алгоритме, описывается не в терминах состояний детерминированных автоматов (ДА), а в терминах частных событий недетерминированных автоматов, одновременное существование которых и определяет состояние эквивалентного ему ДА. Так как число частных событий недетерминированных автоматов значительно меньше числа состояний эквивалентных ему ДА, то описание управляющего алгоритма на языке СНДА будет отличаться значительной простотой. Представленная методика формального описания частных событий алгоритма управления передачей сообщений в распределенных и многопроцессорных системах на языке СНДА обеспечивает реализацию основных свойств, которыми должны обладать системы управления: отсутствие тупиковых ситуаций (бесконфликтность) и справедливость (отсутствие бесконечного ожидания и нахождения в мониторе процессов, обращающих к общему ресурсу). Аналитическое представление алгоритма управления взаимодействующими параллельными процессами в виде системы рекуррентных канонических бескванторных уравнений позволяет выполнить простую трансформацию описания алгоритма управления на языки описания аппаратуры (например, VНDL) для верификации алгоритма и его аппаратной реализации.
keywords: алгоритм управления, взаимодействующие параллельные процессы, событийные недетерминированные автоматы, механизмы монитора