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 条
  • [41] An Approach to Slicing Concurrent Ada Programs Based on Program Reachability Graphs
    Qi, Xiaofang
    Xu, Baowen
    INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2006, 6 (1A): : 29 - 37
  • [42] A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations
    Liang, Hongjin
    Feng, Xinyu
    Fu, Ming
    POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 455 - 468
  • [43] Concurrent Program Semantic Mutation Testing Based on Abstract Memory Model
    Cao, Lixin
    Zheng, Wei
    Hu, Desheng
    Bai, Han
    2015 IEEE INTERNATIONAL CONFERENCE ON INFORMATION AND AUTOMATION, 2015, : 1200 - 1205
  • [44] CONCURRENT PROGRAM SCHEMES AND THEIR LOGICS
    PELEG, D
    THEORETICAL COMPUTER SCIENCE, 1987, 55 (01) : 1 - 45
  • [45] NOTE ON THE PROOF OF A CONCURRENT PROGRAM
    BEST, E
    INFORMATION PROCESSING LETTERS, 1979, 9 (03) : 103 - 104
  • [46] MONEY AS A CONCURRENT LOGIC PROGRAM
    KAHN, KM
    KORNFELD, WA
    LOGIC PROGRAMMING : PROCEEDINGS OF THE NORTH AMERICAN CONFERENCE, 1989, VOL 1-2, 1989, : 513 - 535
  • [47] Visualization of concurrent program executions
    Artho, Cyrille
    Havelund, Klaus
    Honiden, Shinichi
    COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL II, PROCEEDINGS, 2007, : 541 - +
  • [48] Visualization of concurrent program executions
    Artho, Cyrille
    Havelund, Klaus
    Honiden, Shinichi
    NII Technical Reports, 2007, 2007 (06): : 1 - 12
  • [49] TEMPORAL PREDICATE TRANSITION NETS - A NEW FORMALISM FOR SPECIFYING AND VERIFYING CONCURRENT SYSTEMS
    HE, XD
    INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 1992, 45 (3-4) : 171 - 184
  • [50] A Mechanism of Modeling and Verification for SaaS Customization Based on TLA
    Luan, Shuai
    Shi, Yuliang
    Wang, Haiyang
    WEB INFORMATION SYSTEMS AND MINING, PROCEEDINGS, 2009, 5854 : 337 - 344
12345