Отчеты о покрытии модели

Для оценки полноты тестирования формальной модели имеет смысл строить и изучать достигаемое тестовое покрытие.

Сбор покрытия

Чтобы включить сбор покрытия, нужно открыть Settings, в разделе Anis > Coverage найти настройку Enabled и установить галочку. После этого во время тестирования будет собираться тестовое покрытие по модели.

Если тесты запускаются повторно, нужно определить, что делать с покрытием: дополнять или перезаписывать. Для этого нужно открыть Settings и в разделе Anis > Coverage задать настройку Overwrite.

Критерии покрытия модели

АНИС поддерживает следующие критерии покрытия формальной модели:

• покрытие событий

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

• покрытие элементов охранных условий событий

• покрытие охранных условий внутри событий по MC/DC

• покрытие элементов внутри отдельных охранных условий событий по MC/DC

Покрытие событий: оценивается, использовалось ли событие во время тестирования (по сути, использовалась ли системная операция, соответствующая событию). По каждому событию составляется количество использований. Оно детализируется на два количества: сколько раз охранное условие события целиком было истинным и сколько раз оно было ложным. Это позволяет оценить, каждая ли системная операция запускалась с успешным результатом и с неуспешным результатом.

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

Покрытие элементов отдельных охранных условий событий: позволяет еще больше детализировать покрытие событий. Охранное условие (как логическое выражение) разбивается на элементы (логические подвыражения) и подсчитывается, сколько раз каждый элемент встретился истинным и ложным. Следующие операции разбиваются для получения элементов:

• конъюнкция;

• дизъюнкция;

• импликация.

Покрытие охранных условий внутри событий по MC/DC добавляет в покрытие охранных условий учет независимого влияния каждого отдельного охранного условия на результат охранного условия события целиком. Для этого строятся все векторы MC/DC для конъюнкции отдельных охранных условий каждого события и подсчитывается количество раз, когда реализовался каждый вектор.

Например, если у события E 3 охранных условия G1, G2, G3, то для покрытия по MC/DC достаточно 4-х векторов. Они приведены в следующей таблице:

№	G1	G2	G3	E
1	True	True	True	True
2	False	True	True	False
3	True	False	True	False
4	True	True	False	False

Каждая строка представляет отдельный вектор. На пересечении строки и столбца показано, какое значение должно принимать отдельное охранное условие в этом векторе.

Покрытие элементов внутри отдельных охранных условий событий по MC/DC аналогично предыдущему критерию покрытия с той лишь разницей, что охранное условие рассматривается как формула (конъюнкция, дизъюнкция, импликация) и ее подформулы становятся элементами для составления векторов MC/DC. Отличие от классического MC/DC в том, что элементы могут содержать логические операции, т.е. при составлении списка элементов учитывается только одна (верхняя) логическая операция в формуле охранного условия.

Генерация отчета о покрытии модели

Чтобы сгенерировать отчет о покрытии модели, нужно воспользоваться задачей (Task). Изначально ее нет и ее нужно создать. После этого ее можно вызывать много раз без пересоздания.

Чтобы создать задачу, нужно:

1. вызвать команду Tasks: Configure Task, выбрать пункт о создании tasks.json из шаблона, выбрать Others в качестве шаблона

2. в открывшемся редакторе файла tasks.json надо описать задачу следующим образом:

{
 "version": "2.0.0",
 "tasks": [
     {
         "label": "Generate Model Coverage Report",
         "type": "process",
         "command": "${command:python.interpreterPath}",
         "args": ["-m", "anis.vscode.report"]
     }
 ]
}

Чтобы сгенерировать отчет, нужно вызвать команду Tasks: Run Task и указать задачу генерации отчета. На вопрос об анализе результатов задачи можно ответить вариантом по умолчанию. Откроется терминал, где будет напечатан вывод команды и, в частности, ошибки.

Чтобы просмотреть отчет, нужно открыть файл anis/coverage/index.html. Удобнее это делать извне VSCode. Для открытия внутри VSCode нужно установить расширение Live Share и открыть им файл отчета.

Состав отчета о покрытии модели

Отчет о покрытии состоит из следующих таблиц:

• покрытие событий

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

• покрытие элементов охранных условий событий

• покрытие охранных условий внутри событий по MC/DC

• покрытие элементов внутри отдельных охранных условий событий по MC/DC

Таблица про покрытие событий содержит следующие столбцы:

• «Событие»: название события

• «Успехов»: сколько раз его охранное условие (целиком) было истинным

• «Неуспехов»: сколько раз его охранное условие (целиком) было ложным

Таблица одна, одна строка соответствует одному событию модели.

