Сборники трудов ИСП РАН


Финальные модели спецификации.

И. Бурдонов, А. Косачев.

Аннотация

Работа посвящена исследованию формальных методов тестирования соответствия (конформности) исследуемой системы требованиям, заданным в форме спецификации. Такое тестирование основано на семантике взаимодействия, которая определяет тестовые возможности по управлению (заданный набор тестовых воздействий) и наблюдению действий и отказов (отсутствие действий). Допускаются также ненаблюдаемые (внутренние) действия. Семантика параметризуется семействами наблюдаемых и ненаблюдаемых отказов. Вводится разрушение – запрещённое действие, которого следует избегать при взаимодействии. Определяется понятие безопасного тестирования, при котором не возникают ненаблюдаемые отказы и разрушение, и тестовые воздействия не подаются при дивергенции (бесконечной последовательности ненаблюдаемых действий). На этой основе определяются реализационная гипотеза о безопасности и безопасная конформность, а также генерация полного набора тестов по спецификации.

В работе исследуются различные модели для описания спецификационных требований. Наиболее распространенной моделью является система помеченных переходов – LTS (Labelled Transition System). В то же время для рассматриваемой семантики взаимодействия существенны только трассы (последовательности наблюдений), но не состояния LTS. Поэтому естественной оказывается трассовая модель как множество трасс LTS. Такая семантика позволяет определять только конформности типа редукции, в отличие от конформностей типа симуляций, для проверки которых требуется дополнительная тестовая возможность – опрос состояния реализации [10],[11],[12],[19],[22]. При безопасном тестировании тесты генерируются по безопасным трассам спецификации, для прохождения которых используются только безопасные тестовые воздействия.

Целью данной работы является выделение подмножества трасс спецификации, достаточного для генерации полного набора тестов. Такое подмножество мы назвали финальной трассовой моделью спецификации. С другой стороны, LTS-модель удобна тем, что является способом конечного представления регулярных множеств трасс. Для представления финальной трассовой модели в работе предлагается разновидность LTS, названная финальной RTS (Refusal Transition System). Переходы по наблюдаемым отказам задаются явно (эти отказы входят в алфавит RTS). Такая модель обладает целым рядом полезных для генерации тестов свойств: 1) она детерминирована, 2) трасса наблюдений безопасна тогда и только тогда, когда она заканчивается в нетерминальном состоянии, где нет разрушения, 3) тестовое воздействие безопасно после трассы тогда и только тогда, когда оно безопасно в конечном состоянии трассы, то есть в этом состоянии нет дивергенции, тестовое воздействие не вызывает разрушения и ненаблюдаемых отказов.

В работе предложены алгоритмы преобразования LTS-модели в финальную RTS-модель и определены достаточные условия построения конечной RTS за конечное время.

Ключевые слова

Семантика взаимодействия, отказы, разрушение, дивергенция, конформность, безопасное тестирование, трассы, LTS, генерация тестов

Издание

Труды Института системного программирования РАН, том 22, 2012, стр. 233-280.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-15

Полный текст статьи в формате pdf Вернуться к содержанию тома