Compositional verification of an ATM switch module using interface recognizer/suppliers (IRS)
Mohammadamin Jahanpour, E. Cerny · 2002
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 inter-actions 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.