Formalizing Software Specifications and Requirements in Higher-Order Logic

这个项目的目标是开发执行大型软件系统的正式规范所需的理论、工具和方法。该方法是使用高阶逻辑（HOL）交互式定理证明系统的扩展来形式化Jackson/Zave （J/Z）规范技术。该项目侧重于HOL的理论和设计问题，以及J/Z方法的方法含义。本研究从编程语言的多态性和模块系统的研究中探索思想，并将其应用于HOL理论。J/Z方法已被用于使用基于一阶模型的方法提供att5ess开关的规格。HOL已被用于大量的硬件和软件规范和验证项目，如Viper芯片和标准元语言（SML）的动态语义。本研究探讨了在HOL中实现J/Z方法为用户级验证提供基础的可能性，更广泛地说，为软件的形式化验证提供基础。该项目作为一个联合学术/工业企业进行，借鉴了宾夕法尼亚大学在逻辑、类型论和语义方面的研究，以及at &amp；T Bell实验室在交互式定理证明、应用软件和规范技术方面的研究。

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.