Artículo
Simulation relations for fault-tolerance
Fecha de publicación:
11/2017
Editorial:
Springer
Revista:
Formal Aspects Of Computing
ISSN:
0934-5043
e-ISSN:
1433-299X
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
We present a formal characterization of fault-tolerant behaviors of computing systems via simulation relations. This formalization makes use of variations of standard simulation relations in order to compare the executions of a system that exhibits faults with executions where no faults occur; intuitively, the latter can be understood as a specification of the system and the former as a fault-tolerant implementation. By employing variations of standard simulation algorithms, our characterization enables us to algorithmically check fault-tolerance in polynomial time, i.e., to verify that a system behaves in an acceptable way even subject to the occurrence of faults. Furthermore, the use of simulation relations in this setting allows us to distinguish between the different levels of fault-tolerance exhibited by systems during their execution. We prove that each kind of simulation relation preserves a corresponding class of temporal properties expressed in CTL; more precisely, masking fault-tolerance preserves liveness and safety properties, nonmasking fault-tolerance preserves liveness properties, while failsafe fault-tolerance guarantees the preservation of safety properties. We illustrate the suitability of this formal framework through its application to standard examples of fault-tolerance.
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CCT - CORDOBA)
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Citación
Demasi, Ramiro Adrian; Castro, Pablo Francisco; Maibaum, Thomas S. E.; Aguirre, Nazareno Matias; Simulation relations for fault-tolerance; Springer; Formal Aspects Of Computing; 29; 6; 11-2017; 1013-1050
Compartir
Altmétricas