Abstract
This paper describes a specification notation of temporal logic to describe the requirements of real-time systems. The notation is extended by a calculus of occurrences of predicates. Using the logic and the calculus we show that common real-time properties such as durations, number of occurrences, precedence and other properties can be described. It is then used to describe the IEEE 802 Token Bus specification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, and D. L. Dill. Model checking for real-time systems. In Proceedings Symposium on Logic in Computer Science, 1990.
H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Proceedings of the 16th ACM Symposium on the Theory of Computing, pages 51–63, Washington D.C., 1984.
H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal logic. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 173–183, Florida, 1986.
Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Unpublished, 1991.
E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.
D. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. In Proceedings Symposium on Logic in Computer Science, pages 402–413, 1990.
J. Hooman and J. Widom. A temporal-logic based compositional proof system for real-time message passing. In Lecture Notes in Computer Science 366, pages 424–441. Springer-Verlag, Heidelberg, 1989.
F. Jahanian and A. Mok. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, 12:890–904, 1986.
R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, 1989.
B. Moszkowski and Z. Manna. Reasoning in interval temporal logic. In Lecture Notes in Computer Science 164, pages 371–383. Springer-Verlag, Heidelberg, 1983.
Z. Manna and A. Pnueli. Verification of concurrent programs: The temporal framework. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, pages 215–273. Academic Press, London, 1981.
Y. Naik. A temporal approach to requirements specification of real-time systems. To be submitted as a Technical Report, 1991.
J.S. Ostroff. Temporal Logic for Real-time Systems. Research Studies Press, 1989.
A. Pnueli and E. Harel. Applications of temporal logic to the specification of real time systems (extended abstract). In Lecture Notes in Computer Science 331, pages 84–98. Springer-Verlag, Heidelberg, 1988.
R. L. Pickholtz, editor. Local Area Networks and Multiple Access Networks, chapter 1, pages 1–30. Computer Science Press, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Naik, Y. (1991). A temporal approach to requirements specification of real-time systems. In: Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1992. Lecture Notes in Computer Science, vol 571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55092-5_19
Download citation
DOI: https://doi.org/10.1007/3-540-55092-5_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55092-1
Online ISBN: 978-3-540-46692-5
eBook Packages: Springer Book Archive