Анализируются существующие проблемы и возможность применения формальных методов при разработке отказоустойчивых компьютерных систем. Рассматривается интеграция формального метода разработки Event-B и метода анализа надежности FME(C)A для выявления возможных отказов, оценки их критичности, а также оптимального выбора и формального доказательства корректности средств восстановления и обеспечения отказоустойчивости. Предложена процедура перехода от Event-B модели корректной системы к Event-B модели корректной отказоустойчивой системы.