Details
| Title | Технология программирования. Верификация параллельных и распределенных программных систем: учебное пособие |
|---|---|
| Creators | Карпов Юрий Глебович |
| Organization | Санкт-Петербургский государственный политехнический университет |
| Imprint | Санкт-Петербург: Изд-во Политехн. ун-та, 2010 |
| Electronic publication | Санкт-Петербург, 2020 |
| Collection | Учебная и учебно-методическая литература ; Общая коллекция |
| Subjects | Вычислительные системы — Программирование ; Сложные системы — Моделирование ; верификация ; тестирование ; учебники и пособия для вузов |
| UDC | 004.415.5(075.8) |
| Document type | Tutorial |
| Language | Russian |
| Speciality code (FGOS) | 09.00.00 |
| Speciality group (FGOS) | 090000 - Информатика и вычислительная техника |
| DOI | 10.18720/SPBPU/2/si20-987 |
| Rights | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
| Record key | RU\SPSTU\edoc\63694 |
| Record create date | 10/30/2020 |
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 |
Учебное пособие соответствует содержанию авторского курса "Технология программирования. Верификация параллельных и распределенных программных систем" для студентов, обучающихся по направлению 230100 магистерской подготовки "Информатика и вычислительная техника". Рассмотрены вопросы актуальности проблемы верификации сложных программных систем, разрабатываемых для критических применений. Изложены темпоральные логики LTL, CTL и CTL*, используемые для спецификации свойств параллельных и распределенных систем, представлены алгоритмы верификации реагирующих систем для случаев, когда свойства их поведения представлены формулами логик CTL и LTL. Главное внимание уделено ясности изложения: введенные темпоральные логики объясняются на большом числе примеров, алгоритмы верификации подробно разъясняются, каждая глава сопровождается задачами. Предназначено для студентов высших учебных заведений, обучающихся по направлению "Информатика и вычислительная техника", для преподавателей, инженеров и научных работников.
Печатается по решению редакционно-издательского совета Санкт-Петербургского государственного политехнического университета.
| Network | User group | Action |
|---|---|---|
| ILC SPbPU Local Network | All |
|
| Internet | Authorized users SPbPU |
|
| Internet | Anonymous |
|
- ОГЛАВЛЕНИЕ
- Предисловие
- Глава 1. Проблема верификации
- Глава 2. Темпоральные логики
- Глава 3. Алгоритм model checking для CTL
- Глава 4. Алгоритм model checking для LTL
- Заключение
- Библиографический список
Access count: 43
Last 30 days: 0
