【摘要】 形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属性完成了证明 ,说明了使用PVS系统的某些经验和技巧更多还原

【Abstract】 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.更多还原