%0 Journal Article
%T 基于协议验证的时间自动机取证模型
%J 南京邮电大学学报(自然科学版)
%D 2016
%X 如何确保计算机获取的证据真实可靠，成为法院上可供参考的法律依据，这是一个迫切需要解决的问题。因此，需要一种形式化描述方法使得数字取证调查具有可靠性和可信性。文中提出一种基于协议验证的TA（时间自动机）形式化描述方法，利用取证工具获得具有时间属性的行为数据，并用TA描述计算机取证的动态事件重构行为，通过UPPAAL工具进行需求分析和验证来达到取证的目的。
%K 时间自动机 取证模型 动态行为 形式化方法
%U http://nyzr.njupt.edu.cn/ch/reader/view_abstract.aspx?file_no=201606017&flag=1