Specifying Concurrent Program Based on TLA

Rui Chen; Shi Gong Long

doi:10.4028/www.scientific.net/AMM.490-491.798

Paper Titles

The Technology of Flexible Blank Holder Forming and the Study of its Numerical Simulation
p.776

Asynchronous Multi-Sensor Fusion Algorithm Based on the Steady-State Kalman Filter
p.781

Numerical Simulation on Effect of Pressure-Released Hole Combined Support with Rockbolt by Dynamic Loading
p.789

Synthesized ADRC for One-Level Inverted Pendulum System through Combination of Separating and Assembling
p.794

Specifying Concurrent Program Based on TLA
p.798

A High-Gain Observer-Based Pd Controller Design for Dynamic Positioning of Ships
p.803

Design of Mobile Interactive Learning Community Based on Electronic Cognitive Apprenticeship Mechanism
p.809

Study of Curve Planning Algorithm for Partition-Type Rotary Burrs
p.814

Partition Scheduling Research of Hard Real-Time and Multi-Core System
p.824

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 490-491Specifying Concurrent Program Based on TLA

Specifying Concurrent Program Based on TLA

Abstract:

. The Temporal logic of actions TLA is a logic for specifying and reasoning about concurrent systems, which make systems and their properties are expressed in the same logic. In this paper, we introduce the concurrent programming languages and behavior semantics, mainly describe safety properties and liveness properties in TLA and take NeedhamSchroeder symmetric key protocol as an example to illustrate how to specify these properties in concurrent program by TLA.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 490-491)

Pages:

798-802

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.490-491.798

Citation:

Cite this paper

Online since:

January 2014

Authors:

Rui Chen, Shi Gong Long

Keywords:

Concurrent, Liveness, Safety, TLA

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] Leslie LAMPORT. The Temporal Logic of Actions [M]. ACM Transactions on Programming Languages and Systems. 1994. 5, 16(3): 872-923.

DOI: 10.1145/177492.177726

Google Scholar

[2] Abadi M, Blanchet B. Analyzing Security Protocols with Secrecy Types and Logic Programs [C] Portland, Oregon, 2002.

DOI: 10.1145/565816.503277

Google Scholar

[3] LAMPORT. Specifying concurrent program modules [M]. ACM Transactions on Programming Languages and Systems 5, 2 (April), 190-222, (1983).

DOI: 10.1145/69624.357207

Google Scholar

[4] BALSER, BAUMLER, REIF. Interactive Verification of Concurrent Systems using Symbolic Execution [J]. In Proceedings of 7th International Workshop of Implementation of Logics (IWIL 08), (2008).

Google Scholar

[5] Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions [J]. In: Foundations of Software Engineering, ACM (2009).

DOI: 10.1145/1595696.1595702

Google Scholar

[6] CALCAGNO, PARKINSON and VAFEIADIS. Modular safety checking for fine-grained concurrency [J]. In SAS, pages 233–248, (2007).

DOI: 10.1007/978-3-540-74061-2_15

Google Scholar

[7] Estrin A, Kaminski M. The expressive power of temporal logic of actions [M]. In Proceedings of the Tenth International Conference on Concurrency Theory, pages274–287, (1999).

Google Scholar

[8] KATOEN. Principles of Model Checking [M]. University of Twente, Lecture Notes, (2004).

Google Scholar