Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings

Abstract

We present an algebraic approach to the model checking of fault-tolerant systems. Fault models and fault-handling mechanisms are modelled using special-purpose process operators. Besides providing for natural models, special-purpose operators allow systems with large state spaces to be verified using systems with small state spaces. To support this verification technique we show that a kind of simulation relation on processes preserves all process operators in tyft/tyxt format.