SoD-HCER: Design for Verification

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

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.