model-checking Апрель 2010

model-checking@asvk.cs.msu.ru

1 участники
10 обсуждения

Слайды
by model checking course mailing list 28 Апр '10

28 Апр '10

Дорогие студенты, 1. Выложены слайды 10 и 11 лекций, в первых девяти исправлено приличное количество опечаток. При подготовке к экзамену рекомендуется использовать обновлённые слайды. 2. В пятницу на семинаре могут досдать практикум те, кому не хватило времени сегодня. 3. Постепенно начинают появляться оценки за практикум. В соответствующей графе таблицы они подсвечены разными цветами. То, что не подсвечено -- это не оценка, а так, сумма баллов. 4. Для АСВК -- при незначительном отклонении вниз от оценки "отлично" (например, "3" за одно из заданий при всех остальных "5") в диплом мы поставим вам "5", но это не повлияет на базовый балл на экзамене (т.е. он будет таким, как при "4"). С уважением, Константин Савенков.

1 0

Новости
by model checking course mailing list 27 Апр '10

27 Апр '10

Дорогие студенты, Я благополучно вернулся из Астаны. Завтра будет выставлены (в табличку) отметки за практикум студентам АСВК, совмещённый с приёмом 5-го задания. Остальные группы тоже могут сдать 5-е задание, но с меньшим приоритетом, чем АСВК. Вообще критерии оценки ваших трудов (замечу, что критерии более чем либеральные): "отлично" -- от "2 и 5 задания на '5', среди 1, 3 и 4 допускается до 2-х оценок '4' (третья -- "5") " до "все задания на отлично". "хорошо" -- "2, 5 и 4 задания на '4', 1 и 3 -- на '3' " до нижней границы "отлично". "удовлетворительно" -- от "2, 5 и 4 задания на '3', 1 и 3 не сданы" до нижней границы "отлично". В ведомости и зачётки эти данные будут проставлены во время зачётной сессии, о дате напишу. Информацию о присланных решениях 5-го задания постараюсь разместить сегодня. По поводу непроверенных вторых и пятых заданий: ответственный (за это) человек обещал проверить их до завтра, в крайнем случае -- проверим завтра. Экзамен будет проходить с 7 по 10 июня, в три дня. С уважением, Константин Савенков.

1 0

Проверено 4-е задание (LTL)
by model checking course mailing list 19 Апр '10

19 Апр '10

Дорогие студенты, Оценки проставлены в таблицу. Комментарий по оценкам: одно и то же количество правильно написанных формул может соответствовать различным оценкам. Так, если человек написал правильно сложную формулу и допустил незначительные ошибки в двух других формулах, то он получает "три". Если же человек написал верно простую формулу, а в двух других продемонстрировал непонимание семантики темпоральных операторов -- он получает "два". Как-то так. В целом -- с LTL большие проблемы. Тем, у кого задание не зачтено, крайне рекомендуется к экзамену закрыть этот пробел. Попросите у товарищей их варианты, прорешайте, сравните свои ответы с правильными. Остальным тоже рекомендуется -- не у всех свойства в заданиях были разнообразными. С уважением, Константин Савенков.

1 0

Re: [model-checking] Model Checking Task 5
by model checking course mailing list 12 Апр '10

12 Апр '10

Олег, совершенно верно! :-) С уважением Константин Савенков. Олег Борисенко пишет: > Во всех именах файлов, наверное, должно быть task5? > > > 2010/4/12 model checking course mailing list <model-checking(a)lvk.cs.msu.su>: > >> Для данной в третьем задании программы и построенной для неё модели: >> >>

1 0

Model Checking Task 5
by model checking course mailing list 12 Апр '10

12 Апр '10

