Для данной в третьем задании программы и построенной для неё модели:

1. Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод верификатора по проверке свойства поместить в текстовой файл с именем task5_safety_out.txt.

2. В модели не должно быть недостижимого кода (unreachable code), за исключением конечных состояний процессов (-end-). Если такой код в модели найден, исправить её.

3. В модели не должно быть циклов бездействия (non-progress cycles), за исключением:

  3.1) цикла, связанного с бесконечным выполнением моделируемой функции

  3.2) циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными.

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

              Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем task5_nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml.

4.      Перечисленные ниже свойства описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. При этом не должны использоваться какие-либо вспомогательные переменные. Спецификации приложить в файле с именами spec.ltl:

4.1.      В ходе выполнения тела функции рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*.

4.2.      В ходе выполнения тела функции после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*,

4.3.      На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера  ресурсов.

4.4.      В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться  не более одного процесса.

4.5.      В ходе выполнения тела функции, функция kfree вызывается не более одного раза.

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

5a. В случае, если модель пришлось изменить:

- описать, почему спецификация не выполняется на исходной модели;

-  описать, как изменилась модель и почему;

-  описать, почему новая модель адекватна;

-  приложить контрпример, выданный pan, в файле counterexample.txt;

-  приложить исходную и изменённую модели в файлах task5.pml и task5_modified.pml;

-  приложить вывод pan в файле task5_ver_out.txt.

5b. В случае, если спецификация не выполняется на модели:

-  приложить контрпример, выданный pan, в файле counterexample.txt;

-  построить по контрпримеру Spin контрпример на исходной программе;

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

-  приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных.

-  приложить модель в файле task5.pml;

-  приложить вывод pan в файле task4_ver_out.txt.

-  создать вспомогательный файл со спецификацией (например, «spec_1.ltl») для проверки оставшихся свойств.

5c. В случае, если изменения в модели не потребовались и спецификация выполняется:

-  приложить модель в файле task4.pml;

-  приложить вывод pan в файле ver_out.txt.

Крайниe сроки сдачи – неделя 14-18 мая. Самая-последняя-сдача-после-дедлайна будет в зачетную сессию, там же будут выставлены оценки за практикум АСВК (конкретную дату напишу позже).

С уважением,
Константин Савенков.