Интеграция с монитором

Основная цель пользователя АНИС — проверить трассы, собранные монитором, на формальной модели. Для этого необходимо:

  1. описать формат трасс монитора;

  2. настроить параметры загрузчика трасс;

  3. выполнить команду загрузки трасс.

В результате этих действий АНИС транслирует трассы в тесты (тестовые функции pytest). Выполняя тесты, пользователь проверяет трассы на модели.

Поддерживаемый монитор

На данный момент АНИС поддерживает мониторы одного вида. Он называется Pytest_json. Это мониторы со следующими свойствами:

  1. Все трассы располагаются в одной директории, один файл соответствует одной трассе, имя файла начинается с trace_.

  2. Трассы записаны в формате JSON.

  3. Каждая трасса имеет уникальный идентификатор, он записан внутри файла.

  4. Трасса получена в результате выполнения некоторого pytest-теста, тестом была некоторая функция (возможно, параметризованная), идентификатором трассы является nodeid этого теста.

  5. В файле трассы записан один объект со следующими атрибутами:

    • nodeid теста (строка);

    • начальное состояние окружения, перед выполнением целевой последовательности операций в тесте (объект);

    • массив операций (массив объектов); каждая операция имеет имя (строка) и код завершения (целое число); код 0 означает успешное завершение, остальные коды — неуспешное завершение.

Пример трассы:

{
  "nodeid": "test_fs_search.py::test_chmod[file-prY-pxY-pprN-ppxY]",
  "initial": {
    "init_users": {"user": [1001, 1004, []]},
    "init_groups": [1004],
    "init_files": {
      "/_pparent/parent/obj": [2049, 2228227, 1001, 1004, 33279, {}, ["user::rwx", "group::rwx", "other::rwx"]],
      "/tst_prog": [2049, 21, 0, 0, 33279, {}, ["user::rwx", "group::rwx", "other::rwx"]]
    },
    "init_dirs": {
      "/_pparent": [2049, 2228225, 1001, 1004, 16639, {}, ["user::-wx", "group::rwx", "other::rwx"]],
      "/_pparent/parent": [2049, 2228226, 1001, 1004, 16895, {}, ["user::rwx", "group::rwx", "other::rwx"]]
    },
    "root_dev": 2049,
    "root_ino": 2,
    "root_uid": 0,
    "root_gid": 0,
    "uid": 1001,
    "gid": 1004,
    "umask": 18,
    "exeFile_dev": 2049,
    "exeFile_ino": 21,
    "pid": 312399
  },
  "operations": [
    {
      "syscall": "chmod",
      "proc": "tst_prog",
      "pid": 312399,
      "euid": 1001,
      "egid": 1004,
      "pathname": "/_pparent/parent/obj",
      "mode": 83,
      "perms": 32851,
      "ret": 0
    }, {
      "syscall": "exit_group",
      "proc": "tst_prog",
      "pid": 312399,
      "euid": 1001,
      "egid": 1004,
      "error_code": 0,
      "ret": 0
    }
  ]
}

В этой трассе указан идентификатор теста в атрибуте nodeid, затем начальное окружение — в атрибуте initial, затем последовательность операций — в operations.

Описание формата трасс. Настройка среды

Для настройки АНИС на определенный монитор нужно описать имена атрибутов в файлах-трассах (так как АНИС не фиксирует названия этих атрибутов). Кроме того, нужно задать директорию, в которой находятся файлы с трассами. Для этого нужно сделать следующее:

Формат трассы — это объект со следующими атрибутами:

  • traceId — строковый атрибут, равный имени атрибута трассы с уникальным идентификатором трассы

  • initial — строковый атрибут, равный имени атрибута с описанием начального окружения трассы

  • operations — строковый атрибут, равный имени атрибута с описанием последовательности целевых операций трассы

  • name — строковый атрибут, равный имени атрибута с названием целевой операции

  • ret — строковый атрибут, равный имени атрибута с целочисленным кодом завершения целевой операции

Пример описания формата трассы для трассы из предыдущего примера:

{
  "traceId": "nodeid",
  "operations": "operations",
  "initial": "initial",
  "name": "syscall",
  "ret": "ret"
}

Можно задавать только часть атрибутов. Для остальных атрибутов будут использованы значения по умолчанию:

{
  "traceId": "nodeid",
  "operations": "operations",
  "initial": "initial",
  "name": "name",
  "ret": "ret"
}

Чтобы задать формат трасс, нужно:

  1. Открыть настройки, выбрать настройки для расширения Event-B, настройка для вида монитора уже выбрана (так как поддерживается пока один вид мониторов)

  2. Задать настройку Traces Dir — путь в файловой системе до директории с трассами; в этом пути можно использовать переменную ${workspaceFolder} для обращения к текущему workspace folder;

  3. Задать настройку Trace Format — JSON-объект с форматом трассы; формат JSON-объекта описан выше.

Затем нужно загрузить трассы в АНИС. Для этого нужно выполнить команду Event-B: Load traces. В случае ошибок загрузки диагностика будет размещена в канале Event-B Client. В канале будет перечислен список созданных тестовых модулей с трассами. Их количество и названия должны совпадать с тестами, запускавшимися в мониторе.

Кроме того, нужно перейти на вкладку Testing и убедиться в отсутствии ошибок pytest. Все тесты должны отображаться корректно. Если медиатор еще не написан, pytest не сможет предоставить список тестов. В этом случае необходимо создать файл-заглушку для медиатора. В модельном workspace folder создайте файл mediator.py со следующим текстом:

class TraceTranslator:
    pass

Если впоследствии множество трасс обновится, нужно запускать команду загрузки трасс еще раз.

Добавление нового формата трасс

этот раздел предназначен для разработчиков АНИС; пользователи АНИС могут его пропустить

Если требуется интегрировать АНИС с другим монитором, нужно разработать новый адаптер монитора и пересобрать с ним АНИС.

Задачи адаптера монитора следующие:

  1. транслировать трассы в выходном формате монитора в формат АНИС

  2. предоставлять пользователю возможности по конфигурации транслятора трасс

При необходимости поддержки нового монитора следует обратиться к разработчикам для дальнейших инструкций.