автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Спецификация и тестирование компонентов с асинхронным интерфейсом

Российская Академия Наук Институт Системного Программирования

Хорошилов Алексей Владимирович

СПЕЦИФИКАЦИЯ И ТЕСТИРОВАНИЕ КОМПОНЕНТОВ С АСИНХРОННЫМ ИНТЕРФЕЙСОМ

Специальность 05.13.11 -математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Москва 2006

Работа выполнена в Институте Системного Программирования Российской Академии Наук.

Научный руководитель:

доктор физико-математических наук, Петренко Александр Константинович

Официальные оппоненты:

доктор технических наук, профессор, заслуженный деятель науки и техники РФ Липаев Владимир Васильевич;

кандидат физико-математических наук, Веселое Николай Александрович.

Ведущая организация:

Научно-исследовательский институт системных исследований Российской Академии Наук

Защита диссертации состоится «_» _ 2006 г. в _ часов на

заседании диссертационного совета Д.002.087.01 при Институте Системного Программирования РАН по адресу:

109004, Москва, Б. Коммунистическая, 25, Институт Системного Программирования РАН, конференц-зал.

С диссертацией можно ознакомиться в библиотеке Института Системного Программирования РАН.

Автореферат разослан «_»_2006 г.

Ученый секретарь диссертационного совета кандидат физ.-мат. наук

/Прохоров С.П./

хооед

•^>305"

Общая характеристика работы Актуальность работы

Задача повышения надежности программного обеспечения уже долгое время

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

В результате, одним из основных средств обеспечения качества программных систем было и остается тестирование - при разработке программ с повышенными требованиями к надежности доля затрат на тестирование в бюджете проекта может достигать 80%. Многочисленные исследования в области формальных методов нашли свое отражение и в развитии новых технологий тестирования. Одно из наиболее активно развивающихся направлений - тестирование на основе моделей, уже успело показать свои преимущества в целом ряде крупных индустриальных проектов.

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

Комплексный подход, позволяющий автоматизировать целый спектр задач тестирования на основе математических моделей, представляет собой технология тестирования ишТевК, разработанная в ИСП РАН. Данная технология использует широко известный подход программных контрактов для формального описания требований к программному обеспечению и уникальные методы генерации сложных последовательностей тестовых воздействий на основе неявного описания конечного

автомата. Эффективность этого подхода была подтверждена в многочисленных проектах по тестированию различных программных систем.

Опыт этих проектов показал, что технология итТевК предоставляет широкие возможности по сокращению затрат на разработку и поддержку высококачественных тестовых наборов и улучшению процесса разработки программного обеспечения в целом. В то же время, проявился и ряд ограничений технологии, связанных с ограниченной областью применимости подхода классических программных контрактов.

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

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

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

Основные цели работы

Основными целями представленной диссертационной работы являлись

• разработка и исследование метода тестирования систем с асинхронным интерфейсом на основе моделей;

• реализация инструментальной поддержки процесса разработки тестов на основе предложенного подхода;

• проведение апробации метода и поддерживающих его инструментов.

Научная новизна

В диссертации разработан новый метод тестирования программных систем с

асинхронным интерфейсом на основе моделей. В ней формализованы основные задачи тестирования применительно к асинхронным системам, а именно:

• задача оценки корректности поведения тестируемой системы;

• задача генерации последовательности тестовых воздействий;

• задача оценки качества тестирования.

и предложены алгоритмы решения поставленных задач.

Практическая значимость работы

Практическая значимость работы подтверждается результатами применения

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

• тестирования реализации протокола IPv6 от Microsoft Research (MSR IPv6), проведенное в рамках совместного проекта ИСП РАН и Microsoft Research, Cambridge (MRL Contract No 2000-35);

• тестирования функций Mobile IPv6 на примере реализации Microsoft MIPv6 для Windows СЕ 4.1 и Windows ХР (MSRC Contract No 2002-84);

• тестирования отдельных компонентов TinyOS - распределенной операционной системы для сенсорных сетей, проведенной ИСП РАН совместно с российской компанией Luxoft;

• тестирования реализации протокола MPEG-2 IPMP, выполненное ИСП РАН совместно с Morphibius Technology Inc., Канада;

• тестирования ключевых функций операционной системы реального времени ОС2000 (НИИСИ РАН);

• формализации требований стандарта Linux Standard Base Core 3.1 к прикладному бинарному интерфейсу ОС Linux и разработки систематизированного тестового набора для проверки конформности этому стандарту.

Результаты работы могут быть использованы в исследованиях, которые ведутся в МГУ, ВЦ РАН, ИПМ РАН, НИИСИ РАН, ВНИИСИ РАН, НИЦЭВТ, ГосНИИАС и других научных и промышленных организациях страны.

Апробация

Результаты данной работы были доложены:

• на Международная конференция «Интернет нового поколения», проходившей в Ярославле 21-22 мая 2002 года;

• на конференции студентов, аспирантов и молодых ученых "Технологии Microsoft в теории и практике программирования", проходившей в Москве 4-5 марта 2004 года.

Публикации

Результаты автора по теме диссертации опубликованы в 5 работах, список которых приведен в конце автореферата.

Благодарности

Настоящая работа является составной частью исследований в рамках развития технологии тестирования UniTesK, проводимой в группе RedVerst Института Сисгемного Программирования РАН. Исследование методов спецификации и тестирования систем с асинхронным интерфейсом проводилось совместно с И.Б. Бурдоновым, A.C. Косачевым и В.В. Куляминым. Также автор выражает свою признательность коллегам из группы RedVerst, участвовавшим в реализации системы тестирования CTesK и апробации результатов работы: В. Омельченко, А. Коптелову, Е. Рогову, Н. Пакулину и Г. Ключникову.

Структура и объем работы

