Аннотация: Рассматриваются SDL-спецификации распределенных систем с динамическим порождением и удалением экземпляров процессов. Для них предложен метод трансляции в модифицированные цветные сети Петри - иерархические временные типизированные сети (ИЧТ- сети), в которых используется предложенная Мерлином концепция интервального времени. Естественный подход к верификации основан на использовании формальных моделей, таких, как конечные автоматы, сети Петри и их обобщения. При этом процесс анализа и верификации упрощается. Данная работа описывает SDL-системы с таймерами, которые позволяют адекватно представить значительный класс коммуникационных протоколов. Для них предложен метод трансляции в модифицированные цветные сети Петри - иерархические временные типизированные сети, в которых используются предложенная Мерлином концепция интервального времени. Алгоритм трансляции SDL-спецификаций в сетевые модели системы SDLE реализован методом трансляции в два этапа. Способ моделирования основывается на том, что в многоуровневом описании системы в SDL позиция каждого экземпляра процесса в общей иерархии системы остается неизменной, что позволяет описание системы транслировать в структуру сети, а экземпляры процесса моделировать с помощью фишек. В результате работы алгоритма создается такая сетевая модель, в которой в каждом месте будет содержать не более одной фишки, моделирующей некоторый экземпляр процесса. Таким образом, если во время функционирования системы может существовать n разных экземпляров любого процесса, то в каждом месте моделирующей его сети может содержаться не более n фишек, причем каждая фишка будет соответствовать своему экземпляру процесса. Это факт позволяет существенно повысить эффективность моделирования, так как существенно уменьшает перебор вариантов связывания переменных.

Ключевые слова: сети Петри, SDL, сетевая модель, коммуникационный протокол, экземпляр процесса.

Link:

МЕТОД ТРАНСЛЯЦИИ SDL-СПЕЦИФИКАЦИЙ С ПОМОЩЬЮ МОДИФИЦИРОВАННЫХ СЕТЕЙ ПЕТРИ ВЫСОКОГО УРОВНЯ

Анастасия Заболотная

http://www.foibg.com/ijima/vol01/ijima01-4-p09.pdf