Всю информацию, необходимую для выполнения

Всю информацию, необходимую для выполнения перебора различных порядков, алгоритм поиска получает через интерфейс управляющего (Controller). Архитектура, реализующая методы этого интерфейса, показана на . Основные поставщики информации - это EJBServerInterceptor и JVMHook. EJBServerInterceptor работает на сервере приложений и перехватывает удаленные вызовы методов компонентов. Встраивание данного класса происходит с помощью механизма перехватчиков (interceptor) , определенных в EJB 3.0 []. До выполнения метода компонента выполняются перехватчики, определенные для данного типа компонентов. Механизм перехватчиков используется для реализации таких служб, как управление транзакциями и безопасностью. Нам же от этого механизма требуется только блокировка удаленного вызова метода. EJBServerInterceptor через удаленный интерфейс InfoCollector сообщает информацию о вызываемом методе, создавая по описанию метода переход Transition (processTransition) . Вызов при этом блокируется. JVMHook работает на той же JVM, на которой выполняется тест. Этот класс передает информацию о порождаемых в тесте потоках incActiveThreadCount и decActiveThreadCount, а также информацию о завершении теста notifyEndState. Информация о количестве порождаемых потоков необходима для обнаружения начального глобального состояния. Компоненты, разработанные по технологии EJB, обладают рядом важных свойств:

В компонентах не создаются новые потоки. Если с системой работает N клиентов, то для блокировки всех взаимодействий в системе достаточно заблокировать N вызовов методов.
В каждый момент для экземпляра компонента может выполняться лишь один метод. В зависимости от настроек сервера приложений другие вызовы либо помещаются в очередь, либо завершаются с исключением. Это гарантирует, что данные экземпляра могут одновременно изменяться лишь одним потоком. Кроме того, мы будем требовать выполнения двух дополнительных ограничений, которые не являются обязательными по спецификации EJB, однако выполняются для большинства систем:
Обращения к EntityManager происходят внутри транзакций.
Этим обеспечивается атомарность обновления данных в базе данных.
Все обращения к разделяемой памяти сосредоточены в EntityManger, т.е. других обращений нет.

Последние два ограничения, по сути, требуют, чтобы все обращения к разделяемой памяти были атомарными и контролировались (перехватывались) управляющим. Для систем, удовлетворяющих этим ограничениям, верно, что для любого конкретного состояния системы и воздействий на систему:

Существует единственное дерево перебора;
Пути дерева перебора описывают все возможные результаты выполнения.

Таким образом, гарантируется, что если для воздействий, осуществляемых в переходе автомата, система может работать некорректно (несоответствует спецификации), то соответствующий некорректный результат будет обнаружен. Корректность для всей системы в целом зависит от выбранного разработчиком тестов обобщенного состояния и тестовых воздействий, осуществляемых в сценарных методах. При выполнении ряда гипотез [] можно гарантировать, что вся система корректна. В гипотезах требуется, чтобы система в обобщенных состояниях вела себя "похоже". Важным результатом данной работы является возможность утверждать корректность не только для последовательных, но и распределенных программ.

Содержание раздела