A quantitative, model-based approach to the safety verification problem for general processing systems operating in the discrete time domain is presented It is recognized that the operation of most of these systems involves both discrete and continuous characteristics. Therefore, an appropriate modeling framework is proposed, within which models of purely discrete, purely continuous and hybrid systems of arbitrary complexity can be constructed consistently. The models developed can then be incorporated into a safety verification formulation, which allows the identification of potential hazards that may occur while operating such systems, together with the combinations of events that lead to them. Apart from the dynamic process model, the data required for carrying out the analysis include the space of possible disturbances and the set of operating regimes that are considered to be unsafe or undesirable from the operability point of view. The formulation results in a mixed-integer optimization problem. A number of simple example problems presented illustrate the main ideas of the proposed technique, and the solution of an industrial-scale case study demonstrates its applicability.