Синтез моделей Петри телекоммуникационных протоколов

Abstract

Представлена методология синтеза моделей Петри телекоммуникационных протоколов. Выполнен обзор стандартов телекоммуникационных протоколов. В качестве промежуточного языка спецификаций использованы взаимодействующие последовательные процессы Хоара. Построены методы синтеза конечных автоматов по формуле последовательных процессов и синтеза помеченной сети Петри по формуле взаимодействующих последовательных процессов. Формализована задача синтеза непомеченной сети Петри заданной конечным автоматом.