Abstract
Prototype verification system (PVS) is a verification system that provides an interactive environment for writing formal specifications and checking formal proofs. The application of PVS and its theorem proving component for analyzing hierarchical state-based requirements specifications is investigated. Observations shows that the theorem proving component of PVS is powerful and can solve the problems with spurious error reports. The PVS specification environment and theorem prover are relatively easy to use and have many features that provide advantages over other stand-alone theorem provers. For most test cases, PVS performed efficiently and for large test cases, the efficiency of PVS degraded to a point where the proofs could not completed.
| Original language | English (US) |
|---|---|
| Title of host publication | Proceedings of the High-Assurance Systems Engineering Workshop |
| Publisher | IEEE |
| Pages | 252-262 |
| Number of pages | 11 |
| State | Published - Jan 1 1997 |
| Event | Proceedings of the 1996 High-Assurance Systems Engineering Workshop - Niagara, Can Duration: Oct 21 1996 → Oct 22 1996 |
Other
| Other | Proceedings of the 1996 High-Assurance Systems Engineering Workshop |
|---|---|
| City | Niagara, Can |
| Period | 10/21/96 → 10/22/96 |