АНИС

• Введение
• Установка АНИС
  • Программное обеспечение
  • Процедура установки
  • Правила активации расширения
  • Виды рабочих проектов
• Подготовка формальной модели
  • Написание исходных текстов модели
  • Импорт/экспорт модели из Rodin
  • Трансляция модели в Python
  • Нетранслируемые конструкции языка Event-B
  • Структура генерируемого кода на Python
  • Настройка средств тестирования. Проверка аксиом и инвариантов
  • Уточнение констант и несущих множеств
• Интеграция с монитором
  • Поддерживаемый монитор
  • Описание формата трасс. Настройка среды
  • Добавление нового формата трасс
• Разработка медиатора
  • Интерфейсы классов
  • Методика разработки медиатора
  • Пример применения методики
  • Программная реализация медиатора
• Верификация в АНИС
  • Выполнение верификации
  • Отладка
• Отчеты о покрытии модели
  • Сбор покрытия
  • Критерии покрытия модели
  • Генерация отчета о покрытии модели
  • Состав отчета о покрытии модели
  • Удаление несущественных элементов из отчета
• Динамическая верификация без VSCode
  • Подготовка окружения
  • Загрузка исходных файлов
  • Трансляция модели
  • Трансляция трасс
  • Проверка трасс