Formalizing Software Specifications and Requirements in Higher-Order Logic

点击翻译按钮获取中文摘要

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.