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 条
  • [41] Designing Fault-Tolerant Component Based Applications with a Model Driven Approach
    Hamid, Brahim
    Radermacher, Ansgar
    Lanusse, Agnes
    Jouvray, Christophe
    Gerard, Sebastien
    Terrier, Francois
    SOFTWARE TECHNOLOGIES FOR EMBEDDED AND UBIQUITOUS SYSTEMS, PROCEEDINGS, 2008, 5287 : 9 - 20
  • [42] SPECIFICATION OF FAULT-TOLERANT SYSTEM ISSUES BY PREDICATE TRANSITION NETS AND REGULAR EXPRESSIONS - APPROACH AND CASE-STUDY
    BELLI, F
    GROSSPIETSCH, KE
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1991, 17 (06) : 513 - 526
  • [43] Lazy verification in fault-tolerant distributed storage systems
    Abd-El-Malek, M
    Ganger, GR
    Goodson, GR
    Reiter, MK
    Wylie, JJ
    24TH IEEE SYMPOSIUM ON RELIABLE DISTRIBUTED SYSTEMS, PROCEEDINGS, 2005, : 179 - 190
  • [44] Nonadaptive fault-tolerant verification of quantum supremacy with noise
    Kapourniotis, Theodoros
    Datta, Animesh
    QUANTUM, 2019, 3
  • [45] An Efficient Data Integrity Verification and Fault-tolerant Scheme
    Gan, Hui
    Chen, Long
    2014 FOURTH INTERNATIONAL CONFERENCE ON COMMUNICATION SYSTEMS AND NETWORK TECHNOLOGIES (CSNT), 2014, : 1157 - 1160
  • [46] Analysis and Experimental Verification of a Fault-Tolerant HEV Powertrain
    Song, Yantao
    Wang, Bingsen
    IEEE TRANSACTIONS ON POWER ELECTRONICS, 2013, 28 (12) : 5854 - 5864
  • [47] Component-based face detection and verification
    Lee, Kyoung-Mi
    PATTERN RECOGNITION LETTERS, 2008, 29 (03) : 200 - 214
  • [48] Component-based verification in a synchronous setting
    Merceron, A
    Pinna, GM
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2001, 11 (02) : 181 - 203
  • [49] A component-based approach to hand verification
    Amayeh, Gholamreza
    Bebis, George
    Erol, Ali
    Nicolescu, Mircea
    2007 IEEE CONFERENCE ON COMPUTER VISION AND PATTERN RECOGNITION, VOLS 1-8, 2007, : 3010 - +
  • [50] Formal verification of component-based designs
    Daniel Karlsson
    Petru Eles
    Zebo Peng
    Design Automation for Embedded Systems, 2007, 11 : 49 - 90
12345