Up to now

the Dynamic Heterogeneous Redundancy (DHR) structure is a kind of important engineering model about the Mimic Defense (MD) technique. However

there is still a lack of way of formal analysis for DHR structures as there is no formal model available for a DHR structure. To address this problem

we use a Finite State Automaton (FSA) and its Parallel Automaton (PA) to establish a computing model for some attacks and mimic defenses. First

each FSA is employed to model each execution body

while there are a number of execution bodies in a DHR structure. Second

these FSAs are combined in parallel to model the combination of execution bodies. Third

one can get a model of MD automaton which can describe the attacks and MD actions

by modifying the state transition rules. Finally

one can analyse the attacks and MD actions on a DHR structure

according to the conditions of the PA states. Furthermore

we use an Alternating Finite Automaton (AFA) to model some attacks and MD actions. As a result

the automatic MD analysis problem is reduced to the solved AFA model checking problem.