基于PVS的飞机订票系统的形式化描述与验证  

Formal specification and verification of air-ticket reservation systems using PVS

作　　者：杨红丽[1] 刘建元[1] 韩俊刚[1] 

机构地区：[1]西安邮电学院计算机系,陕西西安710061

出　　处：《西安邮电学院学报》2001年第3期1-5,共5页Journal of Xi'an Institute of Posts and Telecommunications

基　　金：国家 8 6 3资助项目

摘　　要：形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属性完成了证明 。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.

关 键 词：PVS 形式化规范 形式化证明 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]