Детальная информация
Название | Технология программирования. Верификация параллельных и распределенных программных систем: учебное пособие |
---|---|
Авторы | Карпов Юрий Глебович |
Организация | Санкт-Петербургский государственный политехнический университет |
Выходные сведения | Санкт-Петербург: Изд-во Политехн. ун-та, 2010 |
Электронная публикация | Санкт-Петербург, 2020 |
Коллекция | Учебная и учебно-методическая литература ; Общая коллекция |
Тематика | Вычислительные системы — Программирование ; Сложные системы — Моделирование ; верификация ; тестирование ; учебники и пособия для вузов |
УДК | 004.415.5(075.8) |
Тип документа | Учебник |
Тип файла | |
Язык | Русский |
Код специальности ФГОС | 09.00.00 |
Группа специальностей ФГОС | 090000 - Информатика и вычислительная техника |
DOI | 10.18720/SPBPU/2/si20-987 |
Права доступа | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
Ключ записи | RU\SPSTU\edoc\63694 |
Дата создания записи | 30.10.2020 |
Разрешенные действия
–
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Группа | Анонимные пользователи |
---|---|
Сеть | Интернет |
Учебное пособие соответствует содержанию авторского курса "Технология программирования. Верификация параллельных и распределенных программных систем" для студентов, обучающихся по направлению 230100 магистерской подготовки "Информатика и вычислительная техника". Рассмотрены вопросы актуальности проблемы верификации сложных программных систем, разрабатываемых для критических применений. Изложены темпоральные логики LTL, CTL и CTL*, используемые для спецификации свойств параллельных и распределенных систем, представлены алгоритмы верификации реагирующих систем для случаев, когда свойства их поведения представлены формулами логик CTL и LTL. Главное внимание уделено ясности изложения: введенные темпоральные логики объясняются на большом числе примеров, алгоритмы верификации подробно разъясняются, каждая глава сопровождается задачами. Предназначено для студентов высших учебных заведений, обучающихся по направлению "Информатика и вычислительная техника", для преподавателей, инженеров и научных работников.
Печатается по решению редакционно-издательского совета Санкт-Петербургского государственного политехнического университета.
Место доступа | Группа пользователей | Действие |
---|---|---|
Локальная сеть ИБК СПбПУ | Все |
|
Интернет | Авторизованные пользователи СПбПУ |
|
Интернет | Анонимные пользователи |
|
- ОГЛАВЛЕНИЕ
- Предисловие
- Глава 1. Проблема верификации
- Глава 2. Темпоральные логики
- Глава 3. Алгоритм model checking для CTL
- Глава 4. Алгоритм model checking для LTL
- Заключение
- Библиографический список
Количество обращений: 38
За последние 30 дней: 1