摘要：動(dòng)態(tài)異構(gòu)冗余結(jié)構(gòu)是擬態(tài)防御技術(shù)的常用工程模型.然而,目前尚缺乏對(duì)該結(jié)構(gòu)實(shí)施形式化分析的手段,因?yàn)樵摻Y(jié)構(gòu)缺乏形式化建模方法.針對(duì)此問題,使用有窮狀態(tài)自動(dòng)機(jī)及其并行組合自動(dòng)機(jī)為一些擬態(tài)攻防行為建立計(jì)算模型.首先,使用單個(gè)有窮狀態(tài)自動(dòng)機(jī)為單個(gè)執(zhí)行體建模;其次,使用有窮狀態(tài)自動(dòng)機(jī)的并行組合為執(zhí)行體組合建模;再次,修改狀態(tài)遷移規(guī)則,得到可描述攻防行為的擬態(tài)防御自動(dòng)機(jī)模型;最后,根據(jù)該自動(dòng)機(jī)模型的狀態(tài)條件,分析動(dòng)態(tài)異構(gòu)冗余結(jié)構(gòu)上擬態(tài)攻防行為的安全性.此外,也可使用交替自動(dòng)機(jī)為擬態(tài)攻防建模,并把安全性自動(dòng)分析規(guī)約為交替自動(dòng)機(jī)模型檢測(cè)問題.