Диссертация состоит из введения, четырех глав, заключения, списка

литературы, включающего 36 названий, и двух приложений. Основной текст (без приложений) занимает 109 машинописных страниц.

Содержание работы

1. Введение

В первой главе представлено введение, в котором приводится общая характеристика темы работы, обосновывается ее актуальность и формулируются цели исследования.

2. Архитектура ипПезК для систем с синхронным интерфейсом

Во второй главе описываются математические модели, лежащие в основе

технологии тестирования ишТевК для систем с синхронными интерфейсами, и рассматривается архитектура тестовой системы, построенной по технологии ишТевК.

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

• оценки корректности поведения тестируемой системы;

• генерации тестовых данных;

• оценки качества тестирования.

Формализуется задача оценки корректности поведения тестируемой системы (рисунок 1), при этом определяются:

• модель поведения тестируемой системы,

Рисунок 1. Формализация оценки корректности поведения

• модель требований к функциональности тестируемой системы,

• отношение «удовлетворяет» между этими моделями.

После того как введены необходимые понятия и даны соответствующие определения, описывается архитектура тестовой системы ишТевК при тестировании систем с синхронным интерфейсом. Схема работы такой тестовой системы представлена на рисунке 2. Тестовая система содержит четыре компонента.

Тестовый сценарий управляет всем процессом тестирования. Он интерактивно, в ходе взаимодействия с целевой системой, генерирует последовательность воздействий на целевую систему. Для этого автоматный механизм осуществляет обход графа, заданного неявным образом в описании тестового сценария. Прохождение по дуге этого графа сопровождается выполнением сценарного воздействия, приписанного данной дуге. Сценарное воздействие, которое является «компактным» тестовым сценарием, управляет последовательностью взаимодействий с целевой системой. По завершению работы сценарного воздействия автоматный механизм либо принимает решение о завершении тестирования, либо выбирает следующую дугу и инициирует следующее сценарное воздействие.

Рисунок 2. Процесс работы тестовой системы в целом

Все воздействия на целевую систему генерируемые тестовым сценарием осуществляются через оракул. Оракул

• проверяет допустимость воздействия в текущем модельном состоянии;

• выполняет это воздействие посредством обращения к медиатору;

• проверяет корректность поведения целевой системы в процессе данного воздействия;

• вычисляет покрытые элементы для всех заданных метрик покрытия и помещает эту информацию в трассу теста.

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

• преобразует вызов модельной функции в соответствующий вызов функции целевой системы;

• получает значения выходных параметров вызванной функции;

• преобразует их в модельное представление - значения выходных параметров модельной функции;

• синхронизирует модельное состояние с внутренним состоянием тестируемой системы после оказания тестового воздействия;

• возвращает оракулу значения выходных параметров модельной функции.

Единственный пассивный компонент тестовой системы - это модельное состояние. Задача модельного состояния заключается в хранении текущих значений переменных состояния, определяющих модельное представление внутреннего состояния целевой системы. Только медиатор, который непосредственно работает с целевой системой, может изменять модельное состояние. Все остальные компоненты могут только читать его.

Медиатор синхронизирует модельное состояние с внутренним состоянием целевой системы одним из двух возможных способов. Если медиатор обладает достоверными знаниями о внутреннем состоянием целевой системы, то он вычисляет модельное состояние на основе этих знаний. В противном случае модельное состояние вычисляется, исходя из предположения о корректном

поведении целевой системы. При работе медиатора первым способом тестирование называется тестированием с открытым состоянием, при работе вторым способом - тестированием со скрытым состоянием.

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

Во-первых, предполагается, что все взаимодействия между целевой системой и ее окружением могут инициироваться только окружением. Во-вторых, предполагается, что все взаимодействия происходят строго последовательно, то есть следующее взаимодействие начинается только после завершения предыдущего. Программные системы, которые самостоятельно инициируют взаимодействия с окружением или могут одновременно участвовать в нескольких взаимодействиях с окружением, названы системами с асинхронным интерфейсом.

3. Тестирование систем с асинхронным интерфейсом

Третья глава содержит описание разработанного метода тестирования систем

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

Первый раздел посвящен проблеме оценки корректности поведения целевой системы. Общая схема решения данной проблемы совпадает со схемой использовавшейся для систем с синхронным интерфейсом (рисунок 1). Требования, предъявляемые к функциональности целевой системы, формализуются при помощи модели требований, а поведение целевой системы, зафиксированное по результатам наблюдения за ней в процессе тестирования, формализуется в модели поведения. Между моделью поведения и моделью требований определяется отношение «удовлетворяет», которое позволяет оценить корректность поведения целевой системы в процессе тестирования относительно предъявляемых к нему требований.

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

