Предложен метод, который позволяет объединить метод анализа деревьев отказов (FTA) и формальную спецификацию в Event-B. Использование методики формальной разработки гарантирует корректность внедрения требований по функциональной безопасности в спецификацию систем критического применения. Предложенный подход основан на пошаговом внедрении результатов анализа по принципу "сверху вниз" на каждом этапе детализации спецификации, начиная с абстрактной и заканчивая реализацией. В статье также приведены измененные модели жизненного цикла разработки программного обеспечения информационно-управляющих систем в соответствии с предлагаемым методом. В качестве примера внедрения FTA в формальную спецификацию была использована противообледенительная система самолета АН-140М. Ключевые слова: методы формальной спецификации и верификации, Event-B, функциональная безопасность, FTA.
