| Automated formal specification and verification systems have been developed to aid in the building of highly reliable software. One such system, the Formal Development Methodology (FDM), is particularly well-suited for design specification and verification. FDM has been used in the design and building of computer security systems. Another system, the Gypsy Methodology, is better suited for program specification and verification. Therefore, in reference to the application of computer security, it may be desirable to begin with a design specification written in Ina Jo, the specification language for FDM, and transform it into Gypsy, the specification language for the Gypsy Methodology, in order to facilitate program specification and verification. The purpose of this thesis is to compare the two methodologies and describe a procedure for transforming an Ina Jo top-level design specification into a specification written in Gypsy, and to discuss the problems and feasibility of making such a transformation. |
