摘要：IF是一個對異步實時系統(tǒng)建模和驗證的開放環(huán)境，建立在具有豐富表達能力，基于時間自動機的中間語言IF符號集之上。文章描述了IF的組成，包括其體系結(jié)構(gòu)，所使用的符號集；然后給出了IF對實時系統(tǒng)驗證的方法，并運用此驗證方法對一個實時系統(tǒng)實例進行了驗證。

關(guān)鍵詞：IF；異步實時系統(tǒng)；時間自動機；實時系統(tǒng)驗證