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