MSc
Lesson Booking System
The object-oriented design of a university room-booking system, paired with an executable model that treats the booking load as a stochastic process and searches for how often the platform must refresh its view.
A software-engineering deliverable in two halves that never meet in code: thirty-four design diagrams for a university classroom booking system, and a Modelica model that simulates it and checks its requirements while it runs. There is no implemented application, deliberately.
- Design half
- 34 draw.io diagrams, plus a LaTeX write-up
- Model half
- 316 lines of Modelica, 7 components, 2 monitors
- Results
- 10 randomised-seed runs passed; a 10-point parameter sweep
- Repository
- VincenzoImp/lesson-booking-system
What it was
The model treats the system as a clocked discrete-event process rather than as CRUD. A room’s availability is a three-state Markov chain with a written transition matrix, resampled every four hours and mapped to capacities of a hundred, fifty or zero seats. Student bookings arrive each minute from a categorical distribution that includes cancellations. Two real university platforms are modelled as sampling relays that re-read the room’s state periodically, so the interesting quantity is how stale the platform’s view is allowed to get.
Two monitors turn the requirements into signals. One raises a safety flag if bookings ever go negative or exceed capacity, and a liveness flag if bookings arrive without the count moving. The other compares the true state against what the platform perceives and tracks the worst discrepancy.
Both campaigns ran and their logs are in the repository: ten runs with randomised seeds, all passing, and a ten-point sweep of the platform’s polling period against an explicit objective that prices a state mismatch heavily and squares the booking error.
What I took from it
Writing the requirement as a monitor rather than as a sentence is what makes the sweep possible. Once “the platform’s view must not drift” is a signal you can plot, choosing how often to poll stops being a judgement call and becomes a search, and the objective function you write down is where the real judgement moved to.