In this paper we report the experiments carried out during the specificatio
n and validation of the fault-tolerance mechanisms developed in the Europea
n project Generic Upgradable Architecture for Real-time Dependable Systems
(GUARDS). These mechanisms are the components of an architecture developed
for embedded safety-critical systems. The validation approach is based on m
odel-checking techniques and exploits the verification methodology supporte
d by the Just Another Concurrency Kit (JACK) environment. The properties th
at guarantee the desired behaviour of the mechanisms are specified as tempo
ral logic formulae; the JACK model-checker is then used to verify that the
behaviour of the mechanisms satisfy such properties also in the presence of
faults. (C) 2001 Elsevier Science Ltd. All rights reserved.