Article

Free access

Open systems in TLA

Authors:

Martín Abadi,

Leslie LamportAuthors Info & Claims

PODC '94: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing

Pages 81 - 90

https://doi.org/10.1145/197917.197960

Published: 14 August 1994 Publication History

PDF eReader

References

[1]

Martfn Abadi and Leslie Lamport. Decomposing specifications of concurrent systems. To appear in PROCOMET '94, Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi.

Digital Library

Google Scholar

[2]

Martfn Abadi and Leslie Lamport. An oldfashioned recipe for real time. Research Report 91, Digital Equipment Corporation, Systems Research Center, 1992. An earlier version, without proofs, appeared in {8, pages 1-27}.

Digital Library

Google Scholar

[3]

Martfn Abadi and Leslie Lamport. Composing specifications. A CM Transactions on Programming Languages and Systems, 15(1):73-132, January 1993.

Digital Library

Google Scholar

[4]

Martfn Abadi and Leslie Lamport. Conjoining specifications. Research Report 118, Digital Equipment Corporation, Systems Research Center, 1993.

Google Scholar

[5]

Martfn Abadi and Gordon Plotkin. A logical view of composition and refinement. Theoretical Computer Science, 114(1):3-30, June 1993.

Digital Library

Google Scholar

[6]

Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181-185, October 1985.

Crossref

Google Scholar

[7]

Pierre CoIlette. Application of the composition principle to Unity-like specifications. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT'93: Theory and Practice of Software Development, volume 668 of Lecture Notes in Computer Science, pages 230-242, Berlin, 1993. Springer-Verlag.

Crossref

Google Scholar

[8]

J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. Real- Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992. Proceedings of a REX Real-Time Workshop, held in The Netherlands in June, 1991.

Google Scholar

[9]

Cliff B. Jones. Specification and design of (parallel) programs. In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 321-332. IFIP, North-Holland, September 1983.

Google Scholar

[10]

Leslie Lamport. The temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991. To appear in Transactions on Programming Languages and Systems.

Digital Library

Google Scholar

[11]

Carver Mead and Lynn Conway. Introduction to VLSI Systems, chapter 7. Addison-Wesley, Reading, Massachusetts, 1980.

Digital Library

Google Scholar

[12]

Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417-426, July 1981.

Digital Library

Google Scholar

[13]

Paritosh K. Pandya and Mathai Joseph. P~A logic--a compositional proof system for distributed programs. Distributed Computing, 5(1):37-54, 1991.

Digital Library

Google Scholar

[14]

Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series, pages 123-144. Springer-Verlag, October 1984.

Digital Library

Google Scholar

[15]

Eugene W. Stark. A proof technique for rely/guarantee properties, in S. N. Maheshwari, editor, Foundations of Software Technology and Theoretical Computer Science~ volume 206 of Lecture Notes in Computer Science, pages 369- 391, Berlin, 1985. Springer-Verlag.

Crossref

Google Scholar

Cited By

View all

(2019)ReferencesConcurrency10.1145/3335772.3335940(319-333)Online publication date: 4-Oct-2019
https://dl.acm.org/doi/10.1145/3335772.3335940
Fekete A(2019)Liveness conditions in model-based service specificationsACM SIGSOFT Software Engineering Notes10.1145/222132.22214020:4(62-71)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/222132.222140
Ogata K(2019)A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptionsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-017-7036-213:1(51-72)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s11704-017-7036-2
Show More Cited By

Index Terms

Open systems in TLA

Recommendations

Distributed algorithms in TLA (abstract)
PODC '00: Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing
TLA (the temporal logic of actions) is a simple logic for describing and reasoning about concurrent systems. It provides a uniform way of specifying algorithms and their correctness properties, as well as rules for proving that one specification ...
TLA in Pictures

Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specification and those ...
Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification
ITNG '08: Proceedings of the Fifth International Conference on Information Technology: New Generations

This paper contributes towards a multi-paradigm approach for the specification validation verification and refinement of concurrent agile systems. It brings together two complementary rigorous and largely accepted frameworks: Meseguer’s true-concurrent ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PODC '94: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing

August 1994

406 pages

ISBN:0897916549

DOI:10.1145/197917

Chairmen:
James Anderson
Univ. of North Carolina at Chapel Hill
,
David Peleg
Weizmann Institute & IBM T.J. Watson
,
Elizabeth Borowsky
Univ. of California at Los Angeles

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 August 1994

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PODC94

Sponsor:

PODC94: 13th Annual ACM Symposium on Principles of Distributed Computing

August 14 - 17, 1994

California, Los Angeles, USA

Acceptance Rates

PODC '94 Paper Acceptance Rate 67 of 133 submissions, 50%;

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
345
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)8

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

(2019)ReferencesConcurrency10.1145/3335772.3335940(319-333)Online publication date: 4-Oct-2019
https://dl.acm.org/doi/10.1145/3335772.3335940
Fekete A(2019)Liveness conditions in model-based service specificationsACM SIGSOFT Software Engineering Notes10.1145/222132.22214020:4(62-71)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/222132.222140
Ogata K(2019)A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptionsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-017-7036-213:1(51-72)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s11704-017-7036-2
Filippidis IMurray RHolzmann G(2016)A multi-paradigm language for reactive synthesisElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.202.6202(73-97)Online publication date: 2-Feb-2016
https://doi.org/10.4204/EPTCS.202.6
Filippidis IDathathri SLivingston SOzay NMurray R(2016)Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox2016 IEEE Conference on Control Applications (CCA)10.1109/CCA.2016.7587949(1030-1041)Online publication date: Sep-2016
https://doi.org/10.1109/CCA.2016.7587949
Hanssen ØCerqueira RWang N(2005)Towards declarative characterisation and negotiation of bindingsProceedings of the 4th workshop on Reflective and adaptive middleware systems10.1145/1101516.1101524Online publication date: 28-Nov-2005
https://dl.acm.org/doi/10.1145/1101516.1101524
Jonsson BTsay Y(2005)Assumption/guarantee specifications in linear-time temporal logic (extended abstract)TAPSOFT '95: Theory and Practice of Software Development10.1007/3-540-59293-8_200(262-276)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-59293-8_200
Kurshan RLamport L(2005)Verification of a multiplier: 64 bits and beyondComputer Aided Verification10.1007/3-540-56922-7_14(166-179)Online publication date: 27-May-2005
https://doi.org/10.1007/3-540-56922-7_14
Lim A(1997)Advanced techniques for maintaining reliability of complex computer systemsProceedings of the Thirtieth Hawaii International Conference on System Sciences10.1109/HICSS.1997.663154(4-13)Online publication date: 1997
https://doi.org/10.1109/HICSS.1997.663154
Lim A(1996)Abstraction and composition techniques for reconfiguration of large-scale complex applicationsProceedings of International Conference on Configurable Distributed Systems10.1109/CDS.1996.509361(186-193)Online publication date: 1996
https://doi.org/10.1109/CDS.1996.509361
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Distributed algorithms in TLA (abstract)

TLA in Pictures

Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification