Felix C. Gärtner: A survey of transformational approaches to the specification and verification of fault-tolerant systems. Technical Report TUD-BS-1999-04, Department of
Computer Science, Darmstadt University of Technology,
Darmstadt, Germany, April 1999.
Abstract
Proving that a program suits its specification and thus can be
called correct has been a research subject for many years
resulting in a wide range of methods and formalisms. However, it is
a common experience that even systems which have been proven correct
can fail due to physical faults occuring in the system. As computer
programs control an increasing part of todays critical
infrastructure, the notion of correctness has been extended to
fault tolerance, meaning correctness in the presence of a
certain amount of faulty behavior of the environment. Formalisms to
verify fault-tolerant systems must in some form or another model
faults and faulty behavior. Common ways to do this are based on a
notion of transformation either at the program or the
specification level. We survey the wide range of formal methods to
verify fault-tolerant systems which are based on some form of
transformation. Our aim is to structure the area and relate these
methods to one another. Finally we discuss the advantages and
shortcomings of the approaches and state some directions for future
research.
Available as gnuzipped Postscript file.
Felix Gärtner (felix@informatik.tu-darmstadt.de)