Верификация сетевых протоколов Санкт-Петербургский Государственный Электротехнический Университет «ЛЭТИ» Команда разработчиков Андрей Магляс Антон Никитин. - презентация

1 Верификация сетевых протоколов Санкт-Петербургский Государственный Электротехнический Университет «ЛЭТИ» Команда разработчиков Андрей Магляс Антон Никитин Евгений Бранзург Константин Шведов Руководитель проекта Сергей Павлов Технический руководитель Василий Соловьев

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

3 Сетевой протокол Сетевой протокол набор правил, позволяющий осуществлять соединение и обмен данными между двумя включёнными в сеть компьютерами (сторонами). Разные протоколы зачастую описывают лишь разные стороны одного типа связи; взятые вместе, они образуют стек протоколов. Названия «протокол» и «стек протоколов» также указывают на программное обеспечение, которым реализуется протокол.

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

5 Описание протокола Сторона 1 Сторона 2

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

7 Обнаружение ошибок

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