Формальное описание моделей систем в языке Z

Приведем наиболее известные из этих моделей:

  • • обобщенная модель, компоненты которой задаются с помощью языка спецификации Z-схем;
  • • модель системы в виде ациклического графа, формально создаваемая с помощью композиционной теории;
  • • формальная модель модульной структуры, которая задается в виде графа, имеет язык его спецификации.

Обобщенная модель является формальной, создается с помощью языка спецификации Z-схем и включает в себя описание:

  • • создания узла управления моделью;
  • • назначения метки узла графа;
  • • задания внешних характеристик и параметров модулей.

Созданная модель включает в себя:

  • • совокупность Z-схем с набором деклараций и ограничений;
  • • инварианты схем для верификации модели.

На определение обобщенной модели повлияли следующие операции:

  • • выбор модуля из библиотеки шаблонов, переименование шаблонов или их конкретизация соответственно определению узла графа, где зафиксирован шаблон;
  • • связь модулей в модульную структуру системы, модули которой имеют интерфейс порта после конкретизации слота и отмечаются меткой соответствующей Z-схемы;
  • • верификация связей модулей, которая включает в себя проверку атрибутов и ТД;
  • • создание нового шаблона, инкапсуляция его интерфейса и соответствующей схемы.

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

Каждому модулю модели соответствует сервис как провайдера (provider), так и потребителя (consumer) услуг. Дуга графа от модуля М к модулю Доопределяет интерфейс, который может предоставлять модуль ДО для модуля М.

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

Базис формального метода представления модели — спецификация интерфейсов модулей для двух вышсказанных пользователей сервисов. Интерфейс удовлетворяет следующим свойствам:

  • • разделение (separable) модулей с точки зрения проектирования и спецификации, интерфейс которых не требует описания среды модуля;
  • • композиция (composition), когда модули соединяются с помощью механизмов композиционной теории в виде системы с гарантированными связями между ними.

Данная теория базируется на модели интерфейса для взаимодействия модз'лей системы между собою через сетевые протоколы (TCP, UDP и др.). Каждый протокол передает разным модулям этой модели параметры для нахождения требуемого сервиса.

Модель интерфейса задает связь модуля со средой в виде дискретного события (event), которое возникает только тогда, когда модуль и среда действуют вместе, и создают событие, рассматриваемое на стороне интерфейса.

Таким образом, интерфейс специфицирован как множество последовательностей событий для наблюдения за поведением модулей модели. Предположим, что S определяет спецификацию модуля М, которая включает в себя все возможные случаи его поведения и задает разные ситуации, которыми могут быть:

  • • событие интерфейса или состояние наблюдателя системы;
  • • анализ, который является конечным или представлен неопределенной последовательностью;
  • • формализм определения этой последовательности;
  • • условия выполнения события.

Эти предположения разрешают обеспечить разноуровневую систему взаимодействия модулей модели через механизм протоколов и систему наблюдения за событиями.

Проект модели VDM системы состоит из двух модулей: модуля управления CONT и модуля распределения памяти STOR.

Модуль CONT имеет следующую спецификацию действий:

Общее назначение этой спецификации состоит в том, что потребитель может вставлять данные в coin для отправки запроса (reguest) модулю памяти. Этот модуль дает ответ (response) на запросы и имеет следующую спецификацию:

Модель VM определяет параллельную обработку модулей CONT, STOR, а также связь со средой.

При этом спецификация УМ имеет вид

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >