Computer Science - Formal Methods - Rodin toolset assignment
دوازده سال پیش منتشر شده
تعداد بازدید: 1328
کد پروژه: 8032
شرح پروژه
Computer Science - Formal Methods - Rodin toolset assignment Question 1 In a university degree programme, students are registered on courses. Students must be enrolled on the degree programme to be registered in a course. There is no need to consider multiple degree programmes - just assume we are modeling a single degree programme. Assume the types STUDENT and COURSE are defined in a context. • Define Event-B variables and invariants that represent the enrolled students in the degree programme and also the courses that students are registered in. Ensure the invariants are sufficiently strong. • Include an event for enrolling a student on the programme. • Include an event for registering a student in a course. Ensure the guards are sufficiently strong. • Include an event for de- enrolling a student from the degree programme. • Include an event for removing a course from the degree programme. Question 2 A hotel reception system allocates quests to rooms. Each room is allocated to at most one guest. When a guest checks in, the system finds a free room and allocates that room to them. When they check-out, the room is de-allocated. Write an Event-B specification of a system that manages the allocations of a fixed set of rooms. Include a check-in operation and a check-out operation. • Define appropriate types for the specification • Define Event-B variables and invariants. • Include events for checking a guest in and checking a guest out of the hotel. • Add an event to the room allocation system to check which room(s) a guest is allocated to. • Extend your B model so that the hotel has a variable set of rooms that can be extended or reduced. Add events to add and remove rooms. Extend the existing events where necessary.
مهارت ها و تخصص های مورد نیاز
بودجه
5,000 تومان تا 100,000 تومان
مهلت برای انجام
20روز
وضعیت مناقصه
بسته
درباره کارفرما
عضویت سیزده سال پیش
