
118 Requirements Engineering for Software and Systems
INVARIANTs—conditions that must hold throughout the execution of the pro-
gram. Here N represents the natural numbers {0,1,2,3, …}. We continue with a
partial description of the behavioral intent of this model.
Notice that the three variables of interest are the platforms, max_trains, and
trains_in_station. e INVARIANT sets constraints on the number of trains in
the station (must be a non-negative number) and the maximum number of trains
in the system (must be a non-negative number and there can be no more than that
number in the station). It continues with platforms as a sequence of t ...