A formal method for finite relation model based on symbolic logic

Formal methods have been widely used in computer science and being improved day by day. Towards finite relation models, this paper advances a new formal method used by sextuple based on symbolic logic. It can use simple formal normative language to depict the relation between the modules in model exactly. With logical reasoning, it can analyse the models with theorem proving and model checking. In addition, combined with the goal model of case study in urban transportation requirements, this paper expounds the specific application of the new formal methods, and proves that this new formal method can ensure the correctness of the model and avoid the obscure conflict. Compared with Z and VDM, it predefines less data and more functions.