Информационная система "Конференции"

VI Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (с участием иностранных ученых)

29-31 октября 2005 года, г. Кемерово, Россия

Тезисы докладов

информационные технологии

Спецификация и верификация протокола с чередованием битов

Тумуров Э.

Институт Систем Информатики СО РАН (Новосибирск)

Цель работы --- разработка технологии построения программ реального времени на примере коммуникационного протокола с чередованием битов (Alternating Bit Protocol, ABP). ABP является протоколом, обеспечивающим надёжную однонаправленную передачу данных от передатчика к приёмнику через ненадёжные каналы, при передаче по которым возможна потеря или искажение сообщений, но не меняется их порядок.

Передача сообщений управляется битом приёмника и битом передатчика, которые вначале совпадают. Сообщение передатчика содержит блок данных, бит передатчика и контрольную сумму. При получении неискажённого сообщения приёмник посылает подтверждение с битом сообщения. Если бит сообщения совпадает с битом приёмника, то приёмник принимает блок данных и инвертирует свой бит. Если сообщение передатчика было потеряно или искажено, то передатчик делает повторную посылку сообщения. Передатчик, получив сообщение от приёмника, при совпадении битов сообщения и собственного, переходит к передаче следующего блока данных.

Формальная спецификация протокола ABP состоит из программы на языке функционального программирования P и условие тождества последовательности блоков, передаваемых передатчиком и получаемых приёмником. Условие корректности записывается во временной логике.

Доказательство условия корректности сводится к доказательству следующей пары утверждений:

очередной блок гарантированно передаётся по ненадёжному каналу без искажений один раз;
пока очередной блок не доставлен, следующий не поступает на вход.

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

Дополнительные материалы: Полный текст доклада
Примечание. Тезисы докладов публикуются в авторской редакции

Ваши комментарии
Обратная связь

[Головная страница]
[Конференции]