?

Details
Table Card RUSMARC
Title: Введение в язык Promela и систему комплексной верификации Spin: учебное пособие
Creators: Шошмина Ирина Владимировна; Карпов Юрий Глебович
Organization: Санкт-Петербургский государственный политехнический университет
Imprint: Санкт-Петербург: Изд-во Политехн. ун-та, 2010
Electronic publication: Санкт-Петербург, 2021
Collection: Учебная и учебно-методическая литература; Общая коллекция
Subjects: Программирования языки; Вычислительные машины электронные персональные — Программирование
UDC: 004.42(075.8); 004.438(075.8)
Document type: Tutorial
File type: PDF
Language: Russian
Speciality code (FGOS): 09.00.00
Speciality group (FGOS): 090000 - Информатика и вычислительная техника
DOI: 10.18720/SPBPU/2/si21-78
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Record key: RU\SPSTU\edoc\65027

Allowed Actions: –

Action 'Read' will be available if you login or access site from another network Action 'Download' will be available if you login or access site from another network

Group: Anonymous

Network: Internet

Annotation

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

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

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
Internet Authorized users SPbPU Read Print Download
-> Internet Anonymous

Table of Contents

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

Usage statistics

stat Access count: 34
Last 30 days: 0
Detailed usage statistics