Skip Navigation

The Computer Journal 2000 43(3):191-205; doi:10.1093/comjnl/43.3.191
© 2000 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (5)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bernardeschi, C.
Right arrow Articles by Simoncini, L.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Formally Verifying Fault Tolerant System Designs

Cinzia Bernardeschi1, Alessandro Fantechi2 and Luca Simoncini1

1 Dipartimento di Ingegneria della Informazione, Universi di Pisa, Via Diotisalvi 2, 56126 Pisa, Italy Email: cinzia@iet.unipi.it 2 Dipartimento di Sistemi e Informatica, Universi di Firenze, via S. Marta 3, 50139 Firenze, Italy

This paper presents an approach for the specification and the verification of the correctness of fault tolerant system designs achieved by the application of fault tolerant techniques. The approach is based on process algebras, equivalence theory and temporal logic. The behaviour of the system in the absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour. The fault tolerant technique is formalized by a context that specifies how replicas of the system cooperate to deal with faults. The system design is proved to behave correctly under a given fault hypothesis by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design. The opportunities given by the expression of the fault hypothesis using temporal logic are discussed. The actual usability of the approach in real case studies is supported by the availability of automatic tools for equivalence checking and for proving the temporal logic properties by model checking.

Received 13 September, 1999. Revised 5 April, 2000.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.