Tahap analisis dan perancangan merupakan tahap yang sangat penting dalam pengembangan sebuah sistem. Kesalahan pada tahap ini akan berdampak pada tahap berikutnya, dan pada akhirnya berdampak pada kegagalan sistem. Spesifikasi yang dibuat menggunakan bahasa alami memiliki banyak kelemahan seperti kontradiktif, rancu, samar, bermakna ganda, dan tidak lengkap. Metode formal yang menggunakan logika formal dan matematika mulai digunakan untuk mengatasi hal ini. Makalah ini menggambarkan beberapa pemakaian metode formal dalam sistem fault tolerance khususnya sistem avionik modular terintegrasi. Kata kunci : metode formal, fault toleran, IMA.