Specifying Concurrent Program based on TLA

被引：0

作者：

Chen Rui ^{[1
]}

Long Shigong ^{[2
]}

机构：

[1] Guizhou Univ, Sci Coll, Guiyang 550025, Peoples R China

[2] Guiyang Univ, Coll Comp Sci & Informat, Guiyang 550025, Peoples R China

来源：

MECHANICAL DESIGN AND POWER ENGINEERING, PTS 1 AND 2 | 2014年 / 490-491卷

关键词：

Concurrent; Liveness; Safety; TLA; TEMPORAL LOGIC;

D O I：

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

中图分类号：

TH [机械、仪表工业];

学科分类号：

0802 ;

摘要：

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 Needham-Schroeder symmetric key protocol as an example to illustrate how to specify these properties in concurrent program by TLA.

引用

页码：798 / +

页数：2

共 50 条

[1] Specifying concurrent systems with TLA+
Lamport, L
CALCULATIONAL SYSTEM DESIGN, 1999, 173 : 183 - 247
[2] Specifying and Verifying Concurrent C Programs with TLA
Methni, Amira
Lemerre, Matthieu
Ben Hedia, Belgacem
Haddad, Serge
Barkaoui, Kamel
FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2014, 2015, 476 : 206 - 222
[3] SPECIFYING CONCURRENT PROGRAM MODULES
LAMPORT, L
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1983, 5 (02): : 190 - 222
[4] Specifying and Checking Network Protocol Based on TLA
Wan, Liang
Shi, Wenchang
2012 INTERNATIONAL CONFERENCE ON ANTI-COUNTERFEITING, SECURITY AND IDENTIFICATION (ASID), 2012,
[5] Specifying reversibility with TLA+
Kapus, Tatjana
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2020, 116
[6] Some Challenges of Specifying Concurrent Program Components
Hayes, Ian J.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (282): : 10 - 22
[7] Specifying Transaction Control to Serialize Concurrent Program Executions
Boerger, Egon
Schewe, Klaus-Dieter
ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z, ABZ 2014, 2014, 8477 : 142 - 157
[8] Specifying and verifying PLC systems with TLA+
Zhang, Hehua
Merz, Stephan
Gu, Ming
THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 293 - +
[9] Specifying and Verifying CRDT Protocols Using TLA+
Ji Y.
Wei H.-F.
Huang Y.
Lü J.
Ruan Jian Xue Bao/Journal of Software, 2020, 31 (05): : 1332 - 1352
[10] SPECIFYING CONCURRENT OBJECTS
KRAMER, B
SIGPLAN NOTICES, 1989, 24 (04): : 162 - 164

← 1 2 3 4 5 →