We demonstrate how Colured Petri Nets (CPN) can be used to enhance a
traditional software specifications document for an elevator
controller. The traditional specification is given in a textbook. It
includes a description of the desired functionality of the controller
and a description of the subject domain (floors, buttons, cages,
etc.). Based on the given specification we build a CPN model, which is
a coherent description that ties together different pieces of the
given specification. The CPN model is used to argue for the
correctness of the specification. Using simulation, we investigate a
number of scenarios. For each scenario, we check that if a controller
is implemented in compliance with the specification, it will ensure
the desired effects in the subject domain (e.g., that each request is
eventually served).