Details
| Title | Введение в технологии верификации: методические указания для курсового проектирования |
|---|---|
| Creators | Дробинцев Павел Дмитриевич ; Котлярова Лина Павловна |
| Organization | Санкт-Петербургский государственный политехнический университет. Факультет технической кибернетики |
| Imprint | СПб., 2012 |
| Collection | Учебная и учебно-методическая литература ; Общая коллекция |
| Subjects | Вычислительные машины электронные персональные — Математическое обеспечение ; Вычислительные машины электронные персональные |
| UDC | 004.415.53(043.3) |
| Document type | Tutorial |
| File type | |
| Language | Russian |
| Rights | Доступ из локальной сети ИБК СПбПУ (чтение, печать) |
| Record key | RU\SPSTU\edoc\19048 |
| Record create date | 4/12/2012 |
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 |
Рассматриваются современные технологии верификации программного продукта. Приведены и описаны математические модели программ, используемые для проведения формальных доказательств правильности функционирования ПО.
| Network | User group | Action |
|---|---|---|
| ILC SPbPU Local Network | All |
|
| Internet | All |
|
- Введение
- Раздел 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)
- Литература
Access count: 21
Last 30 days: 0
