Формальные методы - часть 2
Интерфейс удовлетворяет следующим свойствам:
– разделенность (separable) модулей с точки зрения проектирования и спецификации, интерфейс которых не требует описания среды модуля;
– композиционность (сомроsіtіоn), когда модули соединяются через композиционную теорию в систему с гарантированными связями между ними.
Данная теория базируется на модели интерфейса для взаимодействия модулей системы между собою через сетевые протоколы (TCP, UDP и др.). Каждый протокол передает разным модулям этой модели параметры для нахождения нужного сервиса.
Модель интерфейса задает связь модуля со средой в виде дискретного события (event), которое возникает только тогда, когда модуль и среда действуют вместе, и создают событие, рассматриваемое со стороны интерфейса. Иными словами, интерфейс специфицируется в виде множества последовательностей событий для наблюдения за поведением модулей модели.
Предположим, что S определяет спецификацию модуля M, которая включает в себя все возможные случаи его поведения и задает разные ситуации, которыми могут быть:
– событие интерфейса или состояние наблюдателя системы;
– анализ является конечным или представлен неопределенной последовательностью;
– формализм определения этой последовательности;
– условия выполнения события.
Эти предположения разрешают обеспечить разноуровневую систему взаимодействия модулей модели через механизм протоколов и систему наблюдения за событиями.
Формальный метод и спецификация RAISE. RAISE– метод и RSL–спецификация (RAISE Spesification Language) [45, 46] были разработаны в 1985–1998гг. как результат предварительного исследования формальных методов. Метод содержит нотации, техники и инструменты для использования формальных методов при конструировании ПС и доказательстве их правильности. Метод имеет программную поддержку в виде набора инструментов и методик, которые постоянно развиваются и используются для конструирования и доказательства правильности программ.