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

Презентация:



Advertisements
Похожие презентации
Предмет изучения кибернетики как теории управления.
Advertisements

Подготовила асс. кафедры СМК Воробьева Т.А.. Программное обеспечение (ПО) - комплекс программ, обеспечивающих обработку или передачу данных, а также предназначенных.
Алгоритмы и исполнители. Алгоритм - описание последовательности действий, строгое исполнение которых приведет к задуманному результату.
СПбГУИТМО, каф. Вычислительной техники Выбор исполнимой модели для описания логики переходов веб- приложений Чепурной Александр Иванович Начный руководитель:
Магистрант кафедры телекоммуникаций и информационных технологий Комиссар Дмитрий Семёнович Руководители: Доцент Резников Геннадий Константинович.
Модель угроз безопасности персональных данных при их обработке в информационных системах АПЭК Выполнил студент Группы 11 инф 112: Сотников П.В. Проверил.
В. Дихтяр ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ (для бакалавров) Российский университет дружбы народов Институт гостиничного бизнеса и туризма Раздел 1.Разработка.
Калугин Александр, PhD, PMP Mercury Development Project Director.
Описания, базовые структуры и этапы анализа систем План I. Цель, структура, система, подсистема, задача, проблема. II. Основные признаки и топологии систем.
Александров А.Г ИТО Методы теории планирования экспериментов 2. Стратегическое планирование машинных экспериментов с моделями систем 3. Тактическое.
ОСНОВЫ ПОСТРОЕНИЯ КОМПЬЮТЕРНЫХ СЕТЕЙ Рахатова Айнура Нурбековна ИС-406 гр.
В. И. Дихтяр ИНФОРМАТИКА Российский университет дружбы народов Институт гостиничного бизнеса и туризма Раздел 3Моделирование объектов и процессов и его.
Разновидности компьютерных сетей. Компьютерная сеть – это совокупность объединенными средствами связи программных и технических средств, предназначенных.
1. Что такое система? 2. Какие виды систем вы знаете? 3. Приведите примеры взаимодействия системы и среды. Укажите входы и выходы. 4. Объясните смысл выражения.
А) сведения об объектах окружающего мира; Б) наука пользования компьютером; В) наука о приемах работы с информацией; Г) сведения об устройствах компьютера;
Технические и программные средства реализации информационных процессов Тема 5-2.
Пакеты передачи данных Виды сетевых протоколов. В локальной сети данные передаются от одной рабочей станции к другой блоками, которые называют пакетами.
Корпоративные и промышленные сети. Корпоративная сеть Первые информационные системы предприятий строились на основе централизованных вычислительных центров.
Программное обеспечение- совокупность всех программ, предназначенных для выполнения на компьютере. Программа- это описание на формальном языке, «понятном»
УПРАВЛЕНИЕ И АЛГОРИТМЫ Управляющий о б ъ е к т О б ъ е к т управления Прямая связь Алгоритм управления Обратная связь Объект (субъект), осуществляющий.
Транксрипт:

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

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

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

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

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

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

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

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