Interfaces and Model Checking for Software

University Of California-Santa Cruz, Santa Cruz CA

Investigators

Abstract

ABSTRACT 0234690 Interfaces and Model Checking for Software PI: Luca de Alfaro When 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 of model-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 the components 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 the development of a compositional approach to software verification based on the joint use of methods for single-component and multiple-component analysis. The broader impact consists in the development of tools and approaches for the design-time validation of software, thereby increasing both dependability and quality of software systems.