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 条
  • [31] Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
    Nanevski, Aleksandar
    Banerjee, Anindya
    Delbianco, German Andres
    Fabregas, Ignacio
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (OOPSLA):
  • [32] Specifying Concurrent Problems: Beyond Linearizability and up to Tasks
    Castaneda, Armando
    Rajsbaum, Sergio
    Raynal, Michel
    DISTRIBUTED COMPUTING (DISC 2015), 2015, 9363 : 420 - 435
  • [33] Specifying a knowledge management system for the Concurrent Engineering Laboratory (NuPES)
    Sato, GY
    de Azevedo, HS
    ADVANCES IN CONCURRENT ENGINEERING: CE99, 1999, 99 : 322 - 326
  • [34] Modeling and Analysis of Workflow Based on TLA
    Chen Shu
    Wu Guo Qing
    JOURNAL OF COMPUTERS, 2009, 4 (01) : 27 - 34
  • [35] ParBlocks - A new methodology for specifying concurrent method executions in Opus
    Laure, E
    EURO-PAR'99: PARALLEL PROCESSING, 1999, 1685 : 925 - 929
  • [36] Survey on Interactive Theorem Proving Based Concurrent Program Verification
    Wang Z.-Y.
    Wu S.-S.
    Cao Q.-X.
    Ruan Jian Xue Bao/Journal of Software, 2024, 35 (09):
  • [37] A Lightweight Program Dependence based Approach to Concurrent Mutation Analysis
    Sun, Chang-ai
    Jia, Jingting
    Liu, Huai
    Zhang, Xiangyu
    2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, : 116 - 125
  • [38] Formal Semantics of Orc Based on TLA+
    You, Zhen
    Xue, Jinyun
    Hu, Qimin
    Hong, Yi
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, 2015, 8979 : 147 - 163
  • [39] Specifying multithreaded Java']Java semantics for program verification
    Roychoudhury, A
    Mitra, T
    ICSE 2002: PROCEEDINGS OF THE 24TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2002, : 489 - 499
  • [40] A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations
    Liang, Hongjin
    Feng, Xinyu
    Fu, Ming
    ACM SIGPLAN NOTICES, 2012, 47 (01) : 455 - 468
12345