The goal of this project is to develop theory, tools, and methods needed to carry out formal specifications of large software systems. The approach is to formalize the Jackson/Zave (J/Z) specification techniques using an extension of the Higher-Order Logic (HOL) interactive theorem-proving system. This project focuses on the theoretical and design issues that this entails for HOL, and the methodological implications for the J/Z approach. The research explores ideas from research on polymorphism and module systems for programming languages, applying them to HOL theories. The J/Z method has been used to provide a specification of the AT&T 5ESS switch using a first-order model-based approach. HOL has been used for substantial hardware and software specification and verification projects such as the Viper Chip and the dynamic semantics of the Standard Meta- Language (SML). This research explores the possibility that realizing the J/Z method within HOL can provide a basis for user level validation and, more generally, for formal verification of software. The project is conducted as a joint academic/industrial enterprise drawing on research in logic, type theory, and semantics at the University of Pennsylvania, and research in interactive theorem proving, application software, and specification techniques at AT&T Bell Labs.
