model-checking Март 2012

model-checking@asvk.cs.msu.ru

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

Итоги приёма первого задания
by model checking course mailing list 27 Мар '12

27 Мар '12

Дорогие студенты, Вчера минуло две недели с дедлайна по первому заданию практикума. Результаты выложены. Давайте подведем итоги. 1. 7 человек прислало решения на почту, 6 из них будут со временем проверены. По поводу ещё одного см. пункт 3. 2. 14 человек не сдали задания, либо не прислали копии решений. Их список уйдет в учебную часть, там их постараются мотивировать приступить к учебе. 3. Плагиат детектед: * Господа Копин (424), Тарасевич (428) и Бабак (422). Баллы за 1.3 аннулированы. В следующий понедельник я ожидаю получить от вас объяснительную с описанием того, кто у кого списывал, подписанную всеми тремя участниками, а также Николаем Мартьяновым из 522 группы. * Госпожа Самохина (425). Баллы за 1.3 аннулированы. От вас объяснительную за подписями вас и Краснова Дениса Олеговича (выпуск ВМК 2011 года). Вашу окончательную судьбу будет решать Березин, а пока я ожидаю, что второе задание каждый из вас выполнит самостоятельно. Ещё несколько человек подошли к вопросу использования чужих решений достаточно творчески, на первый раз не замечу. С уважением, Константин Савенков.

1 0

Итоги дедлайна по первому заданию
by model checking course mailing list 14 Мар '12

14 Мар '12

