A case-study in component-based mechanical verification of fault-tolerant programs

被引：8
|
作者：
Kulkarni, SS [1 ]
Rushby, J [1 ]
Shankar, N [1 ]
机构：
[1] Ohio State Univ, Dept Comp & Informat Sci, Columbus, OH 43210 USA
来源：
19TH IEEE INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS - WORKSHOP ON SELF-STABILIZING SYSTEMS, PROCEEDINGS | 1999年
关键词：
component-based verification; fault-tolerance; program decomposition; mechanical verification; self-stabilization;
D O I：
10.1109/SLFSTB.1999.777484
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper; we present a case study to demonstrate that the decomposition of a fault-tolerant program into its components is useful in its mechanical verification. More specifically, we discuss our experience in using the theorem prover PVS to verify Dijkstra's token ring program in a component-based manner We also demonstrate the advantages of component based mechanical verification.
引用
收藏
页码：33 / 40
页数：8
相关论文
共 50 条
  • [1] A component-based design and compositional verification of a fault-tolerant multimedia communication protocol
    Hanumantharaya, A
    Sinha, P
    Agarwal, A
    REAL-TIME IMAGING, 2003, 9 (06) : 401 - 422
  • [2] Mechanical verification of automatic synthesis of fault-tolerant programs
    Kulkarni, SS
    Bonakdarpour, B
    Borzoo, S
    LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2005, 3573 : 36 - 52
  • [3] A fault-tolerant software architecture for component-based systems
    Guerra, PAD
    Rubira, CMF
    de Lemos, R
    ARCHITECTING DEPENDABLE SYSTEMS, 2003, 2677 : 129 - 149
  • [4] VERIFICATION OF A FAULT-TOLERANT PROPERTY OF A MULTIPROCESSOR SYSTEM - A CASE-STUDY IN THEOREM PROVER-BASED VERIFICATION
    BICKFORD, M
    SRIVAS, M
    IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 10 : 225 - 251
  • [5] A novel approach for component-based fault-tolerant software development
    Sinha, P
    Hanumantharya, A
    INFORMATION AND SOFTWARE TECHNOLOGY, 2005, 47 (06) : 365 - 382
  • [6] A component-based design of a fault-tolerant multimedia communication protocol
    Hanumantharaya, A
    Sinha, P
    Agarwal, A
    IEEE FIFTH INTERNATIOANL SYMPOSIUM ON MULTIMEDIA SOFTWARE ENGINEERING, PROCEEDINGS, 2003, : 164 - 171
  • [7] Eternal - a component-based framework for transparent fault-tolerant CORBA
    Narasimhan, P
    Moser, LE
    Melliar-Smith, PM
    SOFTWARE-PRACTICE & EXPERIENCE, 2002, 32 (08): : 771 - 788
  • [8] Architecting Fault-tolerant Component-based Systems: from requirements to testing
    Bucchiarone, Antonio
    Muccini, Henry
    Pelliccione, Patrizio
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 168 (SPEC. ISS.) : 77 - 90
  • [9] FAULT-TOLERANT PROGRAMS
    BELLI, F
    JEDRZEJOWICZ, P
    ANGEWANDTE INFORMATIK, 1988, 30 (12): : 533 - 538
  • [10] A Case Study in Parallel Verification of Component-Based Systems
    Benes, N.
    Cerna, I.
    Sochor, J.
    Varekova, P.
    Zimmerova, B.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 220 (02) : 67 - 83
12345