Русская Википедия:Estelle (язык спецификаций)
Estelle — метод формального описания распределённых систем, коммуникационных протоколов, основанный на расширенной конечно-автоматной моделиШаблон:Sfn. Разработан и стандартизован ISO (ISO/IEC 9074:1997, в настоящее время стандарт отозван) для описания протоколов модели OSIШаблон:Sfn. Раздельно определяет как общую архитектуру распределённой системы, так и поведение отдельных компонентов. Использует синтаксис стандартного языка ПаскальШаблон:Sfn.
Описание
Спецификация, составленная из модулей, определяет иерархическую структуру взаимодействующих недетерминированных компонентов, имеющих отношение «родитель-ребёнок»Шаблон:Sfn, в которой охватывающий модуль называется «родителем» для описанных в его теле модулей. Самый внешний охватывающий модуль называется спецификацией. В ходе выполнения спецификации может быть создано (изначально или динамически) несколько экземпляров модулей. С точки зрения внешних модулей, модуль является чёрным ящиком, взаимодействие с которым осуществляется через несколько точек взаимодействия и разделяемые экспортируемые переменныеШаблон:Sfn.
Заголовок модуля внешний коммуникационный интерфейс модуля и определяет последовательный или параллельный порядок выполнения дочерних модулей. Коммуникационный интерфейс модуля определяется точками взаимодействия (interaction points), каждая из которых является концом канала, по которому могут приниматься и передаваться сообщения. У каждой точки есть очередь (FIFO) для принятых сообщений (очередь может быть и общей для нескольких точек)Шаблон:SfnШаблон:Sfn.
Тело модуля описывает поведение компонента, используя расширенную модель конечного автомата, и рекурсивно описывает дочерние модулиШаблон:SfnШаблон:Sfn. К каждому переходу расширенного конечного автомата прикреплен набор условий, при выполнении которых автомат меняет состояние и (атомарно) выполняет заданные действияШаблон:Sfn.
Поведение всей системы характеризуется взаимодействием экземпляров выполняемых модулей. Дочерние модули одного родителя выполняются параллельно, а выполнение экземпляров родителя имеет приоритетШаблон:Sfn.
Инструменты
Готовую спецификацию можно использовать для имитационного моделирования системы, например, с помощью набора инструментов EDT, который позволяет как случайный режим имитации, так и режим, заданный пользователем. Спецификацию можно использовать без изменений как реализацию системы. К сожалению, спецификацию нельзя использовать для автоматической формальной верификации или проверки моделей, что является одним из недостатком данного подходаШаблон:Sfn[1].
Кроме того, существует JEstelle — реализация формализма Estelle в сильно ограниченном синтаксисе Java (сместо Паскаля), что позволяет использовать инструменты Estelle для статической проверки спецификацииШаблон:Sfn.
Достоинства и недостатки
Хотя применение Estelle ограничено в основном описанием распределённых коммуникационных систем, можно выделить следующие интересные особенности этого подходаШаблон:Sfn:
- возможность отложить принятие решений о конкретном способе реализации, проиграв несколько вариантов на одной базовой спецификации
- возможность выразить недетерминизм
- реализация распределённой системы на основе готовой спецификации
К недостаткам можно отнестиШаблон:Sfn:
- нет механизмов, устраняющих ошибки в пользовательских требованиях к системе, хотя спецификация и может прояснить некоторые моменты
- не предоставляет формальных методов проверки
Примечания
Литература
- Шаблон:Книга
- Шаблон:СтатьяШаблон:Недоступная ссылка
- ISO/IEC Information technology — Open Systems Interconnection — Estelle: A formal description technique based on an extended state transition model. ISO/IEC 9074:1997, International Organization for Standardisation, Geneva, Switzerland, 1997
- Шаблон:Книга
- ↑ Budkowski S. «Estelle Development Toolset». Computer Networks and ISDN Systems 25:63-82, 1992
