Задачи на формальную спецификацию

---

Задачи на построение модели
в системе Event-B 
Каждый студент выбирает одну из задач для выполнения 
индивидуального задания. Студент свободен в выборе задачи, однако 
запрещается двум студентам решать одну и ту же задачу. Номер выбранной 
студентом задачи сообщается по e-mail. Рекомендуется указать три номера, 
чтобы избежать возможного столкновения по номерам с другими студентами. 
Задание из двух частей.
Часть 1. По содержательной постановке задачи формулируются 
требования. Далее строится автоматная программа на языке автоматного 
программирования, определенном в первой лекции по Event-B, см. слайд 21 
презентации. Автоматная программа снабжается инвариантами управляющих 
состояний и общими инвариантами. Для конечных процессов указывается мера, 
которая во второй части задания заменяется на variant. Построение автоматной 
программы проводится в соответствии с технологией автоматного 
программирования, изложенной в середине первой лекции по автоматному 
программированию. 
Результат первой части задания – описание требований и автоматная 
программа с пояснениями для переменных и управляющих состояний – 
оформляется в виде WORD-файла и посылается по электронной почте 
преподавателю. После исправления критических ошибок студент допускается к 
выполнению второй части задания. 
Часть 2. Автоматная программа кодируется на языке Event-B и 
оформляется в виде проекта в системе Rodin. Формулы корректности, 
сгенерированные в системе Rodin, доказываются применением автоматических 
и интерактивных инструментов. Проводится прогон модели на аниматоре. 
Обнаруженные ошибки протоколируются. 
Результат работы – директория проекта в внутри директории workspace – 
посылается преподавателю в виде zip-файла. Дополнительно представляется 
протокол верификации. 
Не фиксируется форма описания результатов задания. Образцом могут 
служить презентации лекций. Тем не менее, это не снижает требований к 
качеству описания, особенно описанию требований. 
Обнаружение ошибок посредством верификации, использование 
уточнений, проведение нетривиальных доказательств и другие неординарные 
особенности будут оцениваться высоко. 
Некоторые более простые задачи снабжены литерой fgo – for girls only. 
Это небольшое послабление не снижает общих требований к выполнению 
заданий. Задания разные по сложности. Однако оценка определяется с учетом 
объема и сложности проведенной работы таким образом, чтобы все студенты 
находились в равных условиях. 
Представленный набор задач для построения модели в Event-B составлен 
в первую очередь по материалам лекций по автоматному программированию и 

---

2 
лекций по системе Event-B. Некоторые задачи оперируют вещественными 
величинами. Построение модели для таких задач потребует импорта теории 
Real. Разрешается вместо этого использовать целочисленную сетку. В задаче 5, 
полное и точное решение которой проблематично, можно ограничиться 
поиском безопасных стратегий для одного, двух, максимум трех перемещений. 
Массивы и последовательности представляются функциями. Можно 
также использовать списки, очереди и другие структуры, импортируя 
соответствующие теории из стандартной библиотеки. 
Список занятых задач
В начале номера занятой задачи стоит минус 
1 Бахарев Александр группа 22161 
2 Девятериков Антон группа 22153 
3 Пищев Иван группа 22162 
4 Хайруллаев Учкун группа 21152 
5 Бояршин Андрей группа 22161 
6 Листопадова Дарья группа 22153 
7 Мухиддинов Даврон группа 21152 
8 Герасимов Федор группа 22161 
10 Дмитриев Вадим группа 22162 
11 Запанов Ринчин группа 22161 
12 Быков Денис группа 22161 
13 Юнусов Вадим группа 22161 
14 Еркович Степан группа 22162 
15 Зинченко Сергей группа 22153 
18 Слобожанин Артем группа 22162 
19 Бахарев Георгий группа 22162 
20 Мартюшев Алексей группа 22162 
21 Дударь Максим группа 22151 
22 Шаранов Дмитрий группа 22153 
24 Насонов Максим группа 22153 

---

