научная статья по теме ОТ РЕДАКТОРОВ СПЕЦИАЛЬНОГО ВЫПУСКА Математика

Текст научной статьи на тему «ОТ РЕДАКТОРОВ СПЕЦИАЛЬНОГО ВЫПУСКА»

ПРОГРАММИРОВАНИЕ, 2008, № 6, с. 3-4

УДК 681.32

ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ

ОТ РЕДАКТОРОВ СПЕЦИАЛЬНОГО ВЫПУСКА

© 2008 г. В. А. Непомнящий1, А. К. Петренко2

1 Институт систем информатики им. А.П. Ершова СО РАН 630090 Новосибирск, проспект Академика Лаврентьева, 6 2Институт системного программирования РАН 109004 Москва, ул. Б. Коммунистическая, 25 E-mail: vnep@iis.nsk.su, petrenko@ispras.ru Поступила в редакцию 14.07.2008 г.

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

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

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

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

4

НЕПОМНЯЩИЙ, ПЕТРЕНКО

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

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

В статье Н.В. Шилова, И.С. Ануреева, Е.В. Бодина "О генерации условий корректности для императивных программ" предлагается развитие метода верификации программ Флойда-Хоара на случай неструктурированных и недетерминированных программ.

M.JI. Громов, Н.В. Евтушенко, A.B. Коломе-ец - авторы статьи "К синтезу условных тестов для недерминированных автоматов" рассматривают практически важную задачу построения

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

В.А. Непомнящий и его коллеги-соавторы статьи "Моделирование и верификация коммуникационных протоколов, представленных на языке SDE, с помощью сетей Петри высокого уровня" предлагают Иерархические Временные Типизированные сети Петри (ИВТ-сети) и метод трансляции SDE в ИВТ-сети. Этот подход позволяет получать компактное и естественное представление моделей протоколов и применять к ним различные техники верификации. В заключении статьи описываются эксперименты по применению предложенной техники.

A.B. Демаков, C.B. Зеленов, С.А. Зеленова, авторы статьи "Использование абстрактных моделей для генерации тестовых данных сложной структуры" обобщают опыт, полученный при тестировании разнообразных программ, которые можно назвать текстовыми процессорами (например, компиляторы, парсеры заголовков протокольных сообщений, анализаторы и конверторы ХМГ-файлов и проч.). В подходе используются формальные описания моделей и отображений из абстрактных в конкретные модели.

Последняя статья выпуска "Автоматизация массового создания тестов работоспособности" написана группой авторов ИСП РАН - P.C. Зы-биным, В.В. Куляминым, A.B. Пономаренко, В.В. Рубановым, Е.С. Черновым. Она описывает новую технику автоматизированной генерации тестов для проверки работоспособности программных интерфейсов в случае, когда число интерфейсов достигает десятков тысяч, и в первую очередь надо ответить на вопрос, а работает ли система в принципе, с тем, чтобы потом, вероятно, затратив больше времени и больше усилий, получить ответ на вопрос, насколько хорошо работает целевая система. Представленная техника появилась совсем недавно, но уже используется в большом промышленном проекте по тестированию библиотек ОС Tinux, что показывает ее масштабируемость.

ПРОГРАММИРОВАНИЕ №6 2008

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком