The formal specification of the requirements of complex real-time systems