We propose an approach to compositional verification of complex systems

based on the interactions at the interfaces of the components. Interactions

at an interface are first recognized by a finite automaton called interface

recognizer/supplier (IRS). Programming IRS as supplier of the interactions

allows us to simulate interactions of one side of the interface while model

checking the other side. We formulate the composition rule and illustrate

the method on an ATM switch module.