Muse—A Computer Assisted Verification System
| Autor: | Norman Proctor, William F. Wilson, Sam Owre, J.D. Halpern |
|---|---|
| Rok vydání: | 1987 |
| Předmět: |
Soundness
Finite-state machine Programming language business.industry Computer science Proof assistant Specification language computer.software_genre Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Formal specification Formal language Software engineering business computer Formal verification Software Software verification |
| Zdroj: | IEEE Transactions on Software Engineering. :151-156 |
| ISSN: | 0098-5589 |
| DOI: | 10.1109/tse.1987.226477 |
| Popis: | Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a specification written in SPECIAL (the specification language of HDM). In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center A1 evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process. In concept, it is open-ended. We introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|