Formal verification and testing of protocols

被引:5
|
作者
Avresky, DR [1 ]
机构
[1] Boston Univ, Dept Elect Engn, Brookline, MA 02146 USA
关键词
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 条
  • [41] NNTBFV: Simplifying and Verifying Neural Networks Using Testing-Based Formal Verification
    Liu, Haiyi
    Liu, Shaoying
    Xu, Guangquan
    Liu, Ai
    Fang, Dingbang
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2024, 34 (02) : 273 - 300
  • [42] Achieving Energy Efficiency through Load Balancing: A Comparison through Formal Verification of two WSN Routing Protocols
    Khan, Naveed Ahmed
    Saghar, Kashif
    Ahmad, Rizwan
    Kiani, Adnan K.
    2016 13TH INTERNATIONAL BHURBAN CONFERENCE ON APPLIED SCIENCES AND TECHNOLOGY (IBCAST), 2016, : 350 - 354
  • [43] Formal verification of secure ad-hoc network routing protocols using deductive model-checking
    Buttyán L.
    Thong T.V.
    Periodica Polytechnica Electrical Engineering, 2011, 55 (1-2): : 31 - 43
  • [44] Card-Based Cryptography Meets Formal Verification
    Koch, Alexander
    Schrempp, Michael
    Kirsten, Michael
    ADVANCES IN CRYPTOLOGY - ASIACRYPT 2019, PT I, 2019, 11921 : 488 - 517
  • [45] Formal verification and quantitative metrics of MPSoC data dynamics
    Zhang, Hui
    Wu, Jinzhao
    FORMAL ASPECTS OF COMPUTING, 2018, 30 (02) : 219 - 237
  • [46] Formal Verification of a MAC Protocol for Underwater Sensor Networks
    Kumar, N. Suresh
    Kumar, G. Santhosh
    Sivan, Shailesh
    Sreekumar, A.
    IEEE ACCESS, 2023, 11 : 111846 - 111859
  • [47] Card-Based Cryptography Meets Formal Verification
    Koch, Alexander
    Schrempp, Michael
    Kirsten, Michael
    NEW GENERATION COMPUTING, 2021, 39 (01) : 115 - 158
  • [48] Formal-Based Design and Verification of SoC Arbitration Protocols: A Comparative Analysis of TDMA and Round-Robin
    Ben Slimane, Maroua
    Ben Hafaiedh, Imene
    Robbana, Riadh
    IEEE DESIGN & TEST, 2017, 34 (05) : 54 - 62
  • [49] Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID
    Xiao, Meihua
    Li, Wei
    Zhong, Xiaomei
    Yang, Ke
    Chen, Jia
    CHINESE JOURNAL OF ELECTRONICS, 2019, 28 (05) : 1025 - 1032
  • [50] The MODUS Approach to Formal Verification
    Brewka, Lukasz
    Soler, Jose
    Berger, Michael
    BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01): : 21 - 33