?

Details
Table Card RUSMARC
Title: Верификация распределенных систем: учебное пособие для студентов высших учебных заведений, обучающихся по направлению подготовки магистров в образовательной области «Информатика и вычислительная техника»
Creators: Карпов Юрий Глебович; Шошмина Ирина Владимировна
Organization: Санкт-Петербургский государственный политехнический университет
Imprint: Санкт-Петербург: Изд-во Политехн. ун-та, 2011
Electronic publication: Санкт-Петербург, 2020
Collection: Учебная и учебно-методическая литература; Общая коллекция
Subjects: Вычислительные системы — Программирование; верификация программ; учебники и пособия для вузов
UDC: 004.75(075.8); 004.415.5(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/si20-935
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Record key: RU\SPSTU\edoc\63638

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

Представлены научные результаты в области верификации с помощью метода model checking. В теоретической части пособия рассматриваются проблема верификации, темпоральные логики, алгоритм model checking для LTL, структура Крипке как модель реагирующей системы. В практической части приведен обзор основных конструкций языка Promela системы вери­фикации Spin, на примерах демонстрируется разработка моделей на языке Promela. В последнем разделе изложено содержание курсовой работы по ве­рификации нетривиальной системы логического управления с несколькими вариантами заданий. Предназначено для студентов вузов, обучающихся по магистерской программе «Компьютерное моделирование и распределенные вычисления» по направлениям подготовки магистров «Информатика и вычислительная техника». Может быть также использовано при обучении студентов по на­правлению подготовки «Фундаментальная информатика и информацион­ные технологии», а также при обучении в системах повышения квалифика­ции, в учреждениях дополнительного профессионального образования.

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

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. Проблема верификации
  • 2. Темпоральные логики
  • 3. Алгоритм Model Checking для LTL
  • 4. Обзор языка спецификации моделей Promela
  • 5. Описание верифицируемых свойств средствами Promela и Spin
  • 6. Примеры задач для верификации в Spin
  • 7. Курсовая работа «Разработка контроллера светофоров и его верификация»
  • Библиографический список
  • Предметный указатель

Usage statistics

stat Access count: 90
Last 30 days: 5
Detailed usage statistics