Formal validation of fault-tolerance mechanisms inside GUARDS

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.