Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 12
Описание файла
PDF-файл из архива "Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 12 страницы из PDF
Железнодорожное расписание станции.На железнодорожной станции имеется набор платформ и путей, на которыемогут прибывать поезда, известны номера прибывающих поездов, время ихприбытия и отправления, а также станции отправления и назначения. Системаподдержки железнодорожного расписания станции должна обеспечиватьвозможность формирования расписания, внесения в него изменений и выдачуполезной информации (например, список поездов до указанной станцииназначения).634. Система поддержки составления расписания занятий .Система должна обеспечивать возможность составления расписания занятийдля некоторого учебного заведения, внесения в расписание изменений и выдачуполезной информации (например, по итоговому расписанию получитьрасписание указанной группы на заданный день). В расписании должныфиксироваться время и место проведения занятия, предмет и преподаватель,проводящий занятие, а также номер группы, для которой это занятиепроводится.
Расписание не должно содержать коллизий (например, разныезанятия не должны пересекаться друг с другом по месту и времени ихпроведения).5. Планирование автобусного движения в районе .В районе имеется несколько автовокзалов, у каждого из которых есть рядпосадочных площадок. Между автовокзалами курсируют рейсовые автобусы,для каждого рейса фиксируется станция отправления и назначения, посадочнаяплощадка, с которой происходит отправление, а также время посадки в автобуси время в пути.
Система поддержки планирования автобусного движениядолжна обеспечивать возможность добавлять/удалять новые рейсы, вноситьизменения в уже имеющиеся рейсы и выдавать полезную справочнуюинформацию (например, для указанного автовокзала определять все рейсы,отправляющиеся с заданной посадочной площадки и т.д.).6. Заказ и учет товаров в ″бакалейной лавке″.В ″бакалейной лавке″ для каждого товара фиксируется место хранения(определенная полка), количество и поставщик этого товара. Системаподдержки заказа и учета товаров должна обеспечивать возможностьдобавления/удаления нового товара, изменения информации об имеющемсятоваре (например, при изменении количества товара и т.д.) и выдачинеобходимой справочной информации (например, список товаров, количествокоторых необходимо пополнить).7. Управление библиотекой.В библиотеке осуществляется регистрация всех читателей и ведутся каталогипоступивших в библиотеку книг, кроме того для каждого читателя фиксируетсяинформация о том, какие книги находятся у него на руках в данный момент.Система поддержки управления библиотекой должна обеспечиватьвозможность добавления/удаления читателей и соответственно книг в каталоги,регистрацию взятых и возвращенных читателем книг, а также выдаватьполезную справочную информацию (например, о наличии в данный моментуказанной книги и т.д.).8.
Управление памятью на диске.Система обслуживает запросы процессов на использование памяти. Процессможет запросить новую область памяти указанной длины, вернуть ее. Привыделении области памяти по запросу процесса этот процесс становитсявладельцем данной области. Различные процессы могут получать доступ к64памяти на чтение и запись. Определение и изменение прав доступа к указаннойобласти памяти осуществляется только ее владельцем. Неявная иалгебраическая спецификация должны описывать широкий спектр стратегийуправления памятью.9.
Информационное табло по состоянию авиарейсов.На табло отражается следующая информация о рейсе: номер рейса, пунктвылета, время прилета по расписанию, ожидаемое время прилета, статус(отложен, вылетел, прилетел). Система поддержки информационного таблодолжна обеспечивать добавление и удаление информации о рейсах, а такжевнесение изменений в состояние табло, если произошло некоторое событие(например, вылет какого-то рейса отложен на N минут, произошла посадкасамолета указанного рейса и т.д.)10. Управление версиями программного проекта.Программный проект представляет собой некоторую совокупность программ,каждая программа в свою очередь состоит из файлов, файлы связаны друг сдругом отношением ″использует″.
Для каждого файла может существоватьнесколько его вариантов и для каждой программы соответственно несколько ееверсий. Конкретный вариант файла однозначно идентифицируется именемфайла и номером варианта, аналогично версия программы идентифицируетсяименем программы, номером версии и списком вариантов файлов. Каждаяверсия программы должна быть замкнута по отношению ″использует″.
Системаподдержки управления версиями должна обеспечивать возможность создаватьновые варианты файлов и новые версии программ, добавлять и исключатьварианты файлов из версий без нарушения указанной замкнутости, т.е. нельзя,например, удалить из версии какой-то вариант файла, если он используетсяоставшимися файлами.11. Система поддержки составления расписания поездов на железной дороге .Железная дорога представляет собой сеть станций, связанных между собойпутями, (причем могут существовать как однопутные, так и двухпутныеперегоны), на каждой станции имеется N путей, для каждого перегона известновремя, необходимое для его прохождения.
В расписании указывается списокпоездов данной железной дороги с указанием маршрутов их следования(маршрут следования задается списком станций, на которых останавливаетсяпоезд) и временем прибытия/отправления на станции маршрута. Расписаниедолжно быть свободно от коллизий, т.е. на пути перегона так же, как и на путистанции не может находиться одновременно более одного поезда. Системаподдержки составления расписания должна обеспечивать возможностьдобавления и удаления новых маршрутов, внесения изменений в ужесоставленное расписание, а также выдачу полезной информации (например, порасписанию всей железной дороги получить расписание для указаннойстанции).6512.
Управление процессами.Специфицируется набор операций, при помощи которых планировщикоперационной системы поддерживает очереди процессов к ресурсам (например,к устройству ввода/вывода, памяти, процессору, порту ввода/вывода другогопроцесса), при этом внешние операции и/или прерывания, при помощи которыхпользовательские процессы обращаются к планировщику (возбуждаюттребование на обслуживание планировщиком) не рассматриваются.Планировщик поддерживает следующие структуры данных: набор ресурсов,набор процессов, порты ввода/вывода процессов. Набор операций долженпозволять строить и модифицировать перечисленные структуры данных,размещать процесс в очередях к ресурсам, изымать процесс из очереди.13. Утилита make.Утилита получает на вход список файлов и функцию, которая для каждогофайла выдает список файлов, от которых он зависит (например, поиспользованию типов данных).
Кроме того утилита использует в качествевходных данных совокупность файлов. Все файлы, которые утилита получаеткак исходные данные (прямо или косвенно), должны принадлежать этойсовокупности. Результатом утилиты должен стать список файлов –транзитивное замыкание исходного списка. Список-результат долженопределять порядок обработки файлов: каждый «зависящий» файл не долженопережать в списке ни один из файлов, от которого он зависит.14.
Бронирование авиабилетов.В системе бронирования авиабилетов имеется набор авиарейсов, на которыеможно бронировать билеты. Для каждого рейса фиксированы пунктыотправления и назначения, а также дата и время вылета. Система должнаобеспечивать возможность добавления/удаления рейсов, бронированиябилетов /отказа от брони и выдавать полезную справочную информацию(например, об имеющихся свободных местах на рейс и т.д.)15. Управление счетами в банке.В системе обеспечивается регистрация клиентов банка, каждый из которыхможет иметь в этом банке 0 или более счетов.
Любой счет имеет неснижаемыйостаток, по каждому счету ведется баланс. Система поддержки управлениясчетами в банке должна обеспечивать возможность добавления и удаленияклиента банка, открытие и закрытие счета для клиента, просмотр баланса счета,снятие и добавление денег на счет, а также выдавать полезную справочнуюинформацию (например, все счета данного клиента и т.д.).16. Управление аптечной сетью.В аптечную сеть населенного пункта объединены несколько аптек. Всеимеющиеся в аптеках препараты сгруппированы по категориям(жаропонижающие, болеутоляющие и т.д.), по каждой аптеке фиксируетсяинформация о наличии или отсутствии в ней данного препарата. Системадолжна обеспечивать возможность формирования своей информационной базы(добавлять/удалять аптеку в сеть, добавлять/удалять соответствующие66наименования препаратов указанной категории) и выдавать справочнуюинформацию полезного содержания (например, о наличии данного препарата вуказанной аптеке или в сети аптек, все препараты указанной категории и т.д.)17.
Туристическое бюро.Справочная система по обслуживанию туристического бюро содержитинформацию о загрантурах. Для каждого тура фиксируется место егопроведения (страна, курорт, отель), категория отеля проживания, время ипродолжительность тура, а также его стоимость и, возможно, некотораядополнительная информация. Система должна обеспечивать возможностьнаполнения и изменения своей информационной базы – добавлять/удалятьтуры, вносить изменения в данные о туре (например, при изменении стоимоститура), а также выдавать полезную справочную информацию (поиск туров покурорту, в указанной ценовой категории, в заданном диапазоне времени и т.д.)18.
Бюро кредитных историй.Бюро кредитных историй обслуживает сеть банков. В бюро ведется регистрацияклиентов, бравших кредиты в банках этой сети. По каждому кредитуфиксируется банк, выдавший кредит, размер кредита, а также состояниепогашения кредита (кредит в процессе погашения, кредит погашен,невозвращенный кредит). В системе должна быть предусмотрена возможностьрасширения обслуживаемой сети за счет включения в нее нового банка. Крометого система должна обеспечивать возможность добавления нового клиента исоответственно нового кредита к уже имеющемуся клиенту, внесенияизменений о состоянии кредита (например, при погашении кредита), а такжеосуществлять поиск полезной справочной информации (например, находитьвсех клиентов с плохой/хорошей кредитной историей, все невозвращенныекредиты данного банка и т.д.).Методические рекомендацииРазработка спецификации программного интерфейса системы должнаначинаться с определения набора основных операций (функций), которыенеобходимо включить в состав интерфейса.