A Perfecto verification: Combining model checking with deductive analysis to verify real-life software

被引:0
|
作者
Kesten, Y [1 ]
Klein, A
Pnueli, A
Raanan, G
机构
[1] Ben Gurion Univ Negev, Dept Commun Syst Engn, IL-84105 Beer Sheva, Israel
[2] Perfecto Technol Ltd, IL-46733 Herzelia, Israel
[3] Weizmann Inst Sci, IL-76100 Rehovot, Israel
来源
FM'99-FORMAL METHODS | 1999年 / 1708卷
关键词
models; verification (deductive methods; assume-guarantee; compositional) model checkers (SPIN; PROMELA); concurrent systems; security; safety properties; telecommunications; object oriented; network protocols;
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
The paper presents an approach to the formal verification of a complete software system intended to support the flagship product of Perfecto Technologies which enforces application security over an open communication net. Based on initial experimentation, it was decided that the verification method will be based on a combination of model-checking using SPIN with deductive verification which handles the more data-intensive elements of the design. The analysis was that only such a combination can cover by formal verification all the important aspects of the complete system. In order to enable model checking of large portions of the design, we have developed an assume-guarantee approach which supports compositional verification. We describe how this general approach was implemented in the SPIN framework. Then, we explain the need to split the verification activity into the model-checking part which deals with the control issues such as concurrency or deadlocking and a deductive part which handles the data-intensive elements of the design.
引用
收藏
页码:173 / 194
页数:22
相关论文
共 50 条
  • [21] Using SPIN model checking for flight software verification
    Glück, PR
    Holzmann, GJ
    2002 IEEE AEROSPACE CONFERENCE PROCEEDINGS, VOLS 1-7, 2002, : 105 - 113
  • [22] Scalable software model checking using design for verification
    Bultan, Tevfik
    Betin-Can, Aysu
    VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 337 - 346
  • [23] Combining Predicate and Numeric Abstraction for Software Model Checking
    Gurfinkel, Arie
    Chaki, Sagar
    2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2008, : 127 - 135
  • [24] SAFEHULL - NEW DESIGN SOFTWARE FROM ABS FOR REAL-LIFE ANALYSIS
    不详
    NAVAL ARCHITECT, 1993, : E513 - E513
  • [25] Combining predicate and numeric abstraction for software model checking
    Gurfinkel A.
    Chaki S.
    International Journal on Software Tools for Technology Transfer, 2010, 12 (06) : 409 - 427
  • [26] A REAL-LIFE COMMUNICATIONS MODEL
    MACLAURIN, S
    TRAINING AND DEVELOPMENT JOURNAL, 1991, 45 (03): : 79 - 80
  • [27] Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
    Cristia, Maximiliano
    Rossi, Gianfranco
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2024,
  • [28] Combining testing and model checking for verification of high assurance systems
    Desovski, D
    EIGHTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, PROCEEDINGS, 2004, : 279 - 280
  • [29] Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties
    Vander Meulen, Jose
    Pecheur, Charles
    NASA FORMAL METHODS, 2011, 6617 : 406 - +
  • [30] Combining real-time model-checking and fault tree analysis
    Schäfer, A
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 522 - 541