SoD-HCER: Design for Verification

开发可靠的软件是计算机科学中最重要的挑战之一。近年来，在自动发现软件错误的验证技术方面取得了重大进展。然而，这些技术不能分析大型软件系统，因为它们是不可扩展的。本研究的目的是开发一种可验证的设计方法，使软件开发人员能够记录在验证过程中可能有用的设计决策，以提高自动化验证技术的可扩展性和适用性。拟议的研究将探讨实现可扩展验证所需的设计信息类型，以及如何将这些信息从设计阶段转移到自动化验证阶段。验证阶段。通过对软件设计与验证之间相互作用的研究，将促进对软件系统可靠性和设计科学的认识，并将开发一套有助于构建可自动验证的软件组件的设计模式。这些设计模式将提供记录设计信息的机制，这些设计信息是实现可扩展验证所必需的。在这个项目中开发的设计模式也将是有用的工具，在教学中如何构建高度可靠的软件系统，计算机科学的学生。

Abstract0614002Tevfik BultanU of Cal SBDesign for VerificationDeveloping 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.