Alloy Analyzer, a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.)
Z-Specification/notation, Z is a formal (i.e., mathematical) specification notation used by industry (especially in high-integraity systems) as part of the software (and hardware) development process in both Europe and the US. It has undergone international standardization under ISO/IECJTC1/2 . The use of Z resulted in a UK Queen’s Award for Technological Achievement in 1992 for its use in the IBM CICS project and contributed towards one in 1990 for its use to specify the IEEE Standard for Binary Floating-Point Arithmetic (see Technical Monograph PRG-58)
