A graphical environment for the design of concurrent real-time systems
- 1 January 1997
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Software Engineering and Methodology
- Vol. 6 (1) , 31-79
- https://doi.org/10.1145/237432.237438
Abstract
Concurrent real-time systems are among the most difficult systems to design because of the many possible interleavings of events and because of the timing requirements that must be satisfied. We have developed a graphical environment based on Real-Time Graphical Interval Logic (RTGIL) for specifying and reasoning about the designs of concurrent real-time systems. Specifications in the logic have an intuitive graphical representation that resembles the timing diagrams drawn by software and hardware engineers, with real-time constraints that bound the durations of intervals. The syntax-directed editor of the RTGIL environment enables the user to compose and edit graphical formulas on a workstation display; the automated theorem prover mechanically checks the validity of proofs in the logic; and the database and proof manager tracks proof dependencies and allows formulas to be stored and retrieved. This article describes the logic, methodology, and tools that comprise the prototype RTGIL environment and illustrates the use of the environment with an example application.Keywords
This publication has 26 references indexed in Scilit:
- Automatic symbolic verification of embedded systemsIEEE Transactions on Software Engineering, 1996
- The benefits of relaxing punctualityJournal of the ACM, 1996
- VerusACM SIGPLAN Notices, 1995
- Conjoining specificationsACM Transactions on Programming Languages and Systems, 1995
- Validating real-time systems by history-checking TRIO specificationsACM Transactions on Software Engineering and Methodology, 1994
- An old-fashioned recipe for real timeACM Transactions on Programming Languages and Systems, 1994
- A graphical interval logic for specifying concurrent systemsACM Transactions on Software Engineering and Methodology, 1994
- Real-Time Logics: Complexity and ExpressivenessInformation and Computation, 1993
- TRIO: A logic language for executable specifications of real-time systemsJournal of Systems and Software, 1990
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986