Abstract：The mimetic defense system is based on dynamic heterogeneous redundant architecture to improve the security of the system.However，there is a lack of theoretical research on formal verification，analysis and evaluation.In this paper，we first use timed automata as a formal modeling language to describe the processes and mechanisms in the mimetic defense system，such as redundancy，cleaning and decision.Then，based on the model checking tool PAT，we analyze different aspects of the system by using various formal verification methods such as reachability，deadlockfree，model checking based on linear sequential logics and language inclusion checking.Finally，we draw a conclusion about the correctness and effectiveness of the system.
王婷,项露露,陈铁明. 拟态防御系统的时间自动机模型和验证[J]. 小型微型计算机系统, 2020, 41(8): 1718-1724.
WANG Ting,XIANG Lu-lu,CHEN Tie-ming. Time Automata Model and Verification of Mimic Defense System. Journal of Chinese Computer Systems, 2020, 41(8): 1718-1724.
2020, Vol. 41 
