model-checking

model-checking@asvk.cs.msu.ru

130 обсуждения

Выставление оценок АСВК
by model checking course mailing list 18 Май '10

18 Май '10

Дамы и господа, Завтра будут проставляться оценки АСВК. 1. Как вы можете заметить по таблице, есть ряд проблем, я надеюсь, что до завтра они будут исправлены: гр. 420: Кравченко Анна Николаевна -- нет копии решения второго задания. гр. 421: Ковальчук Алина Олеговна - нет копии решения пятого задания. гр. 422: Кабанов Сергей Александрович - нет копии решения пятого задания. Староверов Антон Юрьевич - нет копии решения пятого задания. 2. Ну и следующие товарищи завтра утром приходят на комиссию: гр. 420: Мезенцев Павел Юрьевич Тарасов Георгий Николаевич Шкалев Антон Сергеевич гр.421: Колесин Максим Сергеевич гр. 422: Довгаль Сергей Сергеевич Кириллов Александр Кириллович Мищенко Александр Игоревич С уважением, Константин Савенков.

1 0

Re: [model-checking] Проставление оценок практикума
by model checking course mailing list 16 Май '10

16 Май '10

Проставление оценок АСВК будет проходить в среду, 19 мая, с 12 до 14 (т.е. после комиссии) в к.758. К тому моменту, я надеюсь, мы проверим всё ещё не проверенное, а вы пришлёте всё неприсланное. С уважением, Константин Савенков. 16.05.2010 11:43, Alexander Fingerov пишет: > Здравствуйте, > скажите, пожалуйста, когда можно будет проставить зачёт с оценкой для > группы кафедр АСВК? > > С уважением, Александр Фингеров.

1 0

Допуск к экзамену и автоматы
by model checking course mailing list 05 Май '10

05 Май '10

Уважаемые студенты, Ещё не все работы проверены, поэтому окончательных оценок по практикуму пока нет. 1. Студенты, получающие "отлично" автоматом: гр. 420: 1. Астахова Александра Сергеевна 2. Бердников Юрий Евгеньевич 3. Леонов Николай Николаевич 4. Палевич Владимир Александрович гр.421: 1. Потапов Данила Сергеевич 2. Потапов Дмитрий Борисович 3. Третьяк Елена Викторовна гр.422: 1. Блажевич Ксения Игоревна 2. Чемерицкий Евгений Викторович 3. Щербинин Виктор Владимирович гр.427: 1. Кирсанов Сергей Владимирович гр.428: 2. Коляскина Екатерина Николаевна 3. Кравец Алексей Сергеевич В ходе проверки работ этот список может быть дополнен. 2. Следующим студентам каф. АСВК практикум не может быть зачтён в данный момент: гр.420: 1. Мезенцев Павел Юрьевич 2. Тарасов Георгий Николаевич 3. Шкалев Антон Сергеевич гр.421: 1. Колесин Максим Сергеевич гр. 422: 1. Довгаль Сергей Сергеевич 2. Кириллов Александр Кириллович 3. Мищенко Александр Игоревич Вас я ожидаю на комиссию по практикуму 19 мая к 9:00 в ауд.758. Приносите решённые/исправленные задания практикума (возможно, что ими дело не ограничится и придётся решать задачи на месте). 3. Следующие студенты не могут быть допущены к экзамену в силу того, что они не работали по курсу -- нет достаточного количества зачтённых заданий практикума и не написана положительно ни одна контрольная: гр.420: 1. Тарасов Георгий Николаевич 2. Шкалев Антон Сергеевич гр.421: 1. Колесин Максим Сергеевич гр.422: 1. Довгаль Сергей Сергеевич 2. Мищенко Александр Игоревич гр. 424: 1. Жданов Максим Валерьевич 2. Зубарев Михаил Алексеевич 3. Корищенко Дмитрий Константинович 4. Раков Юрий Викторович гр. 425: 1. Кулаков Дмитрий Михайлович 2. Чурбанов Петр Александрович гр. 427: 1. Борисенко Олег Дмитриевич 2. Воробьев Станислав Михайлович 3. Изотов Виталий Юрьевич 4. Комиссаров Иван Владимирович 5. Фионов Сергей Сергеевич гр. 428: 1. Михов Олег Валерьевич Эти студенты отправляются сразу на пересдачу экзамена, поскольку проверить владение навыками верификации на моделях в рамках обычного экзамена не представляется возможным. А пока я подумаю, каким образом можно такую проверку устроить на пересдаче. Видимо, это будет ряд задач. Возможно, что студенты АСВК, успешно сдавшие комиссию по практикуму, будут по итогам допущены к экзамену. К сожалению, ресурсов для проведения комиссии по практикуму для всех студентов из второго списка у меня нет. С уважением, Константин Савенков.

1 0

Слайды
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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking