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] Petri-nets for formal verification of MAC protocols
    Haines, R. J.
    Clemo, G. R.
    Munro, A. T. D.
    IET SOFTWARE, 2007, 1 (02) : 39 - 47
  • [42] Formal Verification of Security Protocols: the Squirrel Prover (Keynote)
    Delaune, Stephanie
    FOUNDATIONS AND PRACTICE OF SECURITY, PT II, FPS 2023, 2024, 14552 : XI - XIV
  • [43] Formal Verification of Security Protocols: the Squirrel Prover (Keynote)
    Delaune, Stephanie
    FOUNDATIONS AND PRACTICE OF SECURITY, PT I, FPS 2023, 2024, 14551 : XI - XIV
  • [44] Formal verification of activity-based specification of protocols
    Anand, KC
    Shyamasundar, RK
    JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2000, 60 (05) : 639 - 676
  • [45] SoK: Directions and Issues in Formal Verification of Payment Protocols
    Sakurada, Hideki
    Sakurai, Kouichi
    ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 4, AINA 2024, 2024, 202 : 111 - 119
  • [46] Formal verification of standards for distance vector routing protocols
    Bhargavan, K
    Obradovic, D
    Gunter, CA
    JOURNAL OF THE ACM, 2002, 49 (04) : 538 - 576
  • [47] Formal Verification of Distributed Branching Multiway Synchronization Protocols
    Evrard, Hugues
    Lang, Frederic
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, FMOODS/FORTE 2013, 2013, 7892 : 146 - 160
  • [48] Development and testing of formal protocols for oxygen prescribing
    Guyatt, GH
    McKim, DA
    Weaver, B
    Austin, PA
    Bryan, REJ
    Walter, SD
    Nonoyama, ML
    Ferreira, IM
    Goldstein, RS
    AMERICAN JOURNAL OF RESPIRATORY AND CRITICAL CARE MEDICINE, 2001, 163 (04) : 942 - 946
  • [49] Formal Analysis and Verification of Packet Recovery Protocols for Multicast Video
    Atif, Muhammad
    Mushtaq, Nadia
    Mahmood, Sohaib
    Naeem, Muhammad
    Riaz, Amjad
    INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2018, 18 (03): : 110 - 118
  • [50] FORMAL DESCRIPTION AND VERIFICATION OF CCS-BASED PROTOCOLS.
    Karpov, Yu.G.
    Automatic Control and Computer Sciences, 1986, 20 (06) : 16 - 25