Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System. - Paul C. Attie; David H. Lorenz; Aleksandra Portnova; Hana Chockler (CBSE, 2006)