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