Детальная информация
| Название | Технология программирования. Верификация параллельных и распределенных программных систем: учебное пособие |
|---|---|
| Авторы | Карпов Юрий Глебович |
| Организация | Санкт-Петербургский государственный политехнический университет |
| Выходные сведения | Санкт-Петербург: Изд-во Политехн. ун-та, 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
