Loading...
Please wait, while we are loading the content...
Similar Documents
An elementary tutorial on formal specification and verification using pvs
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Butler, Ricky W. |
| Copyright Year | 1993 |
| Description | 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. |
| File Size | 2456178 |
| Page Count | 74 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19940011063 |
| Archival Resource Key | ark:/13960/t9d55jv0f |
| Language | English |
| Publisher Date | 1993-09-01 |
| Access Restriction | Open |
| Subject Keyword | Data Base Management Systems Airline Operations Theorem Proving Data Bases Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
