Name
Abstract | ||
|---|---|---|
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 withMTD 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, suchas 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. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-36135-9_15 | FORTE |
Keywords | Field | DocType |
asynchronous telephony model,telephony feature,modular reasoning,asynchronous compositional reasoning rule,visual specifications,asynchronous system,new notation,formal reasoning,efficient polynomial-time model checking,modular reasoning withmtd property,asynchronous systems,compositional reasoning method,message sequence chart | Timing diagram,Asynchronous communication,Programming language,Model checking,Asynchronous system,Computer science,Theoretical computer science,Linear temporal logic,Call forwarding,Modular design,Distributed computing,Formal verification | Conference |
Volume | ISSN | ISBN |
2529 | 0302-9743 | 3-540-00141-7 |
Citations | PageRank | References |
6 | 0.45 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nina Amla | 1 | 318 | 16.23 |
| e allen emerson | 2 | 7683 | 1183.13 |
| Kedar S. Namjoshi | 3 | 948 | 50.41 |
| Richard J. Trefler | 4 | 222 | 14.59 |