| Popis: |
Muse is a verification system which extends the collection of tools developed by SRI 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 SPECIAL specification. In particular, it enables one to use the HDM 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. |
