SHF: Medium: Contract-Based Black-Box Assurance

University Of Minnesota-Twin Cities, Minneapolis MN

Investigators

Abstract

Systems in diverse domains such as transportation, medicine, aviation and space exploration, increasingly rely on third-party components with embedded software. Due to the lack of visibility into the components' implementation and design, traditional techniques for verifying that the components perform as advertised are not feasible; novel alternatives are needed. This research addresses the assurance of such "black-box" components by developing and evaluating (1) techniques to discover and capture contracts - the do's and the don'ts - that the component must satisfy to operate safely in its intended environment, and (2) rigorous metric-driven criteria that can be used to guide as well as to assess the thoroughness of the component testing. The central hypotheses are that (1) novel test coverage adequacy criteria can be defined over the component's contracts as well as its object code; criteria that when satisfied will ensure the level of confidence needed for a critical system, and (2) object-code symbolic execution techniques can be developed for both automatic discovery of component behaviors as well as for verifying conformance to contracts. The expected advances from this research are: (a) new contract definition and discovery techniques suitable for contract-based testing, (b) coverage criteria for contracts and object-code of software, (c) enhanced object-code symbolic execution techniques, and (d) empirical evaluation of the approach on realistic systems. The anticipated broader impacts of this work are that: (a) observations from the empirical studies conducted provide guidance for regulatory agencies and standards organizations in their efforts; (b) commercial tool vendors adopt these techniques in their software development tools and thus help reduce the very high costs of testing critical systems; (c) extensive automation of the costly manual testing processes enabled by these new techniques provide a powerful incentive to formally specify and model requirements, thereby greatly improving quality in all aspects of software development projects; and (d) open-access to tools, case examples, experimental infrastructure, data, and curricular materials developed, advances the state of software engineering research, education and industrial practice.