Тренинги по применению UniTESK для тестирования ПО и аппаратуры
С 7 по 11 июня в Институте системного программирования РАН пройдет два тренинга по технологии UniTESK:
"Функциональная верификация HDL-моделей аппаратного обеспечения с помощью инструмента CTESK" Тренинг предназначен для разработчиков и верификаторов цифрового аппаратного обеспечения. Практические занятия тренинга нацелены на освоение следующих навыков: формальной спецификации модулей аппаратуры, связывания формальных спецификаций с HDL-моделями, автоматической генерации последовательностей тестовых воздействий, оценки качества тестирования в терминах формальных спецификаций. Требования к участникам: Владение языком программирования Си, знакомство с одним из языков описания аппаратуры (VHDL, Verilog).
"Тестирование на основе моделей с помощью инструмента CTESK" Тренинг предназначен для тестировщиков программного обеспечения, обладающего программным интерфейсом на языке программирования Си. Практические занятия тренинга нацелены на освоение следующих навыков: формальной спецификации требований к ПО, автоматической генерации последовательностей тестовых воздействий, оценки качества тестирования в терминах формальных спецификаций. Требования к участникам: Владение языком программирования Си.
Дополнительную информацию по инструменту CTESK можно найти в разделе Документация.
Продолжительность каждого из тренингов 5 дней (по 8 часов). Стоимость участия в тренинге - 25 тыс. рублей. При участии нескольких человек от одной организации предоставляются скидки. По вопросам участия обращайтесь к Александру Константиновичу Петренко по тел. (495)912-53-17 доб. 4404 или по электронной почте
Открыт проект SemaTESK по тестированию семантических анализаторов
В ИСП РАН разработан метод SemaTESK (Semantics Testing Kit) автоматической генерации множеств тестов для фронт-эндов в трансляторах. Метод ориентирован на тестирование анализаторов статической семантики. Наиболее известные методы генерации семантических тестов работают путем фильтрации предварительно сгенерированных более или менее случайным образом синтаксических тестов. В отличие от этих методов, SemaTESK позволяет непосредственно генерировать тесты для контекстных условий. Это очень ощутимо сокращает время генерации и позволяет достигать соответствующие критерии полноты. Метод SemaTESK специфицирования статической семантики позволяет формализовать неформальные требования, содержащиеся в нормативных документах (например, в стандартах). Метод включает в себя язык SRL для компактного формального специфицирования контекстных условий. Метод инструментально поддерживается прототипным генератором STG для эффективной генерации множеств тестов из SRL-спецификаций. Метод SemaTESK был успешно применен в ряде проектов, в том числе по тестированию анализаторов статической семантики языков C и Java.
Выпущена версия 2.3 инструмента разработки тестов JavaTESK, поддерживающего технологию UniTESK для платформы Java. Основные изменения:
Расширены возможности моделирования асинхронных взаимодействий. Введена конструкция expect event для быстрого создания тестов асинхронных систем в стиле TTCN. Улучшено управление состоянием модели.
Добавлена возможность генерации документации по javadoc комментариям в спецификациях.
В отчетах о тестировании найденные ошибки группируются по типам, известные (ранее найденные и занесенные в базу) ошибки отделяются от вновь возникших.
В отчетах о тестировании улучшено представление значений объектов, возникших в ходе тестирования (например, параметров и возвращаемых значений методов).
Инструмент JavaTESK 2.3 можно скачать на странице Скачать.
Итоги года
В 2008 году технология UniTESK активно применялась для создания тестовых наборов для проверки соответствия стандартам в следующих проектах.
Разработка и сопровождение тестового набора для проверки соответствия стандарту Linux Standard Base.
Разработка тестов POSIX-совместимой операционной системы реального времени.
Построение тестов для встроенных систем авионики, поддерживающих стандарт ARINC-653.
Развитие инструментов UniTESK было нацелено на поддержку работ в проектах и общее повышение надежности.
Кроме того, продолжались исследования по теоретическим основам тестирования, методам автоматизации разработки тестов для телекоммуникационных протоколов и распределенных систем, методам тестирования микропроцессов конвейерной архитектуры и их отдельных блоков, методам построения тестов для математических библиотек. Также велись работы по созданию инструментария для верификации драйверов ОС Linux.
Нашими коллегами в этом году было защищено 3 диссертации.
И. Б. Бурдоновым — по теме «Теория конформности для функционального тестирования программных систем на основе формальных моделей» на степень доктора физико-математических наук.
В. В. Рубановым — по теме «Автоматизация построения инструментария кросс-разработки программного обеспечения для расширяемых встраиваемых систем» на степень кандидата физико-математических наук.
А. С. Камкиным — по теме «Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций» на степень кандидата физико-математических наук.
В 2008 году вышла монография И. Б. Бурдонова, А. С. Косачева и В. В. Кулямина «Теория соответствия для систем с блокировками и разрушением», посвященная теоретическим основам тестирования распределенных систем.
Доклады о результатах исследований и отдельных проектов проводились на следующих конференциях и семинарах.
Использование JavaTESK при тестировании интеграционных компонентов Вымпелкома
С начала 2008 года для тестирования интеграционных компонентов на платформе ETL (Extract, Transform, Load), использующихся для пакетной интеграции ПО в коммерческой компании «Вымпелком», применяется инструмент JavaTESK. Использование инструмента повысило качество тестирования, значительно сократило время регрессионного тестирования и затраты ресурсов на изменения и доработку тестов при изменении требований к компонентам.
