Details

Title: Технология программирования. Верификация параллельных и распределенных программных систем: учебное пособие
Creators: Карпов Юрий Глебович
Organization: Санкт-Петербургский государственный политехнический университет
Imprint: Санкт-Петербург: Изд-во Политехн. ун-та, 2010
Electronic publication: Санкт-Петербург, 2020
Collection: Учебная и учебно-методическая литература; Общая коллекция
Subjects: Вычислительные системы — Программирование; Сложные системы — Моделирование; верификация; тестирование; учебники и пособия для вузов
UDC: 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-987
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)

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

Учебное пособие соответствует содержанию авторского курса "Технология программирования. Верификация параллельных и распределенных программных систем" для студентов, обучающихся по направлению 230100 магистерской подготовки "Информатика и вычислительная техника". Рассмотрены вопросы актуальности проблемы верификации сложных программных систем, разрабатываемых для критических применений. Изложены темпоральные логики LTL, CTL и CTL*, используемые для спецификации свойств параллельных и распределенных систем, представлены алгоритмы верификации реагирующих систем для случаев, когда свойства их поведения представлены формулами логик CTL и LTL. Главное внимание уделено ясности изложения: введенные темпоральные логики объясняются на большом числе примеров, алгоритмы верификации подробно разъясняются, каждая глава сопровождается задачами. Предназначено для студентов высших учебных заведений, обучающихся по направлению "Информатика и вычислительная техника", для преподавателей, инженеров и научных работников.

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

Document access rights

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

Table of Contents

  • ОГЛАВЛЕНИЕ
  • Предисловие
  • Глава 1. Проблема верификации
  • Глава 2. Темпоральные логики
  • Глава 3. Алгоритм model checking для CTL
  • Глава 4. Алгоритм model checking для LTL
  • Заключение
  • Библиографический список

Usage statistics

stat Access count: 3
Last 30 days: 2
Detailed usage statistics