?

Детальная информация
Таблица Карточка RUSMARC
Название: Введение в технологии верификации: методические указания для курсового проектирования
Авторы: Дробинцев Павел Дмитриевич; Котлярова Лина Павловна
Организация: Санкт-Петербургский государственный политехнический университет. Факультет технической кибернетики
Выходные сведения: СПб., 2012
Коллекция: Учебная и учебно-методическая литература; Общая коллекция
Тематика: Вычислительные машины электронные персональные — Математическое обеспечение; Вычислительные машины электронные персональные
УДК: 004.415.53(043.3)
Тип документа: Учебник
Тип файла: PDF
Язык: Русский
Права доступа: Доступ из локальной сети ИБК СПбПУ (чтение, печать)
Ключ записи: RU\SPSTU\edoc\19048

Разрешенные действия: –

Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети

Группа: Анонимные пользователи

Сеть: Интернет

Аннотация

Рассматриваются современные технологии верификации программного продукта. Приведены и описаны математические модели программ, используемые для проведения формальных доказательств правильности функционирования ПО.

Права на использование объекта хранения

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все Прочитать Печать Загрузить
-> Интернет Все

Оглавление

  • Введение
  • Раздел 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)
  • Литература

Статистика использования

stat Количество обращений: 21
За последние 30 дней: 0
Подробная статистика