Application Of Linear Temporal Logic On Audit Of Unemployment Insurance

In the course of social insurance audit, it is of great importance to understand d the laws and business processes of the audited area for they are the basis of business processing. Building business model according to the regulations and policies is a effective method. Now, there are lots of ways for model checking. Linear temporal logic has been widely concerned, and has been applied to model checking.In this thesis, the business workflow is built according to the regulations and policies in the form of text. According to the different time when a business happens, business processing model is simplified and improved to get an accurate model to describe the unemployment insurance business. After the building of unemployment insurance business processing model based-on automaton, according to the description of temporal logic, linear temporal logic language is applied to write program, which will be a part of input of model checking. This paper extracts regulations and policies on unemployment insurance for they will be the standard of the model checking of unemployment insurance. and then the inear temporal logic language of the regulations and policies will be transformed into linear temporal logic program which will be a part of the model checking input. As input conditions, the above-mentioned two programs are used to check the correctness of unemployment insurance business model, to achieve the purpose of analyzing and completing the model of unemployment insurance.Finally, the sequential nature of the model is described with LTL. NuSMV is used to check the built model according to the linear temporal logic formulas described with the LTL grammar, which can avoid disagreement on doubtful point generated by audit staff and social security staff and guide the generation of audit approach.