Using PVS to analyze hierarchical state-based requirements for completeness and consistency

Mats Heimdahl, Barbara J. Czerny

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations

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 languageEnglish (US)
Title of host publicationProceedings of the High-Assurance Systems Engineering Workshop
PublisherIEEE
Pages252-262
Number of pages11
StatePublished - Jan 1 1997
EventProceedings of the 1996 High-Assurance Systems Engineering Workshop - Niagara, Can
Duration: Oct 21 1996Oct 22 1996

Other

OtherProceedings of the 1996 High-Assurance Systems Engineering Workshop
CityNiagara, Can
Period10/21/9610/22/96

Fingerprint Dive into the research topics of 'Using PVS to analyze hierarchical state-based requirements for completeness and consistency'. Together they form a unique fingerprint.

Cite this