Name
Abstract | ||
|---|---|---|
This article describes a graphical interval logic that is the foundation of a tool set supporting formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to understand and use. The objective of this article is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of the graphical logic, the article provides some specifications for an elevator system and proves several properties of the specifications. The article also describes the tool set and the implementation. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1145/192218.192226 | ACM Transactions on Software Engineering and Methodology |
Keywords | DocType | Volume |
graphical interval logic,concurrent systems,temporal logic,graphical logic,concurrent system,tool set,temporal property,intuitive graphical representation,software engineer,elevator system,visual languages,concurrent software system,timing diagrams,formal specifications,standard temporal logic,formal specification,automated proof-checking | Journal | 3 |
Issue | Citations | PageRank |
2 | 65 | 7.76 |
References | Authors | |
26 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| L. K. Dillon | 1 | 136 | 13.31 |
| G. Kutty | 2 | 143 | 13.89 |
| L. E. Moser | 3 | 65 | 7.76 |
| P. M. Melliar-Smith | 4 | 2360 | 512.60 |
| Y. S. Ramakrishna | 5 | 534 | 45.81 |