Software Development Environment Supporting Formal Methods

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

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.