model-checking

model-checking@asvk.cs.msu.ru

130 обсуждения

Досрочный экзамен 5 мая
by model checking course mailing list 04 Май '08

04 Май '08

Господа (и дамы), Места в 758 мало, поточные аудитории заняты, поэтому чтобы вам не толпиться в коридоре бестолку, давайте сделаем так: АСВК приходит на экзамен к 9:00, остальные группы -- к 12:00. -- С уважением, Константин Савенков.

1 0

Досрочный экзамен
by model checking course mailing list 29 Апр '08

29 Апр '08

Добрый день, Прежде всего -- прошу прощения за то, что вчера всем пришлось так долго ждать на зачёте АСВК -- мы ещё не отработали процедуру, в следующий раз ;-) будет быстрее. На странице с оценками (http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ) появилась окончательная информация о допуске к досрочному экзамену. Критерии допуска -- субъективные. Если по результатам практикума нам показалось, что студента можно допустить на экзамен с одним вопросом из первых двух разделов, то он допускается. Если ошибки, допущенные при выполнении практикума, заставили нас в этому усомниться -- не допускается. 4-е задания тех, кто в любом случае не будет допущен к досрочному экзамену, будут проверяться по ходу дела дальше, результат этой проверки повлияет на то, порлучите ли вы аналогичную задачу на экзамене. Отдельно хотелось бы сказать про четвёртую задачу. Большинство из вас предпочло не описывать темпоральную спецификацию с оператором until, а ввести кучу вспомогательных переменных-флагов и проверять, фактически, свойство safety. Мы, в общем, закрыли на это глаза, поскольку в условии задания никаких ограничений не вводилось. Замечания и снижение оценки получили лишь те студенты, в чьих работах для того, чтобы разобраться в логике работы вспомогательных переменных пришлось потратить изрядное время. Тем не менее, всем следует ожидать, что мы проверим на экзамене ваше понимание темпоральной логики при помощи дополнительных вопросов-задач. Это относится и к основному, и к досрочному экзамену. -- С уважением, Константин Савенков.

1 0

Зачёт по практикуму , экзамен и всё такое
by model checking course mailing list 23 Апр '08

23 Апр '08

Добрый день. Мы проверили большую часть решений 3-го задания. Напоминаю, что результаты лежат вот здесь, с комментариями: http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ Сегодня-завтра проверим остальные. Присланные решения четвёртых заданий для АСВК будут проверены к зачёту (28.04), для остальных кафедр -- к досрочному экзамену (5.05). Все студенты АСВК должны придти на зачёт 28.04 в ауд. 758, с 9:00 до 14:20 (ну разве что кроме тех, кто уверен, что он написал на 5; но если что, не обессудьте). Лекций 25 апреля и 4 мая НЕ БУДЕТ. Консультация будет за несколько дней перед основным экзаменом, дата будет объявлена ближе к делу. Список экзаменационных вопросов лежит вот здесь: http://docs.google.com/Doc?id=dhf679dj_10dhnfpv28 В билете будет один вопрос из первых двух разделов и один вопрос из последних двух разделов. Досрочный экзамен 5 мая будет проходить в ауд. 758 с 9:00 до 14:00. Информация о допуске к досрочному экзамену будет там же, где и оценки за решённые задачи. Сейчас написано, кто точно НЕ ДОПУЩЕН. У остальных есть шанс. На досрочном экзамене Вы получите один вопрос из первых двух разделов, но в качестве дополнительных вопросов будут даваться вопросы и из последних двух разделов. -- С уважением, Константин Савенков.

1 0

Четвёртое задание
by model checking course mailing list 07 Апр '08

07 Апр '08

Господа (и дамы), Ниже находится текст четвёртого, последнего задания. Перешлите его, пожалуйста, тем вашим коллегам, которые не удосужились подписаться на рассылку. Срок высылки решённого задания -- 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 ------------------------------------ -- С уважением, Константин Савенков.

1 0

Небольшое добавление по поводу третьего задания
by model checking course mailing list 26 Мар '08

26 Мар '08

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

1 0

Результаты проверки первого задания
by model checking course mailing list 21 Мар '08

21 Мар '08

Господа, результаты проверки первого задания выложены сюда: http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ Насколько я понимаю, возможны вопросы с вашей стороны. Ответы на вопросы первого типа ("У меня оценка X, что делать?"): "у меня оценка 'на экзамене'", "у меня оценка 2" -- Вы либо не получили вовремя задание, либо не прислали ответ, либо прислали категорически неправильный ответ. Получите задачу на экзамене. Если Вы -- с АСВК, то получите задачу на специально организованном зачёте. "у меня оценка X, а я хочу Y | X<Y" -- предупредите перед экзаменом и получите соотв. задачу на экзамене. На досрочный экзамен Вы уже не попадаете. Можете попытаться поаппелировать, но врядли Вы в этом преуспеете. "у меня оценка 5" -- всё хорошо, возможно Вы попадёте на льготный приём экзамена. Ответ на вопросы первого типа ("я присылал(а) решение, а у меня стоит 'на экзамене'"): Пишите, разберёмся. -- С уважением, Константин Савенков.

1 0

Статистика решенных заданий
by model checking course mailing list 17 Мар '08

17 Мар '08

Добрый день, Информация о присланных решениях задач практикума доступна по адресу http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ Если по вашему мнению информация в таблице не соответствует действительности, сообщите мне об этом. Оценки в таблице появятся как только, так сразу. Третья задача будет разослана на этой неделе. -- С уважением, Константин Савенков.

1 0

Второе задание
by model checking course mailing list 01 Мар '08

01 Мар '08

Добрый день, Детальная легенда на второе задание: Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа состояний этой модели. Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором. О том, как среди вывода верификатора распознать число состояний модели, вы можете прочитать в руководстве к системе Spin. Результаты необходимо прислать ПО ПОЧТЕ. Срок сдачи задания -- до 14 марта включительно, -- С уважением, Константин Савенков.

1 0

Информация
by model checking course mailing list 29 Фев '08

29 Фев '08

Господа, 1) начиная с сегодня-после-лекции заявки на первую задачу больше не принимаются. 2) тем, кто отправлял заявку на этой неделе и задачи не получил, я отправлю задачи до субботы 3) на следующей неделе, 7 марта, лекции НЕ БУДЕТ (я улетаю в командировку). 4) для тех, кто не был на лекции: помимо задания в легенде, нужно построить модель функции из первой задачи на языке Promela и использовать систему SPIN, чтобы точно оценить число состояний получившейся модели. -- С уважением, Константин Савенков.

1 0

Материалы лекций
by model checking course mailing list 21 Фев '08

21 Фев '08

Господа, слайды лекций доступны по адресу: http://savenkov.lvk.cs.msu.su/mc.html -- С уважением, Константин Савенков. P.S. Настоятельно прошу старост прислать мне списки групп.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking