Детальная информация
| Название | Введение в технологии верификации: методические указания для курсового проектирования |
|---|---|
| Авторы | Дробинцев Павел Дмитриевич ; Котлярова Лина Павловна |
| Организация | Санкт-Петербургский государственный политехнический университет. Факультет технической кибернетики |
| Выходные сведения | СПб., 2012 |
| Коллекция | Учебная и учебно-методическая литература ; Общая коллекция |
| Тематика | Вычислительные машины электронные персональные — Математическое обеспечение ; Вычислительные машины электронные персональные |
| УДК | 004.415.53(043.3) |
| Тип документа | Учебник |
| Тип файла | |
| Язык | Русский |
| Права доступа | Доступ из локальной сети ИБК СПбПУ (чтение, печать) |
| Ключ записи | RU\SPSTU\edoc\19048 |
| Дата создания записи | 12.04.2012 |
Разрешенные действия
–
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
| Группа | Анонимные пользователи |
|---|---|
| Сеть | Интернет |
Рассматриваются современные технологии верификации программного продукта. Приведены и описаны математические модели программ, используемые для проведения формальных доказательств правильности функционирования ПО.
| Место доступа | Группа пользователей | Действие |
|---|---|---|
| Локальная сеть ИБК СПбПУ | Все |
|
| Интернет | Все |
|
- Введение
- Раздел 1. Верификация и тестирование.
- Методы обеспечения качества программного обеспечения
- Методы и особенности тестирования
- Методы автоматизации тестирования
- Инструментарий тестирования
- Формальный подход к проблеме обеспечения качества ПО
- Математический аппарат моделей программ
- Обзор моделей программ
- Инструментарий верификации
- Сравнительный анализ средств верификации
- Раздел 2. Математический аппарат моделей программ.
- Сети Петри
- Конечные автоматы
- Регулярные множества и выражения
- Алгебры параллельных процессов
- CSP (Communicating Sequential Processes) [4]
- CCS (Calculus of Communicating Systems) [Mil]
- Транзиционные системы, агенты и среды
- Темпоральные логики
- Формальные языки проектирования.
- SDL
- MSC
- UML
- Раздел 3. Методы верификации ПО
- Методы верификации
- Нотации описания систем
- Дедуктивные методы верификации
- Методы проверки на модели
- Методы верификации
- Раздел 4. Системы верификации ПО.
- Инструменты формализации
- VDM (Vienna Development Method) [Jones90]
- Z [Spivey88]
- B [Abrial96]
- RAISE (Rigorous Approach to Industrial Software Engineering) [Mil90]
- Lotos [LOTOS88]
- EDT [edt]
- Автоматические верификаторы
- HOL(Higher Order Logic) [Gordon93]
- Isabelle [Nipkow02]
- PVS
- CATS (CASL Tool Set) [cats]
- Инструментарий для проверки на модели
- SMV (Symbolic Model Verifier)
- Spin
- Kronos [kr]
- MEIJE [mj]
- Murphi [mur]
- VRS
- Раздел 5. Верификация требований к программным системам
- Общая схема технологии автоматизированной верификации и тестирования
- Используемые формальные языки
- Основы метода базовых протоколов
- Базовые протоколы
- Язык базовых протоколов
- Базовый протокол в MSC
- Система верификации VRS
- Поиск ошибок в спецификациях
- Модуль проверки свойств системы на основе SDL спецификаций
- Модуль поиска недетерминизмов
- Модуль проверки аннотированных спецификаций
- Модуль генерации трасс
- Модуль клиента VRS
- Учебный пример POTS(Plain Old Telephone System)
- Литература
Количество обращений: 21
За последние 30 дней: 0
