Детальная информация

Название: Разработка Web-интерфейса для верификатора Spin: бакалаврская работа: 09.03.01
Авторы: Бояркин Никита Сергеевич
Научный руководитель: Ицыксон Владимир Михайлович
Организация: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Выходные сведения: Санкт-Петербург, 2017
Коллекция: Выпускные квалификационные работы; Общая коллекция
Тематика: формальная верификация; проверка моделей; конечный автомат; верификатор Spin
Тип документа: Выпускная квалификационная работа бакалавра
Тип файла: PDF
Язык: Русский
Код специальности ФГОС: 09.03.01
Группа специальностей ФГОС: 090000 - Информатика и вычислительная техника
DOI: 10.18720/SPBPU/2/v17-4080
Права доступа: Доступ по паролю из сети Интернет (чтение, печать, копирование)

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

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

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

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

Аннотация

В данной работе описывается процесс разработки веб-интерфейса для верификатора Spin с возможностью интерактивного конструиро­вания конечных автоматов. Охватываются следующие этапы цикла разработки программного обеспечения: анализ, проектирование, реализация и тестирование.Кроме того, производится обзор популярных решений для формальной верификации программных систем и ихс равнение по введен­ным критериям.

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

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

Оглавление

  • ВВЕДЕНИЕ
  • 1. Анализ подходов
    • 1.1. Проверка моделей
    • 1.2. Темпоральные логики
      • 1.2.1. Темпоральная логика линейного времени LTL
      • 1.2.2. Темпоральная логика ветвящегося времени CTL
      • 1.2.3. Временная темпоральная логика ветвящегося времени TCTL
      • 1.2.4. Расширенная темпоральная логика ветвящегося времени CTL*
    • 1.3. Сравнительный анализ подходов к проверке моделей
      • 1.3.1. Cadence SMV
      • 1.3.2. NuSMV
      • 1.3.3. UPPAAL
      • 1.3.4. HyTech
      • 1.3.5. Spin
    • 1.4. Вывод
  • 2. Постановка задачи
    • 2.1. Назначение и цели создания интерфейса
    • 2.2. Требования к программному обеспечению
      • 2.2.1. Серверное программное обеспечение
      • 2.2.2. Клиентское программное обеспечение
    • 2.3. Требования к оформлению и верстке страниц
    • 2.4. Функциональные возможности
      • 2.4.1. Режим редактирования
      • 2.4.2. Режим конструктора
    • 2.5. Требования к производительности
    • 2.6. Вывод
  • 3. Проектирование архитектуры системы
    • 3.1. Клиент-серверное взаимодействие
    • 3.2. Режимы работы
    • 3.3. Серверная часть
      • 3.3.1. Проверка целостности и корректности клиентского запроса
      • 3.3.2. Подготовка к запуску верификатора Spin
    • 3.4. Клиентская часть
      • 3.4.1. Функциональные блоки
      • 3.4.2. Конструктор конечных автоматов
    • 3.5. Вывод
  • 4. Разработка системы
    • 4.1. Используемый стек технологий
      • 4.1.1. Серверные технологии
      • 4.1.2. Клиентские технологии
    • 4.2. Сервер
      • 4.2.1. Система журналирования
      • 4.2.2. Подготовка к запуску верификатора Spin
      • 4.2.3. Запуск процессов
    • 4.3. Клиент
      • 4.3.1. Система журналирования
      • 4.3.2. Основные модули
      • 4.3.3. Конструктор
      • 4.3.4. Дизайн
    • 4.4. Вывод
  • 5. Тестирование системы
    • 5.1. Определение тестируемых компонентов
    • 5.2. Тестирование сервера
      • 5.2.1. Тестирование проверок корректности клиентского запроса
    • 5.3. Тестирование клиента
      • 5.3.1. Тестирование команд конструктора
      • 5.3.2. Тестирование преобразования конечных автоматов в текстовое представление
      • 5.3.3. Тестирование производительности
    • 5.4. Вывод
  • ЗАКЛЮЧЕНИЕ
  • СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
  • ПРИЛОЖЕНИЕ А. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПОДХОДОВ К ПРОВЕРКЕ МОДЕЛЕЙ
  • ПРИЛОЖЕНИЕ Б. РЕАЛИЗАЦИЯ СЕРВЕРА
  • ПРИЛОЖЕНИЕ В. РЕАЛИЗАЦИЯ КЛИЕНТА
  • ПРИЛОЖЕНИЕ Г. ТЕСТИРОВАНИЕ

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

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