原文传递
An elementary tutorial on formal specification and verification using PVS
| 题名： | An elementary tutorial on formal specification and verification using PVS |
| 作者： | Butler, Ricky W. |
| 关键词： | tutorial；specification；element；form；capabilities；development；terminal；operation；prototype；variant |
| 摘要： | A tutorial on the development of a formal specification and its verification using the Prototype Verification System (PVS) is presented. The tutorial presents the formal specification and verification techniques by way of specific example - an airline reservation system. The airline reservation system is modeled as a simple state machine with two basic operations. These operations are shown to preserve a state invariant using the theorem proving capabilities of PVS. The technique of validating a specification via 'putative theorem proving' is also discussed and illustrated in detail. This paper is intended for the novice and assumes only some of the basic concepts of logic. A complete description of user inputs and the PVS output is provided and thus it can be effectively used while one is sitting at a computer terminal. |
| 报告类型： | 科技报告 |
相关文献
- Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations.
- Abstract Model of the SATS Concept of Operations Initial Results and Recommendations
- Hybrid Verification of an Air Traffic Operational Concept
- Tools for Formal Specification, Verification, and Validation of Requirements
- Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request
- Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations.
检索历史
应用推荐
