Господа,
Для данной в третьем задании программы и построенной для неё модели:
1. Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в
модели быть не должно. Вывод верификатора по проверке свойства поместить
в текстовой файл с именем task4_safety_out.txt.
2. В модели не должно быть недостижимого кода (unreachable code), за
исключением конечных состояний процессов (-end-). Если такой код в
модели найден, исправить её.
3. Сформулированные в третьей задаче свойства описать в модели с помощью
assertions, проверить с помощью Spin. Возможно потребуется ввести
дополнительные переменные. Модель с assertions приложить в файле с
именем task4_assert.pml. Вывод pan по проверке приложить в файле с
именем task4_assert_out.txt
4. В модели не должно быть циклов бездействия (non-progress cycles), за
исключением:
4.1) цикла, связанного с бесконечным выполнением моделируемой функции
4.2) циклов, соответствующих циклам моделируемой функции, которые
после абстракции предикатов стали бесконечными.
Иными словами, конструкции, добавленные в модель
(например, предназначенниые для моделирования случайных данных) не
должны вносить в модель бесконечных циклов.
Вывод верификатора для проверки отсутствия циклов
бездействия приложить в файле с именем task4_nonprogress_out.txt. Метки
progress, предназначенные для того, чтобы верификатор не обращал
внимания на бесконечные циклы, перечисленные в пунктах 4.1 и 4.2, должны
быть расставлены в модели model_assert.pml.
5. Сформулированные в третьей задаче свойства описать с помощью
логики линейного времени в формате Spin, проверить с помощью Spin. При
этом не должны использоваться какие-либо вспомогательные переменные.
Спецификацию приложить в файле с именем spec.ltl.
Также описать на LTL и проверить свойство, что в ходе одной итерации
функции функция kfree вызывается не более одного раза.
4a. В случае, если модель пришлось изменить:
- описать, почему спецификация не выполняется на исходной модели;
- описать, как изменилась модель и почему;
- описать, почему новая модель адекватна;
- приложить контрпример, выданный pan, в файле counterexample.txt;
- приложить исходную и изменённую модели в файлах task4.pml и
task4_modified.pml;
- приложить вывод pan в файле task4_ver_out.txt.
4b. В случае, если спецификация не выполняется на модели:
- приложить контрпример, выданный pan, в файле counterexample.txt;
- построить по контрпримеру Spin контрпример на исходной программе;
- убедиться в том, что контрпример на исходной программе выполняется;
- приложить контрпример на исходной программе в файле
prog_counterexample.txt. Контрпример должен быть описан в виде
последовательности номеров строк исходной программы и значений переменных.
- приложить модель в файле task4.pml;
- приложить вывод pan в файле task4_ver_out.txt.
4c. В случае, если изменения в модели не потребовались и спецификация
выполняется:
- приложить модель в файле task4.pml;
- приложить вывод pan в файле ver_out.txt.
5. Крайний срок сдачи задания -- 8 мая.
6. При сдаче задания на занятии практикума выслать все указанные выше
файлы на почтоный адрес model-checking(a)lvk.cs.msu.su.
С уважением,
Константин Савенков.
