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
[J]. REAL-TIME IMAGING, 2003, 9 (06) : 401 - 422
[2] Mechanical verification of automatic synthesis of fault-tolerant programs
Kulkarni, SS
Bonakdarpour, B
Borzoo, S
[J]. 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
[J]. 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
[J]. 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
[J]. 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
[J]. 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
[J]. 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
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 168 (SPEC. ISS.) : 77 - 90
[9] FAULT-TOLERANT PROGRAMS
BELLI, F
JEDRZEJOWICZ, P
[J]. 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.
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 220 (02) : 67 - 83

← 1 2 3 4 5 →