Пособие соответствует содержанию специальной дисциплины "Распределенные алгоритмы и протоколы" направления подготовки магистров 552800 "Информатика и вычислительная техника".В первой главе приведен обзор основных средств языка Promela свободнораспространяемой системы верификации Spin. Вторая глава посвящена описанию верифицируемых свойств в системе верификации Spin. В третьей главе на нетривиальных примерах демонстрируется разработка нескольких моделей. В частности, строятся модели программных систем: протокола выбора лидера, известной старинной логической задачи и криптографического протокола аутентификации Нидхама — Шредера. В четвертой главе описана курсовая работа по верификации нетривиальной системы логического управления с несколькими вариантами заданий. Модернизация лекционного курса "Распределенные алгоритмы и протоколы" для магистров ФТК СПбГПУ выполнена при частичной поддержке фирмы "Интел" (договор № SPB/R&D/139/2006 от 16.11.2006 г. Санкт-Петербургского государственного политехнического университета и "Интел Текнолоджис"). Предназначено для студентов старших курсов факультета технической кибернетики, также может быть интересно аспирантам, программистам и исследователям в области информатики.

Печатается по решению редакционно-издательского совета Санкт-Петербургского государственного политехнического университета.

• Оглавление
• Введение
• Глава 1. Обзор языка спецификации моделей Promela
• Глава 2. Описание верифицируемых свойств средствами Рготеіаи Spin
• Глава 3. Примеры задач для верификации в Spin
• Глава 4. Описание курсовой работы “Разработка контроллера светофоров наперекрестке и его верификация”
• Библиографический список
• Приложение А. Установка и настройка системы Spin с GUI XSpin
• Приложение В. Код алгоритма Нидхама — Шредера на языке Ргошеіа