Requirements Engineering for Reactive Systems: Coloured Petri Nets for an Elevator Controller

This paper presents a model-based approach to requirements engineering for reactive systems; we use an elevator controller as case study. We identify and justify two key properties that a model which we construct must have, namely: (1) controller-and-environment-partitioned, which means constituting a description of both the controller and the environment, and distinguishing between these two domains and between desired and assumed behaviour; (2) use case-based, which means constructed on the basis of a given use case diagram and reproducing the behaviour described in accompanying scenario descriptions. For the case study, we build an executable model in the formal modelling language coloured Petri nets. We demonstrate how this model is useful for requirements engineering, since it provides a solid basis for addressing behavioural issues early in the development process, for example regarding concurrent execution of use cases and handling of failures.