| Autor: |
Halpern, J. Daniel, Owre, Sam, Proctor, Norman, Wilson, William F. |
| Předmět: |
|
| Zdroj: |
IEEE Transactions on Software Engineering; Feb87, Vol. 13 Issue 2, p151-156, 6p, 3 Color Photographs, 3 Diagrams |
| Abstrakt: |
Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HUM). 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 HUM). In particular, it enables one to use the 8DM system to meet the requirements for formal verification in a National Computer Security Center Al 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. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
