Interfaces and Model Checking for Software

软件的接口和模型检查

• 批准号: 0234690
• 负责人: Luca De Alfaro
• 金额: $ 40万
• 依托单位: University of California-Santa Cruz
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-15 至 2007-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0234690&HistoricalAwards=false
• 关键词: Interfaces; Model; Checking; Software

ABSTRACT0234690Interfaces and Model Checking for SoftwarePI: Luca de AlfaroWhen software is used in critical applications, errors that go undetected in the design phase and occur during actual system operation can have disastrous consequences. The proposed research focuses on the development of techniques for software verification based on the joint use ofmodel-checking and interface theories.Software model-checking constructs and analyzes finite abstractions of the software, refining the abstractions until they can be shown to satisfy a property, or until errors are found in the software.Interface theories permit the specification of the interaction behavior of software components.The proposed research will combine these two techniques into a scalable and compositional approach to software verification, where model-checking is used to analyze individual software components, and interfaces are used to specify and verify the interaction between thecomponents in a design. The approach will be applied to the verification of the NASA MDS testbed.The intellectual merit of the proposed project consists in thedevelopment of a compositional approach to software verification basedon the joint use of methods for single-component andmultiple-component analysis.The broader impact consists in the development of tools and approachesfor the design-time validation of software, thereby increasing bothdependability and quality of software systems.

ABSTRACT0234690软件的接口和模型检查PI：Luca de Alfaro当软件用于关键应用程序时，在设计阶段未检测到的错误以及在实际系统操作期间发生的错误可能会产生灾难性的后果。提出的研究重点是基于模型检测和接口理论的软件验证技术的发展。软件模型检测构造和分析软件的有限抽象，提炼抽象直到它们可以被证明满足某个性质，或者直到发现软件中的错误。接口理论允许对软件组件的交互行为进行规范。该研究将这两种技术结合成一种可扩展的组合软件验证方法，其中模型检测用于分析单个软件组件，接口用于在设计中指定和验证组件之间的交互。该方法将应用于NASA MDS测试台的验证。拟议项目的智力优势在于开发了一种基于单组件和多组件分析方法的组合软件验证方法。其更广泛的影响在于开发了软件设计时验证的工具和方法，从而提高了软件系统的可靠性和质量。