Верификация сетевых протоколов Санкт-Петербургский Государственный Электротехнический Университет «ЛЭТИ» Команда разработчиков Андрей Магляс Антон Никитин Евгений Бранзург Константин Шведов Руководитель проекта Сергей Павлов Технический руководитель Василий Соловьев
Введение Программа предназначена для автоматической верификации сетевых протоколов. Что позволяет проверить работоспособность протокола, выявлением основных типов ошибок: Рассинхронизацию Зацикливание А так же ошибки связанные с неправильным описанием протокола
Сетевой протокол Сетевой протокол набор правил, позволяющий осуществлять соединение и обмен данными между двумя включёнными в сеть компьютерами (сторонами). Разные протоколы зачастую описывают лишь разные стороны одного типа связи; взятые вместе, они образуют стек протоколов. Названия «протокол» и «стек протоколов» также указывают на программное обеспечение, которым реализуется протокол.
Конечный автомат Конечный автомат в теории алгоритмов математическая абстракция, позволяющая описывать пути изменения состояния объекта в зависимости от его текущего состояния и входных данных, при условии что общее возможное количество состояний конечно. Конечный автомат является частным случаем абстрактного автомата.
Описание протокола Сторона 1 Сторона 2
Верификация Основной задачей программы является верификация протоколов. Которые описываются как два независимых конечных автомата. Программа проверяя все возможные состояния обоих автоматов и из взаимосвязи на различных этапах находит типовые ошибки. Такая проверка обеспечивает максимальную точность, но при этом занимает довольно много системных ресурсов и времени, так как процесс верификации является «переборным». Процесс верификации был сильно оптимизирован, что позволило существенно сократить затраты памяти, но при этом увеличил время работы.
Обнаружение ошибок
Заключение Данный программный продукт позволяет проверять протокол на наличие как типовых ошибок, так и ошибок связанных с синхронизацией сторон протокола, тем самым позволяет с высокой точностью отладить протокол, для избежание ошибок в его непосредственной работе.