Дорогие студенты, Дедлайн по первому заданию миновал, при этом есть ряд студентов, которые не приступили к его выполнению (см. https://docs.google.com/spreadsheet/ccc?key=0AhbmHMR5VBIJdFgwcVFnNF9vd3pSdH…). По истечении двух недель с момента дедлайна списки несдавших уйдут в учебную части и к Березину. Учтите, что студенты, не работающие в ходе семестра по курсу, с большой вероятностью не получат дополнительных возможностей пересдать экзамен при возникновении проблем в ходе сессии. Прошу старост групп поинтересоваться у данных студентов, возможно у них есть какие-то уважительные причины. 420: КУРКИН КИРИЛЛ ВЛАДИСЛАВОВИЧ ПУТИЛИН АЛЕКСАНДР ВЛАДИМИРОВИЧ 421: ЕРОФЕЕВ МИХАИЛ ВИКТОРОВИЧ ЗАЧЕСОВ АНТОН АЛЕКСАНДРОВИЧ 422: ВАЛИЕВ КАРИМ РАМИЛЕВИЧ ГАЙДОВ ВИКТОР ВИКТОРОВИЧ ЖУРАВЛЕВ АЛЕКСЕЙ ЮРЬЕВИЧ ЖУРАХОВСКИЙ ОЛЕГ АНДРЕЕВИЧ ЗИМАРИНА ДАРЬЯ СЕРГЕЕВНА КОНДРАТЕНКО АРТЁМ ВИТАЛЬЕВИЧ РЕМЕНЯК МАРИНА ДАНИЛОВНА СОРОКИН АЛЕКСАНДР ИГОРЕВИЧ ТИПИСОВА АЛИСА ОЛЕГОВНА 424: НЕЧАЕВ ЯРОСЛАВ ИГОРЕВИЧ ПОЯРКОВА ДАРЬЯ АЛЕКСАНДРОВНА Кривобородов Егор Васильевич Нетребко Станислав Алексеевич 425: КУПРИКОВ КИРИЛЛ АЛЕКСАНДРОВИЧ ПУЗИКОВ БОРИС ЮРЬЕВИЧ СМАГИН МАКСИМ ВЛАДИМИРОВИЧ 427: ПУСТОВАЛОВ МИХАИЛ АЛЕКСАНДРОВИЧ ЮЩЕНКО ПАВЕЛ АЛЕКСАНДРОВИЧ 428: ГРОШЕВ СЕРГЕЙ ВАЛЕРЬЕВИЧ ДМИТРИЕВ ЕВГЕНИЙ ДМИТРИЕВИЧ МИХАЙЛОВ АЛЕКСАНДР НИКОЛАЕВИЧ ШУБЕРТ АЛЕКСЕЙ ВЛАДИМИРОВИЧ Также ряд студентов не прислали копии сданных решений. Если решения не будут присланы в течение 2-х недель после дедлайна, оценки полученные при сдаче на семинаре, будут аннулированы. С уважением, Константин Савенков.

1 0

Model Checking Task 2
by model checking course mailing list 12 Мар '12

12 Мар '12

Господа и дамы, Второе задание по практикуму состоит из четырёх частей. 1. Построить размеченные системы переходов (LTS) М_1, М_2 функций f и g из первого задания для следующих значений параметров функций f и g: f.a = 1, f.b = 2, g.a = 3, g.b = 4. При этом предполагается, что функции выполняются независимо и никакая другая функция не может влиять на значение глобальной переменной.Состояния LTS должны быть размечены значениями счётчика управления, глобальной переменной и локальных переменных x и y, дуги – выполняемыми операторами. Полученные LTS записать в формате dot и при помощи программного средства dot/GraphViz сгенерировать по ним картинки в формате png. 2. Модифицировать программу из п.3 задания 1 так, чтобы при указании параметра «-lts имя_файла» она строила и сохраняла в указанный файл систему переходов для асинхронной параллельной композиции функций f и g в формате dot (для значений входных параметров(f.a=1,f.b=2,g.a=3,g.b=4)). Состояния LTS должны быть размечены значениями счётчика управления, глобальной переменной и локальных переменных x и y. Дуги должны быть размечены выполняемыми операторами, для операторов ветвления дуги - истинным условием перехода (т.е. для оператора while(x<3) дуга, ведущая в тело цикла, размечается «(x<3)», ведущая на следующий за циклом оператор – «!(x<3)»). Цвет дуг должен зависеть от того, какой процесс выполнил действие. 3. Считая состоянием программы значение переменной h, построить LTS такой модели параллельной программы. Состояния LTS должны быть размечены значением глобальной переменной h (размечать состояния счетчиком операторов не нужно), дуги – выполняемыми операторами, приводящими к изменению переменной h (если действие не приводит к изменению h, его отображать в виде дуги не нужно). Полученную LTS записать в формате dot и при помощи программного средства dot/GraphViz сгенерировать по ней картинку в формате png. 4. Построить модель параллельной программы из первой задачи на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа достижимых состояний этой модели для значений входных параметров (f.a=1,f.b=2,f.c=3,f.d=4). 5. Обоснуйте, почему количество состояний, подсчитанное при помощи системы Spin, отличается от полученного при построении LTS программой из п.2. Баллы за задание: * LTS отдельных процессов - 10 * программа, строящая LTS - 25 * абстрактная LTS (состояние - значение h) - 20 * модель на promela - 25 * обоснование разницы в количестве состояний - 20 ИТОГО: 100 баллов Последний срок сдачи задания -- 2 апреля. Требования к решению Решение задачи должно включать в себя следующие файлы (всего 12 штук, приложены к письму по отдельности): 1. Текстовый файл task.txt c описанием функций f и g. 2. Описание LTS M_1 и M_2 в формате dot в файлах с именами lts_m1.txt и lts_m2.txt, а также сгенерированные по ним картинки в файлах lts_m1.png и lts_m2.png. 3. Исходный код модифицированной согласно п.2 программы в файле group_surname_2.c, описание сгенерированной ей LTS в формате dot в файле lts_m12.dot и сгенерированную по нему картинку в файле lts_m12.png. 4. Описание LTS с состоянием, включающим только значение h, в формате dot в файле abstract_lts_m12.dot и сгенерированную по нему картинку в файле abstract_lts_m12.png. 5. Текстовой файл с расширением group_surname_2.pml с моделью на Promela, текстовой файл log.txt с тем, что выдал верификатор при запуске модели, текстовой файл states.txt с 1) фразой «Согласно верификатору, у модели – N достижимых состояний», где N -- число состояний, выданных верификатором, 2) фразой «В LTS для программы – M достижимых состояний», где М – число, выдаваемое программой из п.2 данной задачи и 3) текстом, описывающим разницу между Mи Nи объясняющим (с точностью до состояния) эту разницу. Дополнительная информация 1. Пример описания LTS в виде графа в формате dot: digraph G { 0 [label=”1,#,1”]; 1 [label=”2,1,1”]; 2 [label=”4,1,1”]; 0 -> 1 [label=”h = a;” color=”red”]; 1 -> 2 [label=”!(h < a)” color=”blue”]; } Графический файл в формате png может быть сгенерирован следующей командой (имя_файла_1 – имя файла с картинкой, имя_файла_2 – имя файла в формате dot): >dot -Tpng -o имя_файла_1 имя_файла_2 2. О том, как среди вывода верификатора распознать число состояний модели, можно прочитать в руководстве к системе Spin (например, здесь: http://spinroot.com/spin/Man/Pan.html#L9). Обратите внимание, что в ходе построения пространства состояний Spin выполняет редукцию частичных порядков, удаление незначащих переменных, слияние состояний, накладывает ограничения на порядок завершения процессов. Более подробно об этом будет рассказано на одной из следующих лекций. 3. Если разница равна 0, это тоже нужно обосновать :-) С уважением, Константин Савенков.

1 0

Копии заданий
by model checking course mailing list 12 Мар '12

12 Мар '12

Дорогие студенты, Напоминаю, что после сдачи задания на семинаре нужно прислать его копию на model-checking(a)lvk.cs.msu.su (до дедлайна). Второе задание по практикуму будет разослано сегодня вечером. Тогда же появятся в таблице результаты сдачи первого задания. С уважением, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Март 2012