Лекция: Метод верификации композиции правильных компонентов

Метод верификации композиции компонентов базируется на спецификации функций и временных (temporal) свойствах готовых проверенных компонентов (типа reuse) [6.23]. Свойства составного компонента из компонентов повторного использования — reuse проверяются с помощью абстракции и общей компонентной модели (ОКМ). Эта модель состоит из совокупности проверенных компонентов, спецификаций их временных свойств и условий функционирования, которые проверяются с помощью аппарата асинхроннойпередачи сообщений (АПС). Его основу составляет модель проверки (Model Сhecking) [6.16, 6.23] временных свойств и обнаружения ошибок взаимодействия, возникающих при композиции компонентов.

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

· спецификация компонентов задается в языке диалекта UML [6.23] и содержит описание временных свойств;

· reuse-компоненты задают функции, спецификации интерфейса и временные свойства;

· композиционный аппарат проверяет свойства составных компонентов.

Модель ОКМ — это совокупность специфицированных компонентов и их временных свойств для обеспечения верификации. Свойство компонента определяется исходя из условий среды. Когда компонент многократно используется в составе составного компонента эти свойства должны учитывать возможности среды и связей с другими компонентами композиции. ОКМ проверяется на модели вычислений АПС.

Представители ОКМ-модели могут быть примитивными и составными. Описание свойств примитивных элементов модели проверяется непосредственно с помощью модели проверки, а свойство составного компонента — на абстракции компонента, составленной из примитива и проверенных свойств в интегрированной среде.

Если абстракция слишком громоздкая для проверки, то применяется композиционный подход для проверки сгруппированных свойств компонентов и включения проверенных свойств в абстракцию.

Данный подход может использоваться в распределенных приложениях, функционирующих на платформах CORBA, DCOM и EJB.

Формально каждый компонент в ОКМ-модели задается в виде, где — исходный код компонента; — интерфейс этого компонента с другими компонентами через передачу сообщений или вызовов процедур; — множество переменных, определенных в и связанных со свойствами множества временных свойств, отражающими особенности среды компонента.

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

Композиция компонентов — это совокупность более простых компонентов:, определенных на модели компонента следующим образом. создается из множества представлений, связанных между собой интерфейсами из набора интерфейсов, операций связи для взаимодействия с другими компонентами;

— множество временных свойств, определенных на и, и проверенных на компонентах с использованием отдельных свойств ;

— подмножество где — ссылка на свойство -компонента из, заданное в .

Модель вычислений АПС — это вычислительная модель системы, заданная на конечном множестве взаимодействующих процессов представленных кортежами:

где — множество переменных с типом; — расширенная модель состояния; — очередь сообщений в порядке их поступления; — множество начальных значений для каждой переменной из, и пустое для .

При выполнении в вычислительной среде создается модель состояния в виде кортежа, где — множество состояний, каждое из которых связано с ассоциативным действием; — множество типов сообщений; — набор переходов, определенных на множествах и

Каждое из состояний переходов — кортеж, где и — состояния в и — тип сообщения во множестве сообщений .

Семантически каждое действие определяется сегментом программы, составленным из операторов: пустой оператор, присваивания, передачи сообщений, условный и составной операторы и др.

Асинхронная передача сообщений АПС вызывает чередование переходов состояний и действий процессов. Для двух процессов и передача сообщения от к включает в себя: тип сообщения из множества для и соответствующие параметры. Когда оператор действия выполняется, сообщение с параметрами ставится вочередь к процессу. Более подробные сведения о верификации компонентов приведены в [6.23].