Модель поведения асинхронных систем содержит все асинхронные взаимодействия, которые были зафиксированы в ходе наблюдений за поведением целевой системы в процессе тестирования. Частичный порядок, заданный на этих взаимодействиях, описывает имеющуюся информацию о взаимном порядке выполнения этих взаимодействий во времени. Принадлежность пары взаимодействий частичному порядку (р[ -< р2) означает, что взаимодействие р! произошло раньше, чем взаимодействие р2. Если взаимодействия несравнимы, то это означает, что их взаимный порядок достоверно неизвестен.

В качестве модели требований к поведению асинхронных систем используется понятие автоматов с отложенными реакциями. Данные автоматы состоят из четырех множеств (множеств состояний, стимулов, непосредственных и отложенных реакций) и переходов, раскрашенных либо парой стимул-непосредственная реакция, либо отложенной реакцией.

Отношение «удовлетворяет» в асинхронном случае определяется следующим образом. Модель поведения (Р, -<) удовлетворяет модели требований А с данным начальным состоянием у0, тогда и только тогда, когда существует такое упорядочивание взаимодействий из мультимножества Р, согласованное с частичным порядком -<, что в автомате с отложенными реакциями А найдется путь, начинающийся в состоянии у0 и помеченный данными взаимодействиями в данном порядке.

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

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

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

асинхронная модель требований получается из нее посредством преобразования, определенного в разделе «Описание асинхронной модели требований».

Модель поведения строится по результатам наблюдения за поведением целевой системы в процессе тестирования. В ходе такого наблюдения, все взаимодействия целевой системы с окружением фиксируются в специальном компоненте тестовой системы -регистраторе взаимодействий. Частичный порядок между этими взаимодействиями задается посредством комбинации двух атрибутов, указываемых при регистрации каждого взаимодействия: идентификатора канала и временной метки.

Проверка корректности полученной асинхронной модели поведения относительно заданной асинхронной модели требований значительно осложняется тем, что модель поведения не содержит полной информации о порядке наблюдавшихся взаимодействий. Вследствие этого требуется рассмотреть все возможные линеаризации частичного порядка и для каждой из них проверить существование соответствующего пути в автомате с отложенными реакциями. Перебор линеаризаций должен не только обеспечивать наименьшую вычислительную сложность, но и избегать перебора к! заведомо неподходящих перестановок, в тех случаях, когда известно, что (п-к)-ый элемент в какой-то перестановке нарушает условия линеаризации. Алгоритм перебора линеаризаций, удовлетворяющий данным требованиям, был построен на основе алгоритма генерации всех перестановок за минимальное число транспозиций. Доказательство правильности алгоритма проверки корректности поведения целевой системы, основанного на этом алгоритме перебора перестановок, представлено в приложении А.

Второй раздел третьей главы посвящен проблеме генерации тестовых данных для асинхронных систем. Решение этой проблемы сильно осложняется большой вычислительной сложностью алгоритмов оценки корректности поведения асинхронных систем. Область применимости этих алгоритмов ограничена асинхронными моделями поведения, состоящими из нескольких десятков взаимодействий.

Одного теста такого размера явно не достаточно для достижения приемлемого качества тестирования. Построение наборов независимых тестов небольшого

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

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

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

*

пассивных введением дополнительного псевдостимула, как это показано в разделе «Стационарное тестирование асинхронных систем».

В следующем разделе рассматривается алгоритм обхода недетерминированных конечных графов, получивший название ndfsm. Основная идея этого алгоритма заключается в следующем. Если в недетерминированном графе существует детерминированный сильносвязный полный остовый подграф, то алгоритм движения может использовать этот подграф для построения обхода, не сталкиваясь непосредственно с проблемами недетерминизма.

При работе с недетерминированными графами алгоритм движения не может гарантировать обход всех дуг графа, так как алгоритм не может выбрать конкретную дугу среди набора дуг, начинающихся в одной вершине и помеченных одним стимулом. Этот выбор происходит недетерминированно и независимо от работы алгоритма движения. Поэтому для недетерминированных графов вводится понятие обхода по стимулам, которое требует прохождение по каждой паре «вершина графа — стимул» вместо прохождения по всем дугам графа. Обход по стимулам совпадает с понятием обхода на классе детерминированных графов и является более слабым на классе недетерминированных графов.

Для алгоритма движения пс^т доказывается, что он является неизбыточным алгоритмом обхода по стимулам на классе конечных графов, обладающих детерминированным силыюсвязным полным остовным подграфом.

Также в данной главе рассматриваются вопросы осуществления параллельных тестовых воздействий, использования доступной части внутреннего состояния целевой системы и метрик качества тестирования асинхронных систем.

В заключении третьей главы дается описание унифицированной архитектуры асинхронного теста, определяющей архитектуру всех тестовых систем, построенных в соответствии с предложенным методом. Основные компоненты асинхропной тестовой системы и схема взаимодействия между ними представлены на рисунке 3.

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

Рисунок 3. Унифицированная архитектура асинхронного теста

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

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

Основными результатами третьей главы являются:

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

■ разработка алгоритмов, решающих основные задачи, и в частности:

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

о разработка неизбыточного алгоритма обхода недетерминированных графов, обладающих детерминированным сильносвязным полным остовным подграфом;

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

4. Программная реализация средств тестирования систем с асинхронными интерфейсами

Четвертая глава содержит описание реализации инструментальной

поддержки предложенного подхода по тестированию систем с асинхронным

интерфейсом. Данная реализация выполнена в виде расширения набора

инструментов CTesK, поддерживающего процесс тестирования по технологии

UniTesK на платформе языка С. Эти расширения включали в себя:

■ введение дополнительных синтаксических конструкций в спецификационное расширение языка С (SEC), используемого для более компактного описания компонентов тестовой системы;

■ расширение транслятора из спецификационного расширения языка С в код на языке С;

■ разработку дополнительных библиотечных компонентов, реализующих

о алгоритм проверки корректности поведения целевой системы, о механизм построения стационарных автоматных тестовых

сценариев ndfsm, о сборку и регистрацию отложенных реакций;

■ расширение формата трассы и функциональности генераторов отчетов; * доработку документации и учебных материалов.

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

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

5. Апробация метода и инструментов

В пятой главе рассматривается опыт применения метода тестирования

асинхронных систем и его реализации в наборе инструментов CTesK, полученный в ходе шести проектов по тестированию различного программного обеспечения. Впервые предложенный подход использовался для тестирования реализации протокола IPv6 от Microsoft Research и функций протокола Mobile IPv6 на примере реализации Microsoft MIPv6 для Windows СЕ 4.1 и Windows ХР, которые проводились в рамках совместных проектов ИСП РАН и Microsoft Research, Cambridge [4]. Асинхронность взаимодействий реализации IPv6 с нижележащими и вышележащими уровнями стека протоколов играло ключевую роль в функциональности системы. Поэтому тестирование асинхронных аспектов поведения являлось важной составляющей этих проектов.

Еще одним примером применения предложенного метода для тестирования телекоммуникационных протоколов было тестирование реализации MPEG-2 IPMP, выполненное ИСП РАН совместно с Morphibius Technology Inc., Канада.

В дополнение к опыту тестирования телекоммуникационных систем предложенный подход применялся для тестирования асинхронных аспектов поведения многопроцессных и многопотоковых систем. Первым таким опытом был пилотный проект по тестированию отдельных компонентов TinyOS -распределенной операционной системы для сенсорных сетей.

Второй работой в этом направлении является проект по тестированию ядра POSIX-совместимой операционной системы реального времени ОС2000. В этом проекте асинхронные аспекты поведения играют существенную роль и включают в себя такие ключевые сервисы операционной системы как управление потоками и процессами, средства межпотокового и межпроцессного взаимодействия, асинхронный ввод-вывод, а также управление сигналами и таймерами.

Еще одним проектом, в рамках которого метод спецификации и тестирования асинхронных систем играет существенную роль, является проект по формализации

требований стандартов и разработке тестового набора для бинарных интерфейсов ОС Linux. Анализ требований к 1532 функциям интерфейса показал, что для 63% групп функций выявлена потребность в использовании метода тестирования систем с асинхронным интерфейсом, а 23% групп функций нуждаются в использовании асинхронных реакций для полного описания требований к целевой системе.

В завершении главы делаются выводы относительно опыта применения предложенного метода. Первый вывод состоит в том, что имеющийся опыт демонстрирует востребованность методов тестирования асинхронных систем, так как во многих проектах асинхронные аспекты играют существенную роль в тестируемой функциональности. Второй вывод заключается в том, что предложенные решения и их реализация в наборе инструментов CTesK позволяют успешно проводить систематизированное тестирование самых сложных асинхронных систем, таких как операционные системы и телекоммуникационные протоколы. 6. Заключение

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

За основу предложенного метода была взята технология тестирования UniTesK для систем с синхронным интерфейсом. В результате исследования технологии были выявлены основные проблемы, препятствующие ее применению для тестирования систем с асинхронным интерфейсом. Эти проблемы заключаются в том, что базовые предположения относительно поведения тестируемой системы, лежащие в основе технологии, оказываются неприменимыми к системам с асинхронным интерфейсом.

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

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

Реализация инструментов, поддерживающих представленный метод, была выполнена в виде расширения набора инструментов CTesK, предназначенных для поддержки технологии UniTesK на платформе языка С. Разработанный набор инструментов сохранил поддержку исходного метода тестирования синхронных систем, и в то же время получил дополнительные возможности по тестированию систем с асинхронным интерфейсом на основе разработанного метода. Данный метод и его инструментальная поддержка были апробированы в шести проектах по тестированию различного программного обеспечения.

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

■ Разработан и исследован метод тестирования систем с асинхронным интерфейсом, заключающийся в разработке автоматизированного тестового набора на основе формального описания требований к тестируемой системе.

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

■ Реализован набор инструментов для поддержки предложенного метода в виде расширения набора инструментов CTesK.

■ Выполнена апробация предложенного подхода в шести проектах по тестированию различных классов систем с асинхронным интерфейсом.

\

7. Приложения

В приложении А приведено доказательство правильности алгоритма проверки корректности поведения целевой системы с асинхронным интерфейсом, а в приложении Б содержится таблица, представляющая результаты анализа бинарного интерфейса ОС Linux относительно доли асинхронных функций в современных операционных системах.

Работы автора по теме диссертации

1. Хорошилов A.B. Спецификация и тестирование систем с асинхронным интерфейсом. Препринт. М: ИСП РАН, 2006.61 С.

2. Баранцев A.B., Бурдонов И.Б., ДемаковА.В., ЗеленовС.В., КосачевА.С., Кулямин В.В., Омельченко В.А., Пакулин Н.В., Петренко А.К., Хорошилов A.B. Подход UniTesK к разработке тестов: достижения и перспективы //Труды Института системного программирования №5. М.: ИСП РАН, 2004. С.121-156.

3. Сортов A.A., Хорошилов A.B. Функциональное тестирование Web-приложений на основе технологии UniTesK // Труды Института системного программирования №8. М.: ИСП РАН, 2004. С.77-97.

4. Агамирзян И.Р., Грошев С.Г., Ключников Г.Н., Косачев A.C., Омельченко В.А., Пакулин Н.В., Петренко А.К., Хорошилов A.B., Шнитман В.З. Применение формальных методов для тестирования MSR IPv6 // «Информатизация и связь». 2002. 12. №3. С. 31-33.

5. Хорошилов A.B. Неявные спецификации асинхронных систем // Тезисы конференции студентов, аспирантов и молодых ученых "Технологии Microsoft в теории и практике программирования". М.: Издательский отдел факультета ВМиК МГУ им. М.В. Ломоносова, 2004. С. 40-41.

Напечатано с готового оригинал-макета

Издательство ООО "МАКС Пресс" Лицензия ИД N00510 <тг 01.12.99 г. Подписано к печати 17.03.2006 г. Формат 60x90 1/16. Усл.печл. 1,25. Тираж 100 экз. Заказ 168. Тел. 939-3890. Тел./факс 939-3891. 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 627 к.

ZOöGü SS 05"

08

1. Введение.

Формальные методы и тестирование программного обеспечения.

Технология ипГГезК.

Системы с асинхронным интерфейсом.

Постановка задачи.

I 2. Архитектура ишТеБК. для систем с синхронным интерфейсом.

Основные понятия.

Модель требований и модель поведения.

Оценка корректности поведения целевой системы.

Формализация задачи.

I Модель поведения.

Модель требований.

Программные контракты.

Описание модели требований.

Описание модели поведения.

Моделирование требований и поведения.

Модели требований и поведения в унифицированной архитектуре теста.

Тестовые сценарии.

Генерация тестовых данных.

Управляющие автоматы.

Тестовый сценарий. ^ Автоматный механизм построения тестового сценария.

Сценарные функции.

Граф автоматного тестового сценария.

Механизм построения тестового сценария с^т.

Тестовый сценарий в унифицированной архитектуре теста.

Модель оценки качества тестирования.

Качество тестирования.

Модель оценки качества тестирования.

Описание метрик покрытия.

Метрики покрытия в унифицированной архитектуре теста. р Управляемые метрики покрытия и оптимизация тестового набора.

Унифицированная архитектура теста.

Системы с асинхронным интерфейсом.

3. Тестирование систем с асинхронным интерфейсом.

Модель требований и модель поведения.

Модель поведения.

Модель требований.

Описание асинхронной модели требований.

Описание асинхронных взаимодействий в модели поведения.

Модель каналов.

Модель временных меток.

Описание асинхронной модели поведения.

Алгоритм проверки корректности поведения.

Требования к полноте набора асинхронных реакций.

Модели требований и поведения в унифицированной архитектуре асинхронного теста.

9 Асинхронные тестовые сценарии.

Генерация тестовых данных для асинхронных систем.

Взаимодействующие автоматы.

Асинхронные функции.

Асинхронные тесты.

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

Асинхронные сценарные функции.

Стационарное тестирование асинхронных систем.

Стационарный автоматный тестовый сценарий.

Асинхронный тестовый сценарий dfsm.

Алгоритм обхода ndfsm.

Параллельные воздействия на целевую систему.

Тестирование с открытым стационарным состоянием.

Нарушение предусловий асинхронных воздействий.

Тестовый сценарий в унифицированной архитектуре асинхронного теста.

Оценка качества тестирования систем с асинхронным интерфейсом.

Ь Качество тестирования систем с асинхронным интерфейсом.

Метрики покрытия асинхронной модели требований.

Описание асинхронных метрик покрытия.

Оценка качества тестирования в унифицированной архитектуре асинхронного теста

Унифицированная архитектура асинхронного теста.

Результаты главы.

4. Программная реализация средств тестирования систем с асинхронными интерфейсами.

Процесс тестирования в технологии UniTesK.

Проекция технологии UniTesK на язык программирования С. щ Тестирование систем с асинхронным интерфейсом на платформе языка С.

5. Апробация метода и инструментов.

Реализация протокола IPv6.

Функциональность протокола Mobile IPv6.

Протокол MPEG-2 IPMP.

Компоненты распределенной операционной системы для сенсорных сетей.

Ядро операционной системы реального времени.

Прикладные бинарные интерфейсы ОС Linux.

Апробация учебных материалов.

Результаты апробации.

Формальные методы и теетировшше программного обеспечения В последнее время наблюдается бурное развитие компьютерных технологий. Они проникают во все сферы деятельности человека и оказывают все большее влияние на его жизнь. Системы управления транспортом и автоматизированные линии производства, банковские платежные системы и телекоммуникационные сети, медицинские системы обеспечения жизнедеятельности и интеллектуальные дома все это является неотъемлемой частью современного мира. Однако, чем большее значение отводится компьютерным системам, тем выше становится цена их ошибок. Как показывает практика, наиболее уязвимым местом компьютерных систем с этой точки зрения является программное обеспечение. Так, ошибка в одном программном модуле многомиллионного межпланетпого корабля Mars Climate Orbiter привела к его гибели в атмосфере Марса после более чем девятимесячного полета [1,2]. Более того, некорректное поведение современных программных систем влечет не только огромные убытки, но и приводит к гибели людей. Например, ошибки в программном обеспечении медицинского оборудования Therac-25 привели к получению повышенной дозы радиации и последуюшей смерти 7 пациентов [3,4]. А арифметическая ошибка в программном обеспечении комплекса противовоздушной обороны Patriot не позволила вовремя обнаружить иракскую ракету, что привело к гибели 28 солдат во время ирако-американской войны 1991 года [5]. И это только малая часть уже имевших место прецедентов. С нарастанием сложности и важности задач, решаемых программными системами, проблема обеспечения их качества становится все острее. Много надежд на существенный прогресс в этом направлении связывается с развитием формальных методов. В широком смысле, под формальными методами понимаются любые попытки использования математических подходов к разработке программного обеспечения с целью повышения его качества[6]. Как правило, для этого используются математические модели различных сущностей, участвующих в процессе разработки. Примерами таких моделей могут служить модель исходных требований к разрабатываемой системе, модель архитектуры системы или модель реализации системы. Одним из основных нанравлений в области формальных методов являются методы доказательства корректности программ, такие как методы аналитической верификации и проверки моделей [7,8,9,10]. В этих методах доказательство корректности программ строится по следующей схеме. Для данной программной системы создаются математическая модель требований к системе и математическая модель реализации этой системы. После чего доказывается наличие отношения «удовлетворяет» между этими двумя моделями, что и рассматривается как доказательство корректности программы. Существует также целый набор вариаций подхода. Например, в качестве модели требований может выступать модель программной системы более высокого уровня абстракции, или доказательство корректности может сводиться к доказательству непротиворечивости одной из математических моделей. Однако, несмотря на больщие усилия вложенные в развитие данного направления, на настоящий момент так и не появилось методов доказательства корректности программ, которые смогли бы предоставить приемлемые решения для обеспечения качества реальных программных систем. В результате, одним из основных средств обеспечения качества программных систем было и остается тестирование: при разработке программ с повышепными требованиями к надежности доля затрат на тестирование в бюджете проекта может достигать 80%. Многочисленные исследования в области формальных методов нашли свое отражение и в развитии новых технологий тестирования. Одно из наиболее активно развивающихся направлений тестирование на основе моделей, уже успело показать свои преимущества в целом ряде крупных индустриальных проектов [11,12,13,14,15,16,17].Тестирование на основе моделей позволяет систематизировать и автоматизировать процесс разработки тестовых наборов посредством использования различного рода математических моделей. И в тех случаях, когда небольшого ручного тестирования оказывается недостаточно для обеспечения требуемого уровня качества программного обеспечения, тестирование на основе моделей позволяет добиться существенного повышения качества тестирования с затратами меньшими, чем при использовании других подходов. Технология UniTesK Комплексный подход, позволяющий автоматизировать целый спектр задач тестирования на основе математических моделей, представляет собой технология тестирования UniTesK [18,19,20], разработанная в Институте Системного Программирования РАН. Данная технология использует широко известный подход программных контрактов [21] для формального описания требований к программному обеспечению и уникальные методы генерации сложных последовательностей тестовых воздействий на основе неявного описапия конечного автомата. Эффективность такого подхода была подтверждена в мпогочислеппых проектах [22], и, в частности, при разработке тестового набора для ядра операциоппой системы канадского телекоммуникационного гиганта Nortel Networks [23]. Технология тестирования UniTesK основывается на базовых принципах формальных методов, таких как формальные спецификации требований к программной системе, и в то же время остается доступной для применения в крупных индустриальных проектах. Ключевым элементов в достижении этого является переход от доказательства корректности программной системы к проверке корректности реального поведения системы на тестовых данных. Для этого вместо построения модели реализации программной системы и доказательства ее корректности относительно модели требований на всех возможных входных данных используется наблюдение за реальным поведепием программной системы на конкретных тестовых данных, построение по результатам наблюдения модели поведения системы и доказательство корректности этой модели относительно модели требований. Такое решение обладает двумя существенными достоинствами, которые обусловлены тем, что модель поведения программной системы на конкретных данных значительно проще, чем модель реализации этой системы, отражающая поведение программной системы па всех возможных входных данных. Первое достоинство решения, предлагаемого технологией UniTesK, заключается в значительном сглаживании нерехода между областью неформальных объектов и областью их математических моделей. Этот переход является одним из наиболее критикуемых мест формальных методов [24]. Применительно к методам доказательства корректности программ проблема данного перехода заключается в том, что доказательство корректности математической модели реализации программпой системы не гарантирует корректность самой реализации. И единственным средством для проверки соответствия между реализацией системы и ее моделью является их сопоставление, выполняемое человеком. Для реальных программных систем такое сопоставление является большой проблемой в виду размеров модели и сложности связей между ее составляющими. Модель поведения системы на конкретных данных, используемая в техпологии UniTesK, является значительно более простой, чем модель реализации, а значит сопоставлепие модели поведения с реальным поведением системы является значительно более простым, чем сопоставление модели реализации с самой реализацией. Второе достоинство решения, предлагаемого технологией UniTesK, состоит в упрощении методов доказательства корректности. Доказать, что поведение программной системы па конкретных тестовых данных является корректным, значительно проще, чем доказать то же самое для всех возможных входных данных. Наиболее важным нрактическим результатом данного факта является то, что область применимости методов доказательства корректности модели поведения программной системы на конкретных данных значительно превосходит область применимости методов доказательства корректности моделей реализации программных систем в целом. Поэтому во многих случаях, когда размеры программных систем не позволяют использовать методы доказательства корректности программ, тестирование на основе моделей по технологии UniTesK успешно применяется и доказывает свои преимущества. Расплатой за эти преимущества является неполнота тестирования по сравнению с доказательством корректности программ. Если в результате доказательства корректности модели реализации, при допущении корректности соответствия между реализацией и ее моделью, следует корректность реализации на всех входных данных, то в результате доказательства корректности модели поведения программной системы на конкретных тестовых данных, при допущении корректности соответствия между реальным поведением и построенной моделью, следует корректность реализации только на тех тестовых данных, которые использовались в процессе тестирования. С другой стороны, если сравнивать технологию UniTesK с обычными методами разработки тестов, то наличие формальных спецификаций требований и методов их автоматической проверки, позволяет значительно упростить процесс разработки высококачественных тестовых паборов. Это достигается за счет того, что добавление новых тестовых данных не требует решения задачи оценки корректности поведения тестируемой системы, так как эта оценка выполняется автоматически на основе формальной снецификации требований. Более того, задача генерации тестовых данных также может быть в значительной степени автоматизирована на основе использования формальных спецификаций. И эта возможность также реализована в технологии UniTesK в виде уникальных методов генерации последовательностей тестовых воздействий на основе неявного описания конечного автомата. Таким образом, технология UniTesK не предоставляет замену методам доказательства корректности программ, по позволяет воспользоваться формальным математическим базисом для разработки качественных тестов с меньшим уровнем затрат по сравнению с обычными методами разработки тестов. Системы с асинхронным интерфейсом Эффективность технологии UniTesK подтверждена многочисленными проектами [22,23], которые показали, что технология предоставляет широкие возможности по сокращению затрат на разработку и поддержку высококачественных тестовых наборов и улучшению нроцесса разработки программного обеспечения в целом. В то же время, проявился и ряд ограничений технологии, связанных с ограниченной областью применимости подхода классических программных контрактов. Подход программных контрактов, основанный на описании инвариантов данных, а также предусловий и постусловий интерфейсных операций, предполагает синхронность всех взаимодействий с программной системой. То есть, работа программной системы рассматривается как последовательность вызовов интерфейсных операций, осуществляемых последовательно: следующий вызов происходит только после завершения предыдущей вызванной операции. Кроме того, классические программные контракты основываются на предположении, что все взаимодействия с программной системой инициируются окружением этой системы, а сама система не может инициировать никаких взаимодействий. С другой стороны, эти предположения не выполняются для широкого класса программных систем, для которых возможность одновременного участия в нескольких взаимодействиях или инициации взаимодействий с окружением является существенной составляющей функциональности. Такие системы далее мы будем называть системами с асинхронным интерфейсом. Например, телекоммуникационные протоколы и драйверы устройств могут участвовать одновременно в нескольких взаимодействиях со своим окружением, и, кроме того, они могут инициировать эти взаимодействия самостоятельно. Другим примером систем с асинхронным интерфейсом, являются компоненты, использующие межпроцессное и межпотоковое взаимодействие, компоненты, создающие и удаляющие процессы или потоки управления, а

Заключение

В рамках настоящей диссертационной работы разработан новый метод тестирования систем с асинхронным интерфейсом на основе моделей. Данный метод расширяет область применимости существующих комплексных подходов к тестированию на основе моделей на новый широкий класс систем - систем с асинхронным интерфейсом.

За основу предложенного метода была взята технология тестирования ЦшТезК для систем с синхронным интерфейсом. В результате исследования технологии были выявлены основные проблемы, препятствующие ее применению для тестирования систем с асинхронным интерфейсом. Эти проблемы заключаются в том, что базовые предположения относительно поведения тестируемой системы, лежащие в основе технологии, оказываются неприменимыми к системам с асинхронным интерфейсом.

Для систем с асинхронным интерфейсом оказывается не верно, что:

• любое взаимодействие между тестируемой системой и ее окружением может инициироваться только окружением;

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

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

Задача оценки корректности поведения целевой системы решается следующим образом:

• требования к функциональности тестируемой системы описываются в виде формальных спецификаций, которые неявным образом задают автомат с отложенными реакциями;

• поведение целевой системы, наблюдаемое в процессе тестирования, представляется в виде частично-упорядоченного множества взаимодействий между целевой системой и ее окружением;

• зафиксированное множество взаимодействий проверяется на соответствие автомату с отложенными реакциями, заданному формальными спецификациями требований.

Если множество соответствует автомату, то считается, что поведение целевой системы в процессе тестирования удовлетворяло предъявляемым к нему требованиям. В противном случае считается, что тестирование обнаружило несоответствие между поведением целевой системы и формальными спецификациями требований.

Проверка соответствия множества взаимодействий автомату с отложенными реакциями осуществляется при помощи специально разработанного алгоритма, корректность которого доказана в приложении А.

Задача генерации тестовых данных для систем с асинхронным интерфейсом существенно осложняется большой вычислительной сложностью алгоритма оценки корректности поведения. Чтобы решить эту проблему и сохранить при этом одно из основных достоинств технологии итТеэК для синхронных систем - автоматическое построение сложных последовательностей тестовых воздействий, использован подход так называемого стационарного тестирования. Идея этого подхода заключается в том, что алгоритм оценки корректности применяется не один раз в конце теста, а постоянно в процессе тестирования, по завершению некоторого шага теста.

Кроме того, для ускорения процесса выполнения тестов и облегчения процесса их разработки разработан новый алгоритм обхода графов пс^т, который особенно актуален для тестирования систем с асинхронным интерфейсом. По сравнению с базовым алгоритмом технологии итТеэК для синхронных систем сШт, этот алгоритм позволяет:

• осуществлять обход не только детерминированных графов, но и определенного класса недетерминированных графов;

• оптимизировать обход графа по количеству выполняемых переходов по дугам.

Задача оценки качества тестирования для систем с асинхронным интерфейсом решается также как и в синхронном случае: на основе разбиения множества всех возможных взаимо-I действий на конечное число классов эквивалентности. Однако, понятие покрытия класса эквивалентности существенно отличается в связи с многочисленностью корректных путей в автомате с отложенными реакциями. Поэтому потребовалось разработать новый алгоритм подсчета покрытия классов эквивалентности по результатам работы асинхронного теста.

На основе рассмотренных математических моделей и алгоритмов была разработана унифицированная архитектура асинхронной тестовой системы, определяющая архитектуру всех * тестовых систем, построенных в соответствии с предложенным методом. В этой архитектуре были выделены основные компоненты тестовой системы, проведено разграничение ответственностей между компонентами и определены правила взаимодействия между ними.

Реализация инструментов, поддерживающих представленный метод, была выполнена в виде расширения набора инструментов CTesK, предназначенных для поддержки технологии 9 UniTesK на платформе языка С. Данные расширения включали в себя:

• введение дополнительных синтаксический конструкций в спецификационное расширение языка С (SEC);

• расширение транслятора из спецификационного расширения языка С в С (SEC2C);

• разработку дополнительных библиотечных компонентов асинхронной тестовой 9 системы;

• расширение формата трассы и функциональности генераторов отчетов;

• доработку документации и учебных материалов.

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

Следует отметить, что большинство работ по программной реализации средств тестирования систем с асинхронными интерфейсами были выполнены автором лично, за исключением работ по расширению формата трассы и функциональности генератора отчетов, в которых oit участвовал в качестве проектировщика и разработчика технического задания, ft Предложенный метод и его инструментальная поддержка были апробированы в шести проектах по тестированию различного программного обеспечения. В качестве тестируемых систем выступали реализации протоколов IPv6, Mobile IPv6, MPEG-2 IPMP, отдельные компоненты распределенной операционной системы для сенсорных сетей TinyOS, ядро операционной системы реального времени OC2ÛOO и функции стандартного бинарного ^ интерфейса операционной системы Linux. Вышеозначенные проекты показали востребованность методов тестирования систем с асинхронным интерфейсом, а также работоспособность предложенных решений и их программной реализации, обеспечивших проведение систематизированного тестирования таких сложных асинхронных систем, как операционные системы и реализации телекоммуникационных протоколов.

Подводя итог вышесказанному, выделим основные результаты, полученные в ходе ^ выполнения диссертационной работы:

• Разработан и исследован метод тестирования систем с асинхронным интерфейсом, заключающийся в разработке автоматизированного тестового набора на основе формального описания требований к тестируемой системе. о Разработаны математические модели и алгоритмы, обеспечивающие решение 9 основных задач тестирования для систем с асинхронным интерфейсом. о Разработана унифицированная архитектура автоматизированного тестового набора для систем с асинхронным интерфейсом и разработано расширение языка SEC для поддержки тестирования асинхронных систем.

• Реализован набор инструментов для поддержки предложенного метода в виде ft расширения набора инструментов CTesK.

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

1. Euler, Е.Е., Jolly, S.D., Curtis, H.H. The Failures of the Mars Climate Orbiter and Mars Polar• Lander: A Perspective from the People Involved // Proceedings of Guidance and Control 2001. American Astronautical Society, AAS 01-074,2001.

2. Report on the Loss of the Mars Climate Orbiter Mission. JPL D-18441, 1999.

3. Porrello, A.M. Death and Denial: The Failure of the Therac-25, A Medical Linear Accelerator.

4. Leveson, N.G., Clark S.T. An Investigation of the Therac-25 Accidents // Computer. July, 1993. » P.18-41.

5. Patriot missile defense: Software problems led to system failure at Dhahran, Saudi Arabia. Report GAO/IMTEC-92-26, Information Management and Technology Division, US General Accounting Office. Washington DC, Feb. 11992.

6. Berry, D. M. Formal methods: the very idea, some thoughts about why they work when they work. I // Science of Computer Programming #42(1). P. 11-27.

7. Floyd, R. W. Assigning meanings to programs // Proceedings Symp. Appl. Math., 19. in: J.T.Schwartz (ed.), Mathematical Aspects of Computer Science. P. 19-32. American Mathematical Society, Providence, R.I., 1967.

8. Francez, N. Verification of programs. Addison-Wesley Publishers Ltd., 1992.

9. Manna, Z. Mathematical theory of computation. McGraw-Hill, 1974.

10. Manna, Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.

11. Dalai, S. R., Jain, A., Karunanithi, N., Leaton, J. M., Lott, С. M., Patton, G. C., Horowitz, В. M. Model-Based Testing in Practice // Proceedings of the ICSE'99. May 1999.

12. Farchi, E., Hartman, A., Pinter, S. S. Using a Model-Based Test Generator to Test for Standard » Conformance // IBM Systems Journal, 2002. V. 41, No. 1, P. 89-110.

13. Gronau, A., Hartman, A., Kirshin, A., Nagin, K., Olvovsky, S. A Methodology and Architecture for Automated Software Testing // IBM Research Laboratory in Haifa Technical Report, 2000.

14. Offutt, A. J., Liu, S., Abdurazik, A. Generating Test Data from State-Based Specifications // Journal of Software Testing, Verification & Reliability. V. 13, No. 1, March 2003.

15. Al-Ghafees, M., Whittaker, J. A. Markov Chain-based Test Data Adequacy Criteria: a Complete

16. Family. // IS June 2002. P. 13-37.

17. Bourdonov, I., Kossatchev, A., Kuliamin, V., Petrenko, A. UniTesK Test Suite Architecture // Proceedings of FME, 2002. LNCS 2391. P. 77-88. Springer-Verlag.

18. Кулямин B.B., Петренко A.K., Косачев A.C., Бурдонов И.Б. Подход UniTesK к разработке тестов // Программирование, 29(6). 2003. С. 25-43.

19. Meyer, В. Applying 'Design by Contract* // IEEE Computer, vol. 25, October 1992. P. 40-51.

20. HTML,PDF. (http://www.unitesk.com).

21. Burdonov, I., Kossatchev, A., Petrenko, A., Cheng, S., Wong, H. Formal Specification and Verification of SOS Kernel // BNR, NORTEL Design Forum, June 1996.

22. Monin, J. F., Hinchey, M. G. Understanding Formal Methods. Springer-Verlag, 2003.

23. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Использование конечных автоматов для | тестирования программ. // Программирование, 2000, №2.

24. Бурдонов И.Б., Косачев A.C., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. //Программирование. 2003. №5.ь С. 11-30.

25. Бурдонов И.Б., Косачев A.C., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. //Программирование. 2004. №1. С. 4-24.

26. Бурдонов И.Б., Косачев A.C., Кулямин В.В. Асинхронные автоматы: классификация и тестирование. // Труды ИСП РАН. 2003. №4. С. 7-84.

27. Stanley, R. P. Enumerative combinatorics. Belmont, 1986.

28. Липский В. Комбинаторика для программистов. Москва, Мир, 1988.

29. Message Sequence Charts. ITU recommendation Z.120.

30. Agamirzian, I., Groshev, S.G., Khoroshilov, A.V., Kluchnikov, G.N., Kossatchev, A.S., Omelchenko, V.A., Pakoulin, N.V., Petrenko, A.K., Shnitman, V.Z. MSR IPv6 verification project,ft December 2001. HTML. (http://www.ispras.ru/~RedVerst).

31. Агамирзян И.Р., Грошев С.Г., Ключников Г.Н., Косачев A.C., Омельченко В.А., I Пакулин Н.В., Петренко А.К., Хорошилов A.B., Шнитман В.З. Применение формальныхметодов для тестирования MSR IPv6 // «Информатизация и связь». 2002. 12. № 3.

32. Linux Standard Base Core 3.1. ISO/IEC IS-23360. HTML. (http://refspecs.freestandards.org/lsb.shtml).

33. Francez, N. Verification of programs. Addison-Wesley, 1992.ft