Login
Search manual

Details

Title Разработка Web-интерфейса для верификатора Spin: бакалаврская работа: 09.03.01
Creators Бояркин Никита Сергеевич
Scientific adviser Ицыксон Владимир Михайлович
Organization Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint Санкт-Петербург, 2017
Collection Выпускные квалификационные работы ; Общая коллекция
Subjects формальная верификация ; проверка моделей ; конечный автомат ; верификатор Spin
Document type Bachelor graduation qualification work
File type PDF
Language Russian
Level of education Bachelor
Speciality code (FGOS) 09.03.01
Speciality group (FGOS) 090000 - Информатика и вычислительная техника
DOI 10.18720/SPBPU/2/v17-4080
Rights Доступ по паролю из сети Интернет (чтение, печать, копирование)
Record key RU\SPSTU\edoc\45410
Record create date 10/20/2017

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

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

Network User group Action
ILC SPbPU Local Network All
Read Print Download
Internet Authorized users SPbPU
Read Print Download
Internet Anonymous
  • ВВЕДЕНИЕ
  • 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. Вывод
  • ЗАКЛЮЧЕНИЕ
  • СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
  • ПРИЛОЖЕНИЕ А. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПОДХОДОВ К ПРОВЕРКЕ МОДЕЛЕЙ
  • ПРИЛОЖЕНИЕ Б. РЕАЛИЗАЦИЯ СЕРВЕРА
  • ПРИЛОЖЕНИЕ В. РЕАЛИЗАЦИЯ КЛИЕНТА
  • ПРИЛОЖЕНИЕ Г. ТЕСТИРОВАНИЕ

Access count: 435 
Last 30 days: 0

Detailed usage statistics