Таблица | Карточка | RUSMARC | |
Разрешенные действия: –
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Группа: Анонимные пользователи Сеть: Интернет |
Аннотация
Рассматриваются современные технологии верификации программного продукта. Приведены и описаны математические модели программ, используемые для проведения формальных доказательств правильности функционирования ПО.
Права на использование объекта хранения
Место доступа | Группа пользователей | Действие | ||||
---|---|---|---|---|---|---|
Локальная сеть ИБК СПбПУ | Все | |||||
Интернет | Все |
Оглавление
- Введение
- Раздел 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 Подробная статистика |