Formal verification and testing of protocols

被引：5
|
作者：
Avresky, DR [1 ]
机构：
[1] Boston Univ, Dept Elect Engn, Brookline, MA 02146 USA
来源：
COMPUTER COMMUNICATIONS | 1999年 / 22卷 / 07期
关键词：
protocols; reachability analysis; execution tree; formal verification;
D O I：
10.1016/S0140-3664(99)00011-0
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We adopt a formalism to describe protocols that is close to the human way of thinking and can be easily used to perform reachability analysis of the described protocol in a state-transition format. This formalism allows for an execution tree (ET) to be generated from a set of assertions such that all paths from the root to the leaves are well-defined formulas. We then extend the formalism with regards to real-time properties. Finally, we present a software verification tool, that implements the aforementioned features in the analysis of protocols. (C) 1999 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：681 / 690
页数：10
相关论文
共 50 条
  • [31] Web GUI for Automating the Formal Verification of Security Protocols using Casper & FDR4
    Scurtu, Andreea
    Pura, Mihai-Lica
    PROCEEDINGS OF THE 11TH INTERNATIONAL CONFERENCE ON ELECTRONICS, COMPUTERS AND ARTIFICIAL INTELLIGENCE (ECAI-2019), 2019,
  • [32] A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving
    Pourpouneh, Mohsen
    Ramezanian, Rasoul
    ISECURE-ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2016, 8 (01): : 3 - 24
  • [33] Verifying and Improving Neural Networks Using Testing-Based Formal Verification
    Liu, Haiyi
    Liu, Shaoying
    Liu, Ai
    Fang, Dingbang
    Xu, Guangquan
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2022, 2023, 13854 : 126 - 141
  • [34] Formal Verification of a Keystore
    Boender, Jaap
    Badevic, Goran
    THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 49 - 64
  • [35] Formal Verification of Websites
    Flores, Sonia
    Lucas, Salvador
    Villanueva, Alicia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) : 103 - 118
  • [36] Formal verification of μ-charts
    Goldson, D
    APSEC 2002: NINTH ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, 2002, : 129 - 136
  • [37] Toward Formal Verification of 802.11 MAC Protocols: Verifying a Petri-net Model of 802.11 PCF
    Haines, Russell
    Clemo, Gary
    Munro, Alistair
    2006 IEEE 64TH VEHICULAR TECHNOLOGY CONFERENCE, VOLS 1-6, 2006, : 2236 - +
  • [38] Toward Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal Cross- and Self-Attention Large Language Model Approach
    Yang, Jingda
    Wang, Ying
    IEEE ACCESS, 2024, 12 : 27858 - 27869
  • [39] Assessing business process models: a literature review on techniques for BPMN testing and formal verification
    Lopes, Tomas
    Guerreiro, Sergio
    BUSINESS PROCESS MANAGEMENT JOURNAL, 2023, 29 (08) : 133 - 162
  • [40] Enhancing the Capability of Testing-Based Formal Verification by Handling Operations in Software Packages
    Liu, Ai
    Liu, Shaoying
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2023, 49 (01) : 304 - 324
12345