SoD-HCER: Design for Verification

University Of California-Santa Barbara, Santa Barbara CA

Investigators

Abstract

Abstract 0614002 Tevfik Bultan U of Cal SB Design for Verification Developing dependable software is one of the most important challenges in computer science. In recent years, there has been significant progress in verification techniques that automatically find errors in software. However, these techniques are not capable of analyzing large software systems since they are not scalable. The goal of this project is to develop a design for verification approach that enables software developers to document the design decisions that can be useful during verification in order to improve the scalability and applicability of the automated verification techniques. The proposed research will investigate what type of design information is needed for achieving scalable verification and how this information can be transferred from the design phase to the verification phase. This investigation of the interplay between software design and verification will advance the knowledge both in dependability of software systems and in science of design. A set of design patterns that facilitate building software components that are amenable to automated verification will be developed. These design patterns will provide mechanisms for recording the design information that is necessary to achieve scalable verification. The design patterns developed within this project will also be useful tools in teaching how to construct highly dependable software systems to computer science students.