Господа (и дамы),
Ниже находится текст четвёртого, последнего задания. Перешлите его,
пожалуйста, тем вашим коллегам, которые не удосужились подписаться на
рассылку.
Срок высылки решённого задания -- 25 апреля.
Понедельник 28 апреля с 9 утра в аудитории 758 -- зачёт по практикуму для
студентов групп кафедры АСВК. Те, кто не прислал какие-то задачи или
недоволен полученной оценкой за практикум (она к этому моменту будет
выставлена), сможет попытаться поправить эту ситуацию на зачёте.
У студентов других групп такая попытка будет на экзамене.
На последней лекции будет консультация к экзамену. Список экзаменационных
вопросов к этому моменту будет разослан.
На майских праздниках меня здесь не будет. С 12 по 25 мая я буду в
командировке. Соответственно, если вы не получите свою оценку по практикуму
на зачёте (это касается студентов АСВК), то к сессии вы допущены не будете, и
помочь вам никто не сможет. Оценка за практикум идёт в диплом.
Соответственно, думайте сами. Особенно это касается господ Ермакова, Салия,
Волкова, Крупа, Попова, Семёнова, Баранова, Любицкого, Петрова и госпожи
Полежаевой.
Экзамен будет после 25 мая. В экзаменационный день будет разбит на две части:
приём экзамена у тех, у кого нет проблем по практикуму и у тех, у кого есть
проблемы.
---- Легенда 4 задания --------
Для данной вам программы и её модели, построенной в ходе решения третьей
задачи:
1. Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в
модели быть не должно. Вывод pan по проверке свойства приложить в файле с
именем safety_out.txt.
2. В модели не должно быть недостижимого кода (unreachable code).
3. Сформулированное в третьей задаче свойство описать в модели с помощью
assertions, проверить с помощью Spin. Возможно потребуется ввести
дополнительные переменные. Модель с assertions приложить в файле с именем
model_assert.prm. Вывод pan по проверке приложить в файле с именем
assert_out.txt
4. В модели не должно быть циклов бездействия (non-progress cycles), за
исключением:
4.1) цикла, связанного с бесконечным выполнением моделируемой функции
4.2) циклов, соответствующих циклам моделируемой функции, которые после
абстракции предикатов стали бесконечными.
Иными словами, конструкции, добавленные вами в модель (например,
дназначенниые для моделирования случайных данных) не должны вносить в модель
бесконечных циклов.
Вывод верификатора для проверки отсутствия циклов бездействия приложить в
файле с именем nonprogress_out.txt. Метки progress, предназначенные для того,
чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в
пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml.
5. Сформулированное в третьей задаче свойство описать с помощью логики
линейного времени в формате Spin, проверить с помощью Spin. Спецификацию
приложить в файле с именем spec.ltl.
a. В случае, если модель пришлось изменить:
* описать в теле письма, почему спецификация не выполняется на исходной
модели;
* описать в теле письма, как изменилась модель и почему;
* описать в теле письма, почему новая модель адекватна;
* приложить контрпример, выданный pan, в файле counterexample.txt;
* приложить исходную и изменённую модели в файлах model.prm и new_model.prm;
* приложить вывод pan в файле ver_out.txt.
b. В случае, если спецификация не выполняется на модели:
* приложить контрпример, выданный pan, в файле counterexample.txt;
* построить по контрпримеру Spin контрпример на исходной программе;
* убедиться в том, что контрпример на исходной программе выполняется;
* приложить контрпример на исходной программе в файле prog_counterexample.txt.
Контрпример должен быть описан в виде последовательности номеров строк
исходной программы и значений переменных.
* приложить вывод pan в файле ver_out.txt.
c. В случае, если изменения в модели не потребовались и спецификация
выполняется:
* приложить модель в файле model.prm;
* приложить вывод pan в файле ver_out.txt.
Во всех случаях письмо должно удовлетворять требованиям:
* письмо написано в формате plain/text без html;
* в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и
utf8 (желательно в кодировке koi8-r).
* к письму должна прилагаться формулировка третьей задачи с файле с именем
task3.txt
------------------------------------
--
С уважением,
Константин Савенков.
