Метод верификации композиции компонентов базируется на спецификации
функций и временных (temporal) свойствах готовых проверенных
компонентов (типа reuse) [6.23]. Свойства составного компонента из
компонентов повторного использования - reuse проверяются с помощью
абстракции и общей компонентной модели (ОКМ). Эта модель состоит из
совокупности проверенных компонентов, спецификаций их временных
свойств и условий функционирования, которые проверяются с помощью
аппарата асинхроннойпередачи сообщений (АПС). Его основу составляет
модель проверки (Model Сhecking) [6.16, 6.23] временных свойств и
обнаружения ошибок взаимодействия, возникающих при композиции
компонентов.
Модель проверки включает в себя идентификацию правильных
компонентов; композицию повторных компонентов по их спецификациям;
формирование общей спецификации компонентной системы, составленной
из правильных компонентов и др. При этом выполняются следующие
условия:
· спецификация компонентов задается в языке диалекта UML [6.23] и
содержит описание временных свойств;
· reuse-компоненты задают функции, спецификации интерфейса и
временные свойства;
· композиционный аппарат проверяет свойства составных
компонентов.
Модель ОКМ - это совокупность специфицированных компонентов и их
временных свойств для обеспечения верификации. Свойство компонента
определяется исходя из условий среды. Когда компонент многократно
используется в составе составного компонента эти свойства должны
учитывать возможности среды и связей с другими компонентами
композиции. ОКМ проверяется на модели вычислений АПС.
Представители ОКМ-модели могут быть примитивными и составными.
Описание свойств примитивных элементов модели проверяется
непосредственно с помощью модели проверки, а свойство составного
компонента - на абстракции компонента, составленной из примитива и
проверенных свойств в интегрированной среде.
Если абстракция слишком громоздкая для проверки, то применяется
композиционный подход для проверки сгруппированных свойств
компонентов и включения проверенных свойств в абстракцию.
Данный подход может использоваться в распределенных приложениях,
функционирующих на платформах CORBA, DCOM и EJB.
Формально каждый компонент в ОКМ-модели задается в виде , где -
исходный код компонента; - интерфейс этого компонента с другими
компонентами через передачу сообщений или вызовов процедур; -
множество переменных, определенных в и связанных со свойствами
множества временных свойств , отражающими особенности среды
компонента.
Каждое свойство - это пара , проверяемая на множестве , где -
свойство компонента в , - множество временных формул из свойств,
определенных на множествах и . Свойства компонента включается в
абстракцию только тогда, когда оно проверено в среде этого
компонента.
Композиция компонентов - это совокупность более простых
компонентов: , определенных на модели компонента следующим образом.
создается из множества представлений , связанных между собой
интерфейсами из набора интерфейсов , операций связи для
взаимодействия с другими компонентами;
- множество временных свойств, определенных на и , и проверенных на
компонентах с использованием отдельных свойств ;
- подмножество где - ссылка на свойство -компонента из , заданное в
.
Модель вычислений АПС - это вычислительная модель системы, заданная
на конечном множестве взаимодействующих процессов представленных
кортежами:
где - множество переменных с типом; - расширенная модель состояния;
- очередь сообщений в порядке их поступления; - множество начальных
значений для каждой переменной из , и пустое для .
При выполнении в вычислительной среде создается модель состояния в
виде кортежа , где - множество состояний, каждое из которых связано
с ассоциативным действием; - множество типов сообщений; - набор
переходов, определенных на множествах и
Каждое из состояний переходов - кортеж , где и - состояния в и -
тип сообщения во множестве сообщений .
Семантически каждое действие определяется сегментом программы,
составленным из операторов: пустой оператор, присваивания, передачи
сообщений, условный и составной операторы и др.
Асинхронная передача сообщений АПС вызывает чередование переходов
состояний и действий процессов. Для двух процессов и передача
сообщения от к включает в себя: тип сообщения из множества для и
соответствующие параметры. Когда оператор действия выполняется,
сообщение с параметрами ставится вочередь к процессу . Более
подробные сведения о верификации компонентов приведены в [6.23].