Системы с асинхронным интерфейсом
Изначально технология UniTesK использовала для формального описания требований к программному обеспечению подход классических программных контрактов []. Этот подход показал себя с лучшей стороны при разработке тестового набора для ядра операционной системы канадского телекоммуникационного гиганта Nortel Networks []. В то же время, проявился и ряд ограничений, связанных с ограниченной областью применимости классических программных контрактов.
Подход классических программных контрактов, основанный на описании инвариантов данных, а также предусловий и постусловий интерфейсных операций, предполагает синхронность всех взаимодействий с программной системой. То есть, работа программной системы рассматривается как последовательность вызовов интерфейсных операций, осуществляемых последовательно: следующий вызов происходит только после завершения предыдущей вызванной операции. Кроме того, классические программные контракты основываются на предположении, что все взаимодействия с программной системой инициируются окружением этой системы, а сама система не может инициировать никаких взаимодействий.
С другой стороны, эти предположения не выполняются для широкого класса программных систем, для которых возможность одновременного участия в нескольких взаимодействиях или инициации взаимодействий с окружением является существенной составляющей функциональности. Такие системы далее мы будем называть системами с асинхронным интерфейсом.
Например, телекоммуникационные протоколы и драйверы устройств могут участвовать одновременно в нескольких взаимодействиях со своим окружением, и, кроме того, они могут инициировать эти взаимодействия самостоятельно. Другим примером систем с асинхронным интерфейсом, являются компоненты, использующие межпроцессное и межпотоковое взаимодействие, компоненты, создающие и удаляющие процессы или потоки управления, а также компоненты, содержащие интерфейсные функции, которые блокируются до наступления некоторых событий.
Формальные спецификации требований к системам с асинхронным интерфейсом на основе классических программных контрактов не могут полностью описать все существенные особенности их функционирования.
Основополагающим камнем в математических моделях технологии UniTesK являются понятия взаимодействия и модели поведения целевой системы. Именно в этих терминах описывается процесс тестирования и на их основе строятся все остальные модели.
Однако, у данных моделей есть несколько ограничений. Во-первых, в них предполагается, что любое взаимодействие между целевой системой и ее окружением может инициироваться только окружением. Во-вторых, предполагается, что все взаимодействия происходят строго последовательно, то есть следующее взаимодействие начинается только после завершения предыдущего.
Примером целевой системы, для которой эти предположения нарушаются, является подсистема, реализующая стек протоколов. Она получает пакеты от вышестоящего уровня, формирует из них пакеты нижележащего уровня и посылает по сети. С другой стороны, эта подсистема получает пакеты из сети, преобразует их и передает вышестоящему приложению.
Передача пакетов в сеть и приложению являются примерами взаимодействий, которые инициируются не окружением, а самой целевой системой. Конечно, эти взаимодействия можно моделировать как часть взаимодействий, инициированных окружением. То есть можно рассматривать пакет, отправленный в сеть, как часть реакции на просьбу послать сообщение от приложения или как часть реакции на пришедший пакет из сети.
Рисунок 10. Стек протоколов
Но в этом случае особенно критичными становится второе ограничение. Рассмотрим взаимодействие, которое инициируется приложением вышестоящего уровня. Приложение просит стек протоколов послать сообщение. Завершением этого взаимодействия будем считать передачу в сеть всех пакетов, необходимых для посылки данного сообщения. Предположение о последовательности взаимодействий не позволяет тестовой системе инициировать следующее взаимодействие до завершения предыдущего. Таким образом, рассмотренная выше архитектура будет ограничена тестированием только тех ситуаций, в которых стек протоколов в каждый момент времени обрабатывает только один запрос о посылке сообщения.
