Сотрудники UniTESK Lab провели исследование применимости UniTESK к задаче тестирования протоколов с установлением соединения на примере «минимального» протокола с установлением соединения ABRACADABRA

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

К настоящему моменту в UniTESK Lab накоплен значительный опыт автоматизированного тестирования датаграммных протоколов, известных также как протоколы без установления соединения. В качестве примеров можно указать протоколы IPv6, IPsec, UDP, ICMP и др.

С целью расширить область применения технологии UniTESK сотрудники UniTESK Lab провели исследование по разработке тестового набора для «минимального» протокола с установлением соединения ABRACADABRA. «Минимальность» протокола заключается в том, что данный протокол поддерживает все ключевые особенности рассматриваемого класса протоколов и, одновременно лишен сложных оптимизаций управления соединением и потоком данных, встречающихся в индустриальных протоколах, таких как TCP, RSCP и других. Протокол ABRACADABRA представляет собой упрощённый пример протокола с установлением соединения, которому, при всей его простоте, присущи все основные черты телекоммуникационных протоколов с установлением соединения. Протокол ABRACADABRA использовался для оценки применимости формальных методов (Formal Description Techniques, FDT) к формализации телекоммуникационных протоколов.

Важной особенностью данной работы является то, что технология UniTESK позволяет автоматизировать тестирование важнейших для протоколов с установлением соединения действий – таймаутов и повторных передач, что оказывается невозможным при использовании многих других методов автоматизации тестирования. Сравнение с другими языками формального описания протоколов показало, что размер спецификации протокола ABRACADABRA на расширении языка Си приблизительно равен размеру спецификаций на языках Estelle и Lotos, то есть технология UniTESK позволяет достигать более высокого уровня автоматизации тестирования, нежели другие методы автоматической генерации тестов их формальных спецификаций при аналогичном размере формальной спецификации.

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