model-checking Апрель 2008

model-checking@asvk.cs.msu.ru

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

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

29 Апр '08

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

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; но е… [View More]

1 0

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

07 Апр '08

Господа (и дамы), Ниже находится текст четвёртого, последнего задания. Перешлите его, пожалуйста, тем вашим коллегам, которые не удосужились подписаться на рассылку. Срок высылки решённого задания -- 25 апреля. Понедельник 28 апреля с 9 утра в аудитории 758 -- зачёт по практикуму для студентов групп кафедры АСВК. Те, кто не прислал какие-то задачи или недоволен полученной оценкой за практикум (она к этому моменту будет выставлена), сможет попытаться поправить эту ситуацию на зачёте. У ст… [View More]удентов других групп такая попытка будет на экзамене. На последней лекции будет консультация к экзамену. Список экзаменационных вопросов к этому моменту будет разослан. На майских праздниках меня здесь не будет. С 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 ------------------------------------ -- С уважением, Константин Савенков. [View Less]

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Апрель 2008