Abstract
This report is a case study applying temporal logic to specify the operation of a bank of identical elevators servicing a number of floors in a building. The goal of the study was to understand the application of temporal logic in a problem domain that is appropriate for the method, and to determine some of the strengths and weaknesses of temporal logic in this domain. The case study uses a finite state machine language to build a model of the system specification, and verifies that the temporal logic specifications are consistent using this model. The specification aspires to be complete, consistent, and unambiguous.
This work is sponsored by the Department of Defence.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barringer, H. Up And Down the Temporal Way. Computer Journal 30(2):134–148, April, 1987.
Clarke, E.M., Emerson, E.A., and Sistla, A.P. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2):244–263, April, 1986.
Clarke, E. M. and Grumberg, O. Research on Automatic Verification of Finite-State Concurrent Systems. Ann Rev. Computer Science (2):269–290, 1987.
Hoare, C.A.R. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, New Jersey, 1985.
Lamport, L. What Good is Temporal Logic. Information Processing 83: 657–668, 1983.
Pnueli, A. Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Lecture Notes in Computer Science #224: 510–584, 1985.
Rescher, Nicholas and Urquhart, Alasdair. Temporal Logic. Springer-Verlag, Wien, New York, 1971.
Schwartz, M. D. and Delisle, N. M. Specifying A Lift Control System With CSP. In Fourth International Workshop on Software Specification and Design, pages 21–27. The Computer Society of the IEEE, April, 1987.
Wood, W. A Temporal Logic Case Study. Technical Report CMU/SEI-89-TR-24, Software Engineering Institute, 1989.
Woodcock, J. C. P., King, S., and Sorensen, I. H. Mathematics for Specification and Design: The Problem with Lifts. In Fourth International Workshop on Software Specification and Design, pages 265–268. The Computer Society of the IEEE, April, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wood, W.G. (1990). Temporal logic case study. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_21
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive