Estelle — метод формального описания распределённых систем, коммуникационных протоколов, основанный на расширенной конечно-автоматной модели . Разработан и стандартизован ISO (ISO/IEC 9074:1997, в настоящее время стандарт отозван) для описания протоколов модели OSI . Раздельно определяет как общую архитектуру распределённой системы , так и поведение отдельных компонентов. Использует синтаксис стандартного языка Паскаль .

Описание

Спецификация, составленная из модулей, определяет иерархическую структуру взаимодействующих недетерминированных компонентов, имеющих отношение «родитель-ребёнок» , в которой охватывающий модуль называется «родителем» для описанных в его теле модулей. Самый внешний охватывающий модуль называется спецификацией . В ходе выполнения спецификации может быть создано (изначально или динамически) несколько экземпляров модулей. С точки зрения внешних модулей, модуль является чёрным ящиком, взаимодействие с которым осуществляется через несколько точек взаимодействия и разделяемые экспортируемые переменные .

Заголовок модуля внешний коммуникационный интерфейс модуля и определяет последовательный или параллельный порядок выполнения дочерних модулей. Коммуникационный интерфейс модуля определяется точками взаимодействия (interaction points), каждая из которых является концом канала , по которому могут приниматься и передаваться сообщения. У каждой точки есть очередь ( FIFO ) для принятых сообщений (очередь может быть и общей для нескольких точек) .

Тело модуля описывает поведение компонента, используя расширенную модель конечного автомата, и рекурсивно описывает дочерние модули . К каждому переходу расширенного конечного автомата прикреплен набор условий, при выполнении которых автомат меняет состояние и (атомарно) выполняет заданные действия .

Поведение всей системы характеризуется взаимодействием экземпляров выполняемых модулей. Дочерние модули одного родителя выполняются параллельно, а выполнение экземпляров родителя имеет приоритет .

Инструменты

Готовую спецификацию можно использовать для имитационного моделирования системы, например, с помощью набора инструментов EDT, который позволяет как случайный режим имитации, так и режим, заданный пользователем. Спецификацию можно использовать без изменений как реализацию системы. К сожалению, спецификацию нельзя использовать для автоматической формальной верификации или проверки моделей , что является одним из недостатком данного подхода .

Кроме того, существует JEstelle — реализация формализма Estelle в сильно ограниченном синтаксисе Java (сместо Паскаля), что позволяет использовать инструменты Estelle для статической проверки спецификации .

Достоинства и недостатки

Хотя применение Estelle ограничено в основном описанием распределённых коммуникационных систем, можно выделить следующие интересные особенности этого подхода :

• возможность отложить принятие решений о конкретном способе реализации, проиграв несколько вариантов на одной базовой спецификации
• возможность выразить недетерминизм
• реализация распределённой системы на основе готовой спецификации

К недостаткам можно отнести :

• нет механизмов, устраняющих ошибки в пользовательских требованиях к системе, хотя спецификация и может прояснить некоторые моменты
• не предоставляет формальных методов проверки

Примечания

Литература

• Henri Habrias, Marc Frappier. Chapter 11 Estelle // . — John Wiley & Sons, 2006. — 418 p. — ISBN 978-1-905-20934-7 .
• Окунишникова Е. В. : препринт. — Новосибирск: Институт систем информатики им. А. П. Ершова СО РАН, 2000. (недоступная ссылка)
• ISO/IEC Information technology — Open Systems Interconnection — Estelle: A formal description technique based on an extended state transition model. , International Organization for Standardisation, Geneva, Switzerland, 1997
• Budkowski, S. and Cavalli, A. and Najm, E. A Graphical Representation and Prototype Editor for the Formal Description Technique Estelle // Formal Description Techniques and Protocol Specification, Testing and Verification. — Springer, 1998. — 467 p. — ISBN 9780412847608 .