model-checking Март 2011

model-checking@asvk.cs.msu.ru

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

Неподписанные контрольные
by model checking course mailing list 27 Мар '11

27 Мар '11

Дорогие студенты, Среди сданных на прошлой лекции контрольных работ три оказались не подписаны. К счастью, все они -- разных вариантов, так что кто забыл подписать -- пишите мне с указанием варианта. С уважением, Константин Савенков.

1 0

Лекция 20.03.2011
by model checking course mailing list 20 Мар '11

20 Мар '11

Дорогие студенты, Я приболел, поэтому лекции 20 марта не состоится. Семинары будут по расписанию. На следующий лекции я буду крайне признателен следующим парам студентов за объяснительные записки относительно высокой степени совпадения их решений первого задания: 1. Дмитрий Рязанцев (428), Дмитрий Сиващенко (428) 2. Александра Федорова (420), Софья Суханова (428) 3. Сергей Вартанов (427), Павел Камаев (428) В отличие от решений практикума, эти записки должны быть написаны совместно и подписаны обоими участниками. С уважением, Константин Савенков.

1 0

Комментарии ко второму заданию
by model checking course mailing list 17 Мар '11

17 Мар '11

Дорогие студенты, Несколько комментариев ко второму заданию. 1. Я совершенно забыл написать, из чего складываются баллы за него: * LTS отдельных процессов - 10 * программа, строящая LTS - 25 * абстрактная LTS (состояние - значение h) - 20 * модель на promela - 25 * обоснование разницы в количестве состояний - 20 ИТОГО: 100 баллов 2. О том, как понять, какое пространство состояний строит SPIN и чем оно отличается от пространства состояний, которое строит ваша программа было рассказано на последней лекции (см. слайды про ключи SPIN) 3. При построении LTS для состояния, включающего только значение h, размечать состояния счетчиком операторов не нужно. Ну и давайте продлим сроки сдачи до 28 марта. С уважением, Константин Савенков.

1 0

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

05 Мар '11

Господа и дамы, Второе задание по практикуму состоит из четырёх частей. 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, его отображать в виде дуги не нужно). Полученную LTS записать в формате dot и при помощи программного средства dot/GraphViz сгенерировать по ней картинку в формате png. 4. Построить модель параллельной программы из первой задачи на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа достижимых состояний этой модели для значений входных параметров (f.a=1,f.b=2,f.c=3,f.d=4). Обоснуйте, почему количество состояний, подсчитанное при помощи системы Spin, отличается от полученного при построении LTS программой из п.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, это тоже нужно обосновать :-) Последний срок сдачи задания -- 21 марта. Методичку постараюсь выложить в ближайшее время. С уважением, Константин Савенков.

1 0

Подведение итогов по первому заданию
by model checking course mailing list 05 Мар '11

05 Мар '11

Дорогие студенты, Дедлайн по первому заданию прошёл. 6 человек из сдавших на семинаре до сих пор не прислали копии на почту (у вас есть время до 14.03). Работы, просто присланные на почту до 02.03 включительно (не сданные на семинаре) будут проверены со временем. 17 человек не сдавали работы на семинаре и не прислали их на почту. Вы можете сдать их _только_ на семинаре, до 14 марта включительно, число баллов будет умножено на 0.6. 14 марта списки не приступивших к практикуму студентов будут у Березина. В отличие от прошлого года, результаты проверки на плагиат радуют -- в паре обнаруженных случаях совместного творчества соавторы постарались сделать программы непохожими не просто переименованием переменных, но и вынесением функций, изменением порядка вычисления состояний и другими интересными способами, демонстрирующими по крайней мере понимание того, что делает программа. Приложенные усилия стоят того, чтобы не считать это плагиатом :-) К.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Март 2011