Для данной в третьем задании программы и построенной для неё модели: 1. Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод верификатора по проверке свойства поместить в текстовой файл с именем task4_safety_out.txt. 2. В модели не должно быть недостижимого кода (unreachable code), за исключением конечных состояний процессов (-end-). Если такой код в модели найден, исправить её. 3. Сформулированные в третьей задаче свойства описать в модели с помощью assertions, проверить с помощью Spin. Возможно, потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем task4_assert.pml. Вывод pan по проверке приложить в файле с именем task4_assert_out.txt . Нужно учитывать, что верификатор остановить проверку на первой же ошибке, поэтому для того, чтобы проверить все свойства, возможно, придётся сделать несколько вариантов модели и ли использовать конструкции #ifndef. 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: 1. В каждом вычислении рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*. 2. В каждом вычислении, после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*, 3. На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера ресурсов. 4. В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться не более одного процесса. 5. В ходе одной итерации функции функция kfree вызывается не более одного раза. Возможно, для разумной проверки свойств модель придётся изменить: исправить ошибки, повысить уровень детальности, добавить системные вызовы, не вошедшие в модель, по-другому описать алгоритм доступа к критической секции ит.п. 6a. В случае, если модель пришлось изменить: - описать, почему спецификация не выполняется на исходной модели; - описать, как изменилась модель и почему; - описать, почему новая модель адекватна; - приложить контрпример, выданный pan, в файле counterexample.txt; - приложить исходную и изменённую модели в файлах task4.pml и task4_modified.pml; - приложить вывод pan в файле task4_ver_out.txt. 6b. В случае, если спецификация не выполняется на модели: - приложить контрпример, выданный pan, в файле counterexample.txt; - построить по контрпримеру Spin контрпример на исходной программе; - убедиться в том, что контрпример на исходной программе выполняется; - приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. - приложить модель в файле task4.pml; - приложить вывод pan в файле task4_ver_out.txt. - создать вспомогательный файл со спецификацией (например, «spec_1.ltl») для проверки оставшихся свойств. 6c. В случае, если изменения в модели не потребовались и спецификация выполняется: - приложить модель в файле task4.pml; - приложить вывод pan в файле ver_out.txt. Крайний срок сдачи – 26 апреля. АСВК может сдавать на семинарах 28 апреля, при выставлении зачёта. С уважением, Константин Савенков.

1 0

Re: [model-checking] Model Checking Task 4
by model checking course mailing list 12 Апр '10

12 Апр '10

Илья, Неправильно: для сдачи "только по почте" сегодня -- крайний день, для сдачи "на семинаре + копия по почте" крайний день -- среда. Задания, сданные сегодня по почте вряд ли будут проверены до среды. С уважением, Константин Савенков. iliya letunov пишет: > Добрый день, > Правильно ли я понимаю, что можно сегодня отослать решение по 4 заданию через интеренет и если в нём будут ошибки, то я смогу исправить их в среду на семинаре? > С уважением, > Летунов Илья. >

1 0

Сроки сдачи 4-го задания
by model checking course mailing list 11 Апр '10

11 Апр '10

Дорогие студенты, В силу того, что сдача 4-го задания сопровождается большим количеством итераций и исправлений, крайний срок сдачи на семинаре переносится на среду, 14 апреля. В среду сдавать могут студенты всех групп, не успевшие этого сделать. Обращаю внимание, что это касается только сдачи на семинаре -- дедлайн по "почтовой" сдаче не меняется, это понедельник 12 апреля. С уважением, Константин Савенков.

1 0

Результаты проверки решений практикума
by model checking course mailing list 08 Апр '10

08 Апр '10

Дорогие студенты. Решения второго задания будут проверены до зачёта. Решения третьего задания уже проверены, результаты в таблице. Обращаю ваше внимание, что есть довольно много тех, у кого в решении третьего задания есть существенные ошибки, которые не позволяют в полной мере оценить решение. Здесь у нас было два варианта: 1) принять точку зрения, что не бывает наполовину правильных программ и не зачесть задания и 2) отложить выставление оценки за задание до исправления недочётов в ходе выполнения задания №5. Мы решили последовать второму варианту. Те, кто не прислал сданное на семинаре задание -- присылайте, иначе оно не будет зачтено. С уважением, Константин Савенков.

1 0

Второй комментарий к 4 заданию
by model checking course mailing list 07 Апр '10

07 Апр '10

Дорогие студенты, Обращаю внимание, что в тексте 4 задания сказано, что свойства, описанные на LTL, должны быть инвариантны к прореживанию. Это означает, что именно так (инвариантно к прореживанию) нужно интерпретировать словесную формулировку свойств. В частности, "P истинно один раз" в формулировке, инвариантной к прореживанию, означает, что в трассе есть один неразрывный участок, на котором истинно P. С уважением, Константин Савенков.

1 0

Комментарий к 4-му заданию
by model checking course mailing list 05 Апр '10

05 Апр '10

Дорогие студенты, Обращать внимание следует на второе письмо -- к первому файл не прикрепился. И, увы, во второе письмо вкралась опечатка. Должно быть так: > Например, формула <>!a удовлетворяет данному требованию, а формула !<>a -- нет. С уважением, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Апрель 2010