Visual specifications for modular reasoning about asynchronous systems

We propose a framework that closely ties together visual specification and modular reasoning of asynchronous systems. The basis of the framework is a new notation, called Modular Timing Diagrams (MTD's), for specifying the universal properties about causality and timing of events in an asynchronous system. MTD's are complementary in nature to Message Sequence Charts, that are typically used to specify existential properties. Our framework includes two algorithms for formal reasoning with MTD's. The first is an efficient polynomial-time model checking algorithm. The second is an algorithm for automatically generating an assume-guarantee partitioning of an MTD, that exploits its inherent decompositional structure. We show how to use this decomposition for modular reasoning with MTD properties in conjunction with an asynchronous compositional reasoning rule. To illustrate the notation and our method, we describe a case study where we specified telephony features, such as call forwarding with MTD's, and verified these properties on an asynchronous telephony model. The compositional reasoning methods led to savings of 15%-80% in verification times, and comparable savings in space.