基于TLA的事件圖模型形式化驗(yàn)證方法
2011-12-31 00:00:00夏薇姚益平慕曉冬
計(jì)算機(jī)應(yīng)用研究 2011年11期
0 引言
仿真模型的驗(yàn)證、確認(rèn)和認(rèn)定(VV＆A)方法可以分為非形式化、靜態(tài)、動(dòng)態(tài)和形式化四大類，然而前三類方法只能證明錯(cuò)誤存在，而不能證明錯(cuò)誤不存在。形式化方法是基于嚴(yán)格的數(shù)學(xué)描述與推理的方法，是對(duì)仿真模型進(jìn)行VVA最有效的方法。
