在社会保险审计的过程中,理解被审计地区的法规和业务流程是非常重要的环节。各地的法规政策是开展业务的基础,根据法规政策来构建当地的业务模型也是理解业务的有效手段。目前,模型检测的方法很多,线性时序逻辑已经受到广泛的关注,并且已经应用到模型检测中。本文根据法规政策的文本描述,构建当地的业务工作流程。依据时间序列上业务事件发生的时间不同,对构建的业务模型进行化简、完备失业保险业务处理流程模型等操作。基于有限状态自动机的失业保险业务处理流程模型构建完毕后,应用线性时序逻辑对模型的时序性质加以描述,针对该时序描述,应用线性时序逻辑语言编写程序,程序作为模型检测输入的一部分。本文提取失业保险法规政策的约束条件,作为失业保险业务模型检测的标准,再将法规的线性时序逻辑语言描述转换成线性时序逻辑程序,这部分程序作为模型检测输入的约束条件。以上两部分程序作为输入条件来检测失业保险业务模型的正确性。本文利用线性时序逻辑来描述失业保险业务处理流程模型的时序性质。根据线性时序逻辑语法规则描述的线性时序逻辑公式,应用NuSMV来检测构建的模型。避免审计人员和社保人员对生成疑点的意见和看法的不一致,指导审计方法的生成。