Design Verification of BJUT Library Management System with PVS

Formal methods are effective in improving the safety and reliability during the development of software. PVS (Prototype Verification System) provides an integrated environment for development and analysis of formal specifications. It consists of a higher order logical specification language integrated with support tools and a powerful theorem prover. In this paper, we specify and verify the design of the library management system of Beijing University of Technology (BJUT) using PVS. Firstly, we describe the requirements of the system and give its Entity Relationship (E-R) model, then design the formal specification of the E-R model and database operations based on the requirement analysis. Some properties essential to the correctness of the system are also given as axioms. Finally, we verify the design by proving some critical properties according to the specifications. In addition, some experiences and skills in using PVS are also described.