基于TLA的事件圖模型形式化驗證方法

0 引言

仿真模型的驗證、確認和認定(VV＆A)方法可以分為非形式化、靜態、動態和形式化四大類，然而前三類方法只能證明錯誤存在，而不能證明錯誤不存在。形式化方法是基于嚴格的數學描述與推理的方法，是對仿真模型進行VVA最有效的方法。