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 条

[31] 1.3.4 Model-Based Design and Verification of Fault-Tolerant Systems
EADS Deutschland, Innovation Works, Munich
81663, Germany
不详
85521, Germany
INCOSE Int. Sym., 2007, 1 (81-94):
[32] Structural analysis of explicit fault-tolerant programs
Gossens, S
Dal Cin, M
EIGHTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, PROCEEDINGS, 2004, : 89 - 96
[33] A temporal model for fault-tolerant parallel programs
Slimani, Y
Majdoub, L
PROCEEDINGS OF THE SIXTH IEEE COMPUTER SOCIETY WORKSHOP ON FUTURE TRENDS OF DISTRIBUTED COMPUTING SYSTEMS, 1997, : 304 - 309
[34] A TECHNIQUE FOR ESTIMATING PERFORMANCE OF FAULT-TOLERANT PROGRAMS
SCHLICHTING, RD
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1985, 11 (06) : 555 - 563
[35] Reliability verification of fault-tolerant systems design based on mutation analysis
Vargas, F
Bezerra, E
Terroso, A
Barros, D
XI BRAZILIAN SYMPOSIUM ON INTEGRATED CIRCUIT DESIGN, PROCEEDINGS, 1998, : 55 - 58
[36] Component Ranking for Fault-Tolerant Cloud Applications
Zheng, Zibin
Zhou, Tom Chao
Lyu, Michael R.
King, Irwin
IEEE TRANSACTIONS ON SERVICES COMPUTING, 2012, 5 (04) : 540 - 550
[37] Synthesizing Round Based Fault-Tolerant Programs Using Genetic Programming
Zhu, Ling
Kulkarni, Sandeep
STABILIZATION, SAFETY, AND SECURITY OF DISTRIBUTED SYSTEMS, SSS 2013, 2013, 8255 : 370 - 372
[38] FORMAL SPECIFICATION AND MECHANICAL VERIFICATION OF SIFT - A FAULT-TOLERANT FLIGHT CONTROL-SYSTEM
MELLIARSMITH, PM
SCHWARTZ, RL
IEEE TRANSACTIONS ON COMPUTERS, 1982, 31 (07) : 616 - 630
[39] FOCUS - AN EXPERIMENTAL ENVIRONMENT FOR VALIDATION OF FAULT-TOLERANT SYSTEMS CASE-STUDY OF A JET-ENGINE CONTROLLER
CHOI, G
IYER, R
CARRENO, V
PROCEEDINGS - IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS, 1989, : 561 - 564
[40] Study of Fault-tolerant Control Strategies for a Fault-tolerant Permanent Magnet Motor
Bai Hongfen
Zhu Jingwei
Qin Junfeng
PROCEEDINGS OF THE 35TH CHINESE CONTROL CONFERENCE 2016, 2016, : 6455 - 6460

← 1 2 3 4 5 →