Model checking fault tolerant systems

被引：30
作者：
Bernardeschi, C
Fantechi, A
Gnesi, S
机构：
[1] Univ Pisa, Dipartimento Ingn Informaz, I-56126 Pisa, Italy
[2] Univ Florence, Dipartimento Sistemi & Informat, I-50139 Florence, Italy
[3] CNR, IEI, I-56124 Pisa, Italy
来源：
SOFTWARE TESTING VERIFICATION & RELIABILITY | 2002年 / 12卷 / 04期
关键词：
formal methods; fault tolerance; model checking; verification;
D O I：
10.1002/stvr.258
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper proposes a modelling approach suitable for formalizing fault tolerant systems, taking into account different fault scenarios. Verification of the properties of such systems is then performed using model checking. A general framework for the formal specification and verification of fault tolerant systems is defined starting from these principles, and experience with its application to two case studies is then presented. Copyright (C) 2002 John Wiley Sons, Ltd.
引用
收藏
页码：251 / 275
页数：25
相关论文
共 41 条
  • [1] [Anonymous], LNCS
  • [2] [Anonymous], 1997, DISTRIBUTED SYSTEMS
  • [3] [Anonymous], 1992, DEPENDABILITY BASIC
  • [4] ALGEBRA OF PROCESSES AND SYNCHRONIZATION
    AUSTRY, D
    BOUDOL, G
    [J]. THEORETICAL COMPUTER SCIENCE, 1984, 30 (01) : 91 - 131
  • [5] A formal verification environment for railway signaling system design
    Bernardeschi, C
    Fantechi, A
    Gnesi, S
    Larosa, S
    Mongardi, G
    Romano, D
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1998, 12 (02) : 139 - 161
  • [6] Bernardeschi C, 1999, LECT NOTES COMPUT SC, V1698, P420
  • [7] Formally verifying fault tolerant system designs
    Bernardeschi, C
    Fantechi, A
    Simoncini, L
    [J]. COMPUTER JOURNAL, 2000, 43 (03) : 191 - 205
  • [8] INTRODUCTION TO THE ISO SPECIFICATION LANGUAGE LOTOS
    BOLOGNESI, T
    BRINKSMA, E
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1987, 14 (01): : 25 - 59
  • [9] Bouali A., 1994, Bulletin of the European Association for Theoretical Computer Science, P207
  • [10] BRUNS G, 1997, LNCS, V1349, P45
12345