A two-person Software Engineering 2 project at Politecnico di Milano (a.y. 2023/24) that produced no application code on purpose. The deliverable was the specification itself: a RASD (Requirements Analysis and Specification Document) and a DD (Design Document) for a platform where educators publish programming challenges and students submit solutions that are tested and scored automatically.
What the system had to do
The domain is deceptively awkward. A challenge has a lifecycle (drafted, open, closed) and so does a submission, and the two interact: a solution arriving one second after a deadline, a student joining a team mid-challenge, an automated test run that fails for infrastructure reasons rather than because the code was wrong. Most of the work went into pinning down what the system must do in each of those cases before anyone could argue about how to build it.
How the model was verified
The interesting part is that the domain model was not just drawn. It was checked.
- The world and machine were modelled in Alloy, in two versions:
alloy.alsand a deliberately relaxed variant used to see which constraints were actually load-bearing. Running the analyser surfaced states the UML diagrams alone happily permitted, such as combinations of challenge and submission status that should never coexist. - The design was documented with a full UML set: use case, sequence, statechart, component and runtime, and deployment diagrams.
Both documents are in the repository, alongside the Alloy models and the diagram sources.
What I took from it
Formal modelling earns its cost at exactly one moment: when the analyser produces a counterexample you did not believe was reachable. That happened often enough here to change how I read a requirements document. The relaxed second model was the more useful of the two, because removing a constraint and watching what the analyser then allows tells you what that constraint was really for, which a diagram never does.