Visual Specifications For Modular Reasoning About Asynchronous Systems

We propose a visual specification notation, Modular Timing Diagrams (MTD's), for specifying causality and timing properties of asynchronous, communicating processes. We designed MTD's to have three qualities: (1) the basic operators are simple and intuitive; (2) commonly occurring properties are easily specified; and (3) the model checking procedures are efficient. We demonstrate the first two aspects with examples, and the third with an automated partitioning algorithm for compositional reasoning. We demonstrate the applicability of MTD's by employing them successfully to an asynchronous telephony model with call-forwarding and other features.