Details

Title Введение в технологии верификации: методические указания для курсового проектирования
Creators Дробинцев Павел Дмитриевич ; Котлярова Лина Павловна
Organization Санкт-Петербургский государственный политехнический университет. Факультет технической кибернетики
Imprint СПб., 2012
Collection Учебная и учебно-методическая литература ; Общая коллекция
Subjects Вычислительные машины электронные персональные — Математическое обеспечение ; Вычислительные машины электронные персональные
UDC 004.415.53(043.3)
Document type Tutorial
File type PDF
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
Read Print Download
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

Detailed usage statistics