model-checking Март 2008

model-checking@asvk.cs.msu.ru

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

Небольшое добавление по поводу третьего задания
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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Март 2008