Hierarchical interface-based non-blocking verification

In this paper we present a hierarchical method that breaks up a plant into two subsystems, and restricts the interaction of the subsystems by means of an interface. We present a definition for an interface, and define a set of interface consistency properties that can be used to verify if a discrete-event system (DES) is non-blocking. Each clause of the definition can be verified using only one of the two subsystems; thus the complete system model never needs to be constructed.