?

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

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

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

Document access rights

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

Table of Contents

  • ВВЕДЕНИЕ
  • 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. Вывод
  • ЗАКЛЮЧЕНИЕ
  • СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
  • ПРИЛОЖЕНИЕ А. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПОДХОДОВ К ПРОВЕРКЕ МОДЕЛЕЙ
  • ПРИЛОЖЕНИЕ Б. РЕАЛИЗАЦИЯ СЕРВЕРА
  • ПРИЛОЖЕНИЕ В. РЕАЛИЗАЦИЯ КЛИЕНТА
  • ПРИЛОЖЕНИЕ Г. ТЕСТИРОВАНИЕ

Usage statistics

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