Mining interface specifications for generating checkable robustness properties

Mithun Acharya, Tao Xie, Jun Xu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A software system interacts with its environment through interfaces. Improper handling of exceptional returns from system interfaces can cause robustness problems. Robustness of software systems are governed by various temporal properties related to interfaces. Static verification has been shown to be effective in checking these temporal properties. But manually specifying these properties is cumbersome and requires the knowledge of interface specifications, which are often either unavailable or undocumented. In this paper, we propose a novel framework to automatically infer system-specific interface specifications from program source code. We use a model checker to generate traces related to the interfaces. From these model checking traces, we infer interface specification details such as return value on success or failure. Based on these inferred specifications, we translate generically specified interface robustness rules to concrete robustness properties verifiable by static checking. Hence the generic rules can be specified at an abstract level that needs no knowledge of the source code, system, or interfaces. We implement our framework for an existing static analyzer that employs push down model checking and apply the analyzer to the well known POSIX-API system interfaces. We found 28 robustness violations in 10 open source packages using our framework.

Original languageEnglish (US)
Title of host publicationProceedings - 17th International Symposium on Software Reliability Engineering, ISSRE 2006
Pages311-320
Number of pages10
DOIs
StatePublished - 2006
Externally publishedYes
Event17th International Symposium on Software Reliability Engineering, ISSRE 2006 - Raleigh, NC, United States
Duration: Nov 7 2006Nov 10 2006

Publication series

NameProceedings - International Symposium on Software Reliability Engineering, ISSRE
ISSN (Print)1071-9458

Other

Other17th International Symposium on Software Reliability Engineering, ISSRE 2006
Country/TerritoryUnited States
CityRaleigh, NC
Period11/7/0611/10/06

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint

Dive into the research topics of 'Mining interface specifications for generating checkable robustness properties'. Together they form a unique fingerprint.

Cite this