Issue No.02 - February (1987 vol.13)
J.D. Halpern , Department of Government Research and Development, Sytek, Inc.
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.
theorem prover, Formal specification, formal verification, HDM, interactive theorem proving, Muse, National Computer Security Center, software verification, SPECIAL
J.D. Halpern, S. Owre, N. Proctor, W.F. Wilson, "Muse?A Computer Assisted Verification System", IEEE Transactions on Software Engineering, vol.13, no. 2, pp. 151-156, February 1987, doi:10.1109/TSE.1987.226477