В данной работе проводится разработка web-интерфейса для верификатора NuSMV с возможностью графического задания описания модели, ее отображения и визуализации контрпримеров. Для этого сначала выполняется обзор и анализ существующих графических интерфейсов для систем Model Checking, формируются требования для разрабатываемой системы. В качестве практической части реализуется приложение с клиент-серверной архитектурой, предоставляющее пользователю возможность графического взаимодействия с верифицируемой моделью, проводится функциональное и модульное тестирование основных компонентов приложения.

This document describes the web-interface development for the NuSMV verifier with the possibility of graphic creation and display the description of the model, also with the possibility of visualization counterexamples. For this, there are presented review and comparative analysis of existing graphical representations for Model Checking systems, and then formation requirements for the developed system. As a practical part, it describes the implementation of application with a client-server architecture allows user possibility of graphical interaction with a verifiable model, also there are presented functional and module testing of main app components.

• ВВЕДЕНИЕ
• 1. Анализ существующих решений
  • 1.1. Критерии оценивания
  • 1.2. Обзор и анализ графических интерфейсов
    • 1.2.1. gNuSMV
    • 1.2.2. NuSMV GUI
    • 1.2.3. NuSeen
    • 1.2.4. ВКР «Разработка Web-frontend для NuSMV»
    • 1.2.5. iSpin
    • 1.2.6. Supremica
  • 1.3. Итоги
• 2. Постановка задачи
  • 2.1. Цели создания
  • 2.2. Функциональные возможности
  • 2.3. Требования к программному обеспечению
    • 2.3.1. Серверная часть
    • 2.3.2. Клиентская часть
  • 2.4. Вывод
• 3. Проектирование архитектуры системы
  • 3.1. Архитектура приложения
  • 3.2. Режимы работы
  • 3.3. Серверная часть
  • 3.4. Клиентская часть
    • 3.4.1. Компоновка интерфейса
    • 3.4.2. Графический редактор
  • 3.5. Вывод
• 4. Разработка системы
  • 4.1. Стек технологий
    • 4.1.1. Back-end
    • 4.1.2. Front-end
  • 4.2. Разработка серверной части
    • 4.2.1. API
    • 4.2.2. Генерация и разбор исходного файла
    • 4.2.3. Верификация
  • 4.3. Разработка клиентской части
    • 4.3.1. Основные модули
    • 4.3.2. Используемые библиотеки
    • 4.3.3. Дизайн
  • 4.4. Вывод
• 5. Тестирование системы
  • 5.1. Тестируемые компоненты
  • 5.2. Тестирование сервера
  • 5.3. Тестирование клиента
  • 5.4. Вывод
• ЗАКЛЮЧЕНИЕ
• СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
• ПРИЛОЖЕНИЕ 1. ЛИСТИНГИ