?

Details
Table Card RUSMARC
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

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

Annotation

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

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
-> Internet All

Table of Contents

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

Usage statistics

stat Access count: 21
Last 30 days: 0
Detailed usage statistics