Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic

被引：0
|
作者：
Sinclair, David [1 ]
Power, James [2 ]
机构：
[1] Dublin City Univ, Sch Comp, Dublin 9, Ireland
[2] Natl Univ Ireland, Dept Comp Sci, Maynooth, Kildare, Ireland
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 133卷
关键词：
complex systems; formal methods; mixed intuitionistic linear logic;
D O I：
10.1016/j.entcs.2004.08.068
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we present a technique for specifying and verifying communications protocols and demonstrate this approach by specifying and verifying two of the fundamental communications protocols, namely TCP and IP, which form the basis of many distributed systems. The logical formalism used is Mixed Intuitionistic Linear Logic in order to use both commutative and non-commutative operators to model the concurrent and sequential processes in these protocols. Key properties of both protocols are proved.
引用
收藏
页码：255 / 273
页数：19
相关论文
共 50 条
  • [1] Specifying and Verifying CRDT Protocols Using TLA+
    Ji, Ye
    Wei, Heng-Feng
    Huang, Yu
    Lü, Jian
    [J]. Ruan Jian Xue Bao/Journal of Software, 2020, 31 (05): : 1332 - 1352
  • [2] The use of conditional grammars for specifying and verifying communication protocols
    Matousek, P
    [J]. MODELLING AND SIMULATION 2001, 2001, : 59 - 62
  • [3] CellScope: Automatically Specifying and Verifying Cellular Network Protocols
    Yu, Yinbo
    Li, You
    Hou, Kaiyu
    Chen, Yan
    Zhou, Hai
    Yang, Jianfeng
    [J]. PROCEEDINGS OF THE 2019 ACM SIGCOMM CONFERENCE POSTERS AND DEMOS (SIGCOMM '19), 2019, : 21 - 23
  • [4] Linear logic and intuitionistic logic
    Okada, M
    [J]. REVUE INTERNATIONALE DE PHILOSOPHIE, 2004, 58 (230) : 449 - 481
  • [5] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
    Yang, SJH
    Chu, W
    Lin, S
    Lee, J
    [J]. THIRD IEEE INTERNATIONAL HIGH-ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 1998, : 150 - 156
  • [6] ON SPECIFYING PROTOCOLS BASED ON LOTOS AND TEMPORAL LOGIC
    ANDO, T
    KATO, Y
    TAKAHASHI, K
    [J]. IEICE TRANSACTIONS ON COMMUNICATIONS, 1994, E77B (08) : 992 - 1006
  • [7] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
    Yang, SJH
    Chu, W
    Lee, J
    [J]. INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1999, 9 (02) : 233 - 249
  • [8] A Program Logic for Verifying Secure Routing Protocols
    Chen, Chen
    Jia, Limin
    Xu, Hao
    Luo, Cheng
    Zhou, Wenchao
    Loo, Boon Thau
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, 2014, 8461 : 117 - 132
  • [9] A PROGRAM LOGIC FOR VERIFYING SECURE ROUTING PROTOCOLS
    Chen, Chen
    Jia, Limin
    Xu, Hao
    Luo, Cheng
    Zhou, Wenchao
    Loo, Boon Thau
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (04)
  • [10] Specifying and verifying systems of communicating agents in a temporal action logic
    Giordano, L
    Martelli, A
    Schwind, C
    [J]. AI(ASTERISK)IA 2003: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2003, 2829 : 262 - 274
12345