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 条
  • [21] Combining formal verification and conformance testing for validating reactive systems
    Rusu, V
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2003, 13 (03) : 157 - 180
  • [22] A Formal Data-Centric Approach for Passive Testing of Communication Protocols
    Lalanne, Felipe
    Maag, Stephane
    IEEE-ACM TRANSACTIONS ON NETWORKING, 2013, 21 (03) : 788 - 801
  • [23] Model-driven approach supporting formal verification for web service composition protocols
    Dumez, C.
    Bakhouya, M.
    Gaber, J.
    Wack, M.
    Lorenz, P.
    JOURNAL OF NETWORK AND COMPUTER APPLICATIONS, 2013, 36 (04) : 1102 - 1115
  • [24] A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks
    Chen, Zhe
    Zhang, Daqiang
    Zhu, Rongbo
    Ma, Yinxue
    Yin, Ping
    Xie, Feng
    SENSOR LETTERS, 2013, 11 (05) : 752 - 764
  • [25] Formal modeling and verification of security protocols on cloud computing systems based on UML 2.3
    Fang, Kunding
    Li, Xiaohong
    Hao, Jianye
    Feng, Zhiyong
    2016 IEEE TRUSTCOM/BIGDATASE/ISPA, 2016, : 852 - 859
  • [26] Formal Verification
    Meenakshi, B.
    RESONANCE-JOURNAL OF SCIENCE EDUCATION, 2005, 10 (05): : 26 - 38
  • [27] Formal verification
    B Meenakshi
    Resonance, 2005, 10 (5) : 26 - 38
  • [28] Specifying linked data structures in JML for combining formal verification and testing
    Gladisch, Christoph
    Tyszberowicz, Shmuel
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 107 : 19 - 40
  • [29] A Security Assurance Framework Combining Formal Verification and Security Functional Testing
    Wang, Weiguang
    Zeng, Qingkai
    Mathur, Aditya P.
    2012 12TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2012, : 136 - 139
  • [30] Formal Verification of Grid Frequency Controllers
    Mohapatra, Anurag
    Peric, Vedran S.
    Hamacher, Thomas
    2021 IEEE PES INNOVATIVE SMART GRID TECHNOLOGY EUROPE (ISGT EUROPE 2021), 2021, : 643 - 648