Dept. of Information
Technologies
Åbo Akademi University
Wednesday, 2 December 2009, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
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.