Software Development Environment Supporting Formal Methods

对支持形式化方法的软件工具开发的研究旨在简化并在正确的软件开发过程中提供帮助。使用形式化规范语言来描述问题有助于通过自动推理技术来验证软件的正确性。在早期的工作中，主要研究人员开发了SEED系统，该系统使用形式方法从形式规范中综合出正确的程序。目标是开发工具来支持在软件工程的所有阶段使用形式化方法，包括设计、规范、实现和维护。为了解决复杂和大型系统的正确开发，该项目侧重于使用形式化方法开发面向对象的软件。该项目包括三个部分。首先，开发一个工具，在用户的帮助下将非正式的问题描述分解成正式的规范。接下来，研究图形浏览器的开发，该浏览器将算法应用于形式规范以确定重用。最后，通过开发一个从程序代码中抽象形式规范的工具来解决将形式方法的好处结合到现有代码中的问题。这些工具将被集成到支持正式方法的软件开发环境中，从而促进构建大型、正确的软件系统。

Research into the development of software tools that support formal methods is aimed at simplifying and providing assistance during the development of correct software. Using a formal specification language to describe a problem facilitates the verification of software correctness through automated reasoning techniques. In earlier work, the principal investigator developed the SEED system that used formal methods to synthesize a correct program from a formal specification. The objective is to develop tools to support the use of formal methods in all phases of software engineering including design, specification, implementation, and maintenance. In order to address the correct development of complex and large systems, the project focuses on the development of object-oriented software using formal methods. The project comprises three parts. First, developing a tool that decomposes an informal problem description into formal specifications with user assistance. Next, investigating the development of a graphical browser that applies algorithms to formal specifications to determine reuse. Finally, addressing the issues of incorporating the benefits of formal methods to existing code through the development of a tool that abstracts formal specifications from program code. The tools will be integrated into a software development environment that supports formal methods, thus, facilitating the construction of large, correct software systems.