Abstract
TLA (the Temporal Logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, with the intent to facilitate the communication between domain and solution experts in the design of reactive systems.
This work was partly supported by a grant from DAAD and APAPE under the PROCOPE program.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The Existence of Refinement Mappings. Theoretical Computer Science 81(2):253–284, 1991.
M. Abadi and S. Merz. On TLA as as logic. in M. Broy (ed.): Deductive Program Design. Springer-Verlag, NATO ASI series F, 1996.
J.-R Abrial. The B-Book. Cambridge University Press, 1996.
B-core. B-Toolkit. User’s Manual, Release 3.2. Technical Report, B-core, 1996
M. Baudinet. Temporal Logic Programming is Complete and Expressive. In Proc. ACM Conf. on Princinples of Programming Languages, pp. 267–280 (1989)
P. Breuer and J. Bowen. Towards Correct Executable Semantics for Z. In J. Bowen and J. Hall, editors, Proc. 8th Z Users Workshop (ZUM94), Workshops in Computing, pages 185–212. Cambridge, Springer-Verlag, Berlin, 1994.
E.A. Emerson and E.M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2 (1982), pages 241–266.
M. Fisher and R. Owens. An introduction to Executable Modal and Temporal Logics. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Computer Science, pages 1–20, Springer-Verlag, 1993.
M. Fisher. Concurrent METATEM—The Language and its Applications. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Computer Science, Springer-Verlag, 1993.
N. E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, 7(5), pages 323–334,1992
R. Gerth, D. Peled, M. Vardi and P. Wolper Simple on-the-fly automatic verification of linear temporal logic PSTV, XIII, pages 3–18, 1995
P. Godefroid and G. J. Holzmann On the verification of temporal properties PSTV, XIII, pages 109–124, 1993
J. Goguen and G. Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, 1997.
A. Gravell. Executing Formal Specifications Need Not Be Harmful. Available on the WWW at URL http://dsse.ecs.soton.ac.uk/amg/papers.html.
C.A. Hoare. An Overview of Some Formal Methods for Program Design. IEEE Computer, pages 85–91, 1987.
I. J. Hayes and C. B. Jones Specifications are not (necessarily) executable. Software Engineering Journal,4(6), pages 320–338,1989
F. Kröger Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science 8. Berlin, Springer-Verlag, 1987
L. Lamport. The module structure of TLA+ Research Report 1996-002, Digital Equipment Corporation, Systems Research Center.
L. Lamport. The operators of TLA+ Research Report 1997-006a, Digital Equipment Corporation, Systems Research Center.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
A. C. Leisenring. Mathematical Logic and Hilbert’s ɛ-Symbol. Gordon and Breach, New York, 1969.
Z. Manna and A. Pnueli The Temporal Logic of Reactive and Concurrent Systems-Specifications New-York etc.: Springer-Verlag, 1992
S. Merz. Efficiently Executable Temporal Logic Programs. In Michael Fisher and Richards Owens editors, Executable Modal and Temporal Logics, IJCAI’93 Workshop, volume 897 of Lecture Notes in Computer Science, pages 69–85, France, 1993, Springer.
M.A. Orgun and W.W. Wadge. Towards a unified theory of intensional logic programming. Journal of Logic Programming 13(4), pp. 413ff (1992)
J. Rushby. Formal Methods and their Role in the Certification of Critical Systems. SRI Technical Report CSL-95-1, March 1995.
L. Sterling, P. Ciancarini and T. Turnidge. On the animation of “not executable” specifications by Prolog. International Journal of Software Engineering and Knowledge Engineering, 6(1):63–87.
M. Utting. Animating Z: Interactivity, transparency and equivalence. Technical Report 94-40. Software Verification Research Center.
M. Vardi and P. Wolper An automata-theoretic approach to automatic program verification Proceedings on the First Symposium on Logic in Computer Science, pages 322–331,1986
P. Wolper. Temporal Logic Can Be More Expressive. Information and Control 56. pages 71–99, 1983
P. Zave and R. T. Yeh. Executable requirement specification for embedded system. Proc. 5th Int. Conf. on Software Engineering, San Diego, California, pages 295–304, 1981.
P. Zave An operational approach to requirements specifications. IEEE Trans. SE-8(3), pages 250–269, 1982.
Y. Mokhtari The invoice system problem in TLA+ Proc. International Workshop on Comparing Systems Specification Techniques, University of Nantes, France March 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mokhtari, Y., Merz, S. (1999). Animating TLA Specifications. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 1999. Lecture Notes in Computer Science(), vol 1705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48242-3_7
Download citation
DOI: https://doi.org/10.1007/3-540-48242-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66492-5
Online ISBN: 978-3-540-48242-0
eBook Packages: Springer Book Archive