Formal specification and verification of air-ticket reservation systems using PVS
Han‐Sol Jun · 2001
Formal methods have been widely used in specification and verification of safetycritical systems.PVS(Prototype Verification Systems) provides an integrated environment for developing and verifying formal specification.In this paper,we use PVS to describe the requirements of air-ticket reservation systems and prove some critical properties of the systems.Some experiences and skills in using PVS are also described.