Таблица про покрытие отдельных охранных условий событий содержит следующие столбцы:

• «Гард»: название отдельного охранного условия события

• «Успехов»: сколько раз это охранное условие было истинным

• «Неуспехов»: сколько раз это охранное условие было ложным

Таблица составляется для каждого события отдельно, каждая строка соответствует отдельныму охранному условию события.

Таблица про покрытие элементов охранных условий событий содержит следующие столбцы:

• «Номер»: порядковый номер элемента в отдельном охранном условии события

• «Успехов»: сколько раз этот элемент был истинным

• «Неуспехов»: сколько раз этот элемент был ложным

Таблица составляется для каждого отдельного охранного условия, каждая строка соответствует своему элементу охранного условия.

Таблица про покрытие охранных условий внутри событий по MC/DC содержит столбцы для каждого отдельного охранного условия и столбец для количества. Каждой строке соответствует свой вектор MC/DC.

Таблица про покрытие элементов внутри отдельных охранных условий событий по MC/DC содержит столбцы для каждого элемента охранного условия и столбец для количества. Каждой строке соответствует свой вектор MC/DC.

Удаление несущественных элементов из отчета

Не все части отчета о покрытии могут быть покрыты целиком. Для этого есть несколько причин:

• в модели есть служебные события, не соответствующие системным операциям; поэтому нет смысла оценивать их покрытие;

• не все охранные условия события могут принимать оба логических значения; типичными примерами могут быть охранные условия о типах параметров событий, эти охранные условия всегда будут истинными, и еще охранные условия, истинность которых обеспечивается выбором соответствующих модельных сущностей в медиаторе;

• аналогичные доводы можно применить и к элементам отдельных охранных условий.

Эти наблюдения приводят к необходимости не показывать такие части отчета о покрытии, которые заведома не будут покрыты целиком. АНИС позволяет описать эти части и учитывать их при построении покрытия.

Для их описания надо открыть Settings и в нем раздел про Anis > Coverage > Report > Ignore Items. Раздел содержит несколько настроек. Большая часть из них редактируется в файле settings.json в формате JSON, ссылка на открытие редактора размещена вместо области для задания значения настройки. Для упрощения ввода настройки в файле смотрите на подсказки и учитывайте следующее их описание:

Const Events — список событий, чьи охранные условия (целиком) не могут принимать оба логических значения (истина и ложь). Эта настройка вводится как перечисление названий событий и по каждому единственное значение (логическое) и текст с причиной этого факта. Причина будет включена в отчет и подвергнута особому анализу.

Пример:

{
"anis.coverage.report.ignoreItems.constEvents": {
   "event1": {
         "value": true,
         "reason": "Является проверкой типа параметра p"
   }
}
}

Const Guards — список отдельных охранных условий (сгруппированный по событиям), которые могут принимать только одно из логических значений. Пример:

{
"anis.coverage.report.ignoreItems.constGuards": {
   "event1": {
       "guard1": {
             "value": true,
             "reason": "Является проверкой типа параметра p"
       }
   }
}
}

Const Conditions — аналогично предыдущим настройкам, но для элементов охранных условий. Охранное условие задается порядковым номером в формуле, начиная с 0. Пример:

{
"anis.coverage.report.ignoreItems.constConditions": {
   "event1": {
       "guard1": {
           "2": {
             "value": true,
             "reason": "Является проверкой типа параметра p"
           }
       }
   }
}
}

Exclude Events Entirely — список имен событий, которые целиком не показываются в отчете (применяется для служебных событий, не соответствующих системным операциям). Этот список имен можно задать непосредственно на странице Settings.

Exclude Events Mcdc Vectors — список MC/DC векторов для покрытия конъюнкции отдельных охранных условий в одном событии. Вектор задается в виде строки из символов T и F в порядке упоминания охранных условий в событии. Этот порядок можно проверить, открыв модуль события в пакете anis.model.events. Атрибут value означает, должен ли этот вектор встречаться (true значит должен встречаться, false — не должен). Пример:

{
"anis.coverage.report.ignoreItems.excludeEventsMcdcVectors": {
   "event1": {
       "TTFT": {
             "value": true,
             "reason": "Является проверкой типа параметра p"
       }
   }
}
}

Exclude Guards Mcdc Vectors — аналогичная настройка, но векторы сгруппированы сначала по событиям, а внутри событий по отдельным охранным условиям. Пример:

{
"anis.coverage.report.ignoreItems.excludeGuardsMcdcVectors": {
   "event1": {
      "guard1": {
         "TTFT": {
                 "value": true,
                 "reason": "Является проверкой типа параметра p"
         }
      }
   }
}
}