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.　©　2010　IEEE.