Для данной в третьем задании программы и построенной для неё модели:
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.
Крайний срок сдачи – 13 мая. Зачёт по практикуму АСВК будет выставлен
также 13 мая.
С уважением,
Константин Савенков.
