SoD-HCER: Design for Verification

SoD-HCER：验证设计

• 批准号: 0614002
• 负责人: Tevfik Bultan
• 金额: $ 20万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-08-15 至 2009-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0614002&HistoricalAwards=false
• 关键词: SoD; HCER; Design; 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.

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