Abstract
In this paper, we explain how we use abstract interpretation for analysing temporal specifications in TLA+. An analysis is obtained by building a predicate behavior which satisfies the specification. Abstract interpretation allows us to transit from a concrete world to an abstract world (generally finite). Using abstract interpretation, we build abstract predicate behaviors and, in general, if the abstract interpretation is sufficiently powerful and expressive, we can build a finite graph of abstract predicates to analyse a temporal specification. TLA/TLA+ is based on an untyped framework, namely the ZF set theory and we show how abstract interpretation fits the requirements of untyping and makes the analysis of temporal specifications easier.
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
J.-R. Abrial. The B book–Assigning Programs to Meanings. Cambridge University Press, 1996.
D. Cansell, J.-P. Gibson, B. Mermet, and D. Méry. Spécification de services dans une logique temporelle compositionnelle. Rapport final du marché n°96 1B CNET-CNRS-CRIN, LORIA UMR 7503 Laboratoire Lorrain de Recherche en Informatique et Applications, février 1999.
D. Cansell and D. Méry. Interprétation de spécifications temporelles à l’aide d’un outil de preuve. In AFADL: Approches formelles dans l’assistance au développement de logiciels, sept, nov 1998.
P. Cousot. Calculational System Design, chapter The Calculational Design of a Generic Abstract Interpreter. NATO ASI Series F. Amsterdam: IOS Press, 1999.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Fourth Conference on Principles of Programming Languages POPL, pages 238–252, Los Angeles, California, 1977. ACM Press.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Sixth Conference on Principles of Programming Languages POPL, pages 269–282, San Antonio, Texas, 1979. ACM Press.
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.
J.-P. Gibson, B. Mermet, and D. Méry. Feature interactions: A mixed semantic model approach. In Gerard O’Regan and Sharon Flynn, editors, 1st Irish Workshop on Formal Methods, Dublin, Ireland, July 1997. Irish Formal Methods Special Interest Group (IFMSIG), Springer Verlag. http://ewic.springer.co.uk/.
J.-P. Gibson and D. Méry. Always and Eventually in Object Requirements. In Rigorous Object Oriented Methods ROOM2 (Bradford), 1998.
J.-P. Gibson and D. Méry. COTSR Proceedings, chapter Fair Objects, page ?? Computer Science and Electronic Engineering. Horwood Publishing Ltd, October 1998.
J.-P. Gibson and D. Méry. Fair objects. In H. Zedan, editor, OT’98 1st UK Colloquium on Object Technology & System Re-engineering (COTSR), 6’8 April 1998.
P. Granger. Static analysis of arithmetical congruences. IJCM, 30:165–190, 1989.
P. Granger. Static analysis of linear congruence equalities among variables of a program. In S. Abramsky and T.S.E. Maibaum, editors, Proc TAPSOFT’91, Volume 1 (CAAP’91), Brighton, UK, LNCS 493, pages 169–192. Springer-Verlag, 1991.
P. Lacan, J.N. Monfort, Le Vinh Quy Ribal, A. Deutsch, and G. Gonthier. The software reliability verification process: The Ariane 5 example. In Proceedings DASIA 98–DAta Systems IN Aerospace, Athens, Greece. ESA Publications, SP-422, May 25–28 1998.
L. Lamport. How to write a long formula. Technical report, COMPAQ Palo Alto, http://www.research.digital.com/SRC/tla/, december 1993.
L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.
L. Lamport. The TLA/TLA + WEB page. COMPAQ Palo Alto, http://www.research.digital.com/SRC/tla/, 1999.
L. Lamport and L. C. Paulson. Should your specification language be typed? Technical report SRC Research Report 147, SRC, 1998.
K. L. McMillan. Symbolic Model Checkin. Kluwer Academic Publishers, 1993.
D. Méry and A. Mokkedem. Crocos: An integrated environment for interactive verification of sdl specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings, Lecture Notes in Computer Science. Springer Verlag, 1992.
Stephan Merz. Rules for abstraction. In R. K. Shyamasundar and K. Ueda, editors, Advances in Computing Science—ASIAN’97, volume 1345 of Lecture Notes in Computer Science, pages 32–45, Kathmandu, Nepal, dec 1997. Springer-Verlag.
Steria Méditerrannée. Atelier B, Version 3.2, Manuel de Référence du Langage B. GEC Alsthom Transport and Steria Méditerrannée and SNCF and INRETS and RATP, 1997.
Union Internationale des Télécommunications. Introduction à l’ensemble de capacités 1 du réseau intelligent. Technical Report UIT-T Q.1211, Union Internationale des Télécommunications, march 1993. Réseau Intelligent.
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
Cansell, D., Méry, D. (1999). Abstract Animator for Temporal Specifications: Application to TLA. In: Cortesi, A., Filé, G. (eds) Static Analysis. SAS 1999. Lecture Notes in Computer Science, vol 1694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48294-6_18
Download citation
DOI: https://doi.org/10.1007/3-540-48294-6_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66459-8
Online ISBN: 978-3-540-48294-9
eBook Packages: Springer Book Archive