3 
-Задача 1 
Имеются следующие дополнения в задаче управления движением на 
мосту. Пусть m – максимальная нагрузка (в килограммах), которую может 
выдержать мост. У каждой машины может быть разный вес. Контроллер 
должен следить за общим весом автомобилей на мосту через существующие 
сенсоры, получая от них сообщения о весе автомобилей. При этом если 
машина въехала на мост с весом X, то при съезде с моста у нее также 
должен остаться вес X. 
-Задача 2 
Имеются следующие дополнения в задаче управления движением на 
мосту. Под мостом периодически проходят корабли. Корабли разные. 
Некоторые корабли обладают небольшим размером и могут проходить 
свободно в любое время. Для других требуется развод моста. Мост нельзя 
разводить, если на нем есть автомобили. В модели должен быть описан не 
только развод мостов, но и движение кораблей, а также ожидание 
кораблями пока откроется мост. Запрос на открытие моста должен 
отправляться при наличии достаточно большого количества кораблей в 
очереди. 
-Задача 3 
Имеются следующие дополнения в задаче управления движением на 
мосту. На мосту имеется смотровая площадка ограниченной вместимости 
(m автомобилей). Автомобиль, едущий с материка, может заехать на 
смотровую площадку, постоять там, а затем уехать назад на материк – не 
заезжая на остров, но подождав, пока автомобили не начнут ехать в нужную 
сторону. А может и продолжить движение в сторону острова. Имеется въезд 
с моста на смотровую площадку и выезд на мост со смотровой площадки. 
Въезд и выезд снабжены сенсорами. 
-Задача 4 
Определить невырожденность квадратной матрицы методом 
эквивалентных преобразований матрицы, используемых в предикатной 
программе «Решение системы линейных уравнений», представленной в 
четвертой лекции по предикатному программированию. 
-Задача 5 
Требуется проложить безопасный маршрут на ровной местности из 
точки А в точку Б. В пределах видимости 20 короновирусников. 
Короновирусник – потенциальный носитель короновирусной инфекции – 
движется в фиксированном направлении с постоянной скоростью 4км/час. 
Маршрут – последовательность точек от А к Б. Можно менять направление 
движения и скорость, но не более 6км/час. Маршрут безопасный, если в 
каждый момент времени расстояние до любого короновирусника 
превышает полтора метра. Требуется проложить безопасный маршрут, либо 
определить, что такой маршрут невозможен. 

---

4 
-Задача 6 (fgo) 
Имеются следующие дополнения в задаче управления движением на 
перекрестке. В начале пешеходного перехода есть кнопка, которую может 
нажать пешеход, чтобы информировать о намерении перейти магистраль. 
Требуется построить контроллер управления светофорами с учетом 
показаний кнопки. 
-Задача 7 
Имеются следующие дополнения в задаче управления движением на 
перекрестке. Имеется постоянно включенный таймер, увеличивающий свое 
показание на единицу через каждую секунду. 25 сек. – время для 
пересечения магистрали пешеходами. 75 сек. – время переключения 
светофора от зеленого к красному для автомобилей. Требуется построить 
контроллер управления светофорами с учетом показаний таймера и 
возможностью изменения отрезков времени между переключениями 
светофоров. 
-Задача 8 
Построить модель «Электронных часов с будильником» из первой 
лекции по автоматному программированию. Дополнительно вводится 
таймер, реализующий пересчет времени через секунду. Изменение таймера 
на секунду должно сопровождаться изменением на секунду времени часов с 
будильником. 
Задача 9 (fgo) 
Построить модель программы «Гадание на кофейных зернах» из 
второй лекции по автоматному программированию. Предварительно 
фиксируется желаемый результат гадания. Разрешается три раза повторить 
гадание, если итоговый результат не совпадает с желаемым. Доказать 
конечность процесса гадания. 
-Задача 10 
Построить модель программы «Управление лифтом» из второй лекции 
по автоматному программированию. Автоматную программу управления 
лифтом необходимо переписать в виде спецификации Event-B. 
Допускаются упрощения, где они возможны и корректны. Вызовы 
гиперфункций придется раскрыть. Можно использовать материалы статьи: 
https://persons.iis.nsk.su/files/persons/pages/lift1.pdf
 
-Задача 11 
Построить модель Протокола чередования битов из второй лекции по 
автоматному программированию. Автоматную программу протокола 
необходимо переписать в виде спецификации Event-B. На входе модели 
протокола бесконечная последовательность блоков данных. Сообщения 
реализуются через переменную – фактически, это очередь длины 1. Потеря 
сообщения моделируется специальным событием стирания сообщения из 
очереди. 

---

5 
-Задача 12 
Построить модель Протокола рукопожатия, устанавливающего 
соединение двух узлов, называемых приемником и передатчиком, 
посредством ненадежных каналов связи, допускающих потерю сообщений. 
Автоматную программу протокола необходимо переписать в виде 
спецификации Event-B.
Ненадежные каналы моделируются процессами M1 и M2. Приемник 
(процесс S) ждет сигнала s начала работы, затем посылает сигналы a 
передатчику (процесс R), пока не получит ответ b, после чего приемник 
посылает сигнал рукопожатия u приемника и завершает свою работу. 
Передатчик, получив сигнал c от приемника, посылает сигнал рукопожатия 
r передатчика и ответ d. На каждый последующий сигнал передатчика c он 
посылает дополнительный ответ d. 
Доказать, что протокол рукопожатия успешно завершает свою работу, 
при условии, что процессы M1 и M2 генерируют выходной сигнал (c и b) 
после некоторого числа входных сигналов (a и d). 
-Задача 13 
Построить модель Протокола Петерсона взаимного исключения 
доступа для двух процессов. Автоматную программу протокола 
необходимо переписать в виде спецификации Event-B.
Алгоритм Петерсона взаимного исключения доступа представлен 
следующей автоматной программой.