Refinement of fault tolerant control systems in B

Abstract

Application of formal methods helps us to gain confidence in building correct software. On the other hand, to guarantee dependability of the overall system we need to build fault tolerant software, i.e., software which is not only fault-free but also is able to cope with faults of other system components. Obviously, this goal is attainable only if fault tolerance mechanisms constitute an intrinsic part of software behaviour. In this paper we propose a formal approach to model-driven development of fault tolerant control systems. We demonstrate how to integrate fault tolerance into the automated refinement process in the B method. The proposed approach is exemplified by a case study - a derivation of safe and fault tolerant controller of a heating system. © Springer-Verlag 2004.