Contract discovery from black-box components

Vaibhav Sharma; Taejoon Byun; Stephen McCamant; Sanjai Rayadurgam; Mats P.E. Heimdahl

doi:10.1145/3278177.3278179

Contract discovery from black-box components

Vaibhav Sharma, Taejoon Byun, Stephen McCamant, Sanjai Rayadurgam, Mats P.E. Heimdahl

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior - its contract - is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.

Original language	English (US)
Title of host publication	WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018
Editors	Vasant Honavar, Tien N. Nguyen, Gary T. Leavens, Robert Dyer, Hridesh Rajan, Hoan Anh Nguyen
Publisher	Association for Computing Machinery, Inc
Pages	5-8
Number of pages	4
ISBN (Electronic)	9781450360579
DOIs	https://doi.org/10.1145/3278177.3278179
State	Published - Nov 9 2018
Event	1st ACM SIGSOFT International Workshop on Automated Specification Inference, WASPI 2018, Co-located with the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 - Lake Buena Vista, United States Duration: Nov 9 2018 → …

Publication series

Name	WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018

Conference

Conference	1st ACM SIGSOFT International Workshop on Automated Specification Inference, WASPI 2018, Co-located with the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
Country/Territory	United States
City	Lake Buena Vista
Period	11/9/18 → …

Bibliographical note

Funding Information:
This material is based on work supported by the National Science Foundation under Grant Number 1563920.

Publisher Copyright:
© 2018 Association for Computing Machinery.

Keywords

Binary analysis
Contract discovery
Symbolic execution

Access

10.1145/3278177.3278179

OpenUrl availability

Full text

Cite this

Sharma, V., Byun, T., McCamant, S., Rayadurgam, S., & Heimdahl, M. P. E. (2018). Contract discovery from black-box components. In V. Honavar, T. N. Nguyen, G. T. Leavens, R. Dyer, H. Rajan, & H. A. Nguyen (Eds.), WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018 (pp. 5-8). (WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018). Association for Computing Machinery, Inc. https://doi.org/10.1145/3278177.3278179

Contract discovery from black-box components. / Sharma, Vaibhav; Byun, Taejoon; McCamant, Stephen et al.
WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018. ed. / Vasant Honavar; Tien N. Nguyen; Gary T. Leavens; Robert Dyer; Hridesh Rajan; Hoan Anh Nguyen. Association for Computing Machinery, Inc, 2018. p. 5-8 (WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sharma, V, Byun, T, McCamant, S , Rayadurgam, S & Heimdahl, MPE 2018, Contract discovery from black-box components. in V Honavar, TN Nguyen, GT Leavens, R Dyer, H Rajan & HA Nguyen (eds), WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018. WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018, Association for Computing Machinery, Inc, pp. 5-8, 1st ACM SIGSOFT International Workshop on Automated Specification Inference, WASPI 2018, Co-located with the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, Lake Buena Vista, United States, 11/9/18. https://doi.org/10.1145/3278177.3278179

Sharma V, Byun T, McCamant S , Rayadurgam S , Heimdahl MPE. Contract discovery from black-box components. In Honavar V, Nguyen TN, Leavens GT, Dyer R, Rajan H, Nguyen HA, editors, WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018. Association for Computing Machinery, Inc. 2018. p. 5-8. (WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018). doi: 10.1145/3278177.3278179

Sharma, Vaibhav ; Byun, Taejoon ; McCamant, Stephen et al. / Contract discovery from black-box components. WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018. editor / Vasant Honavar ; Tien N. Nguyen ; Gary T. Leavens ; Robert Dyer ; Hridesh Rajan ; Hoan Anh Nguyen. Association for Computing Machinery, Inc, 2018. pp. 5-8 (WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018).

@inproceedings{02efea237f274cba9e375253c9276564,

title = "Contract discovery from black-box components",

abstract = "Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior - its contract - is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.",

keywords = "Binary analysis, Contract discovery, Symbolic execution",

author = "Vaibhav Sharma and Taejoon Byun and Stephen McCamant and Sanjai Rayadurgam and Heimdahl, {Mats P.E.}",

note = "Funding Information: This material is based on work supported by the National Science Foundation under Grant Number 1563920. Publisher Copyright: {\textcopyright} 2018 Association for Computing Machinery.; 1st ACM SIGSOFT International Workshop on Automated Specification Inference, WASPI 2018, Co-located with the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 ; Conference date: 09-11-2018",

year = "2018",

month = nov,

day = "9",

doi = "10.1145/3278177.3278179",

language = "English (US)",

series = "WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018",

publisher = "Association for Computing Machinery, Inc",

pages = "5--8",

editor = "Vasant Honavar and Nguyen, {Tien N.} and Leavens, {Gary T.} and Robert Dyer and Hridesh Rajan and Nguyen, {Hoan Anh}",

booktitle = "WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018",

}

TY - GEN

T1 - Contract discovery from black-box components

AU - Sharma, Vaibhav

AU - Byun, Taejoon

AU - McCamant, Stephen

AU - Rayadurgam, Sanjai

AU - Heimdahl, Mats P.E.

PY - 2018/11/9

Y1 - 2018/11/9

N2 - Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior - its contract - is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.

AB - Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior - its contract - is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.

KW - Binary analysis

KW - Contract discovery

KW - Symbolic execution

UR - http://www.scopus.com/inward/record.url?scp=85061795280&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061795280&partnerID=8YFLogxK

U2 - 10.1145/3278177.3278179

DO - 10.1145/3278177.3278179

M3 - Conference contribution

AN - SCOPUS:85061795280

T3 - WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018

SP - 5

EP - 8

BT - WASPI 2018 - Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference, Co-located with FSE 2018

A2 - Honavar, Vasant

A2 - Nguyen, Tien N.

A2 - Leavens, Gary T.

A2 - Dyer, Robert

A2 - Rajan, Hridesh

A2 - Nguyen, Hoan Anh

PB - Association for Computing Machinery, Inc

T2 - 1st ACM SIGSOFT International Workshop on Automated Specification Inference, WASPI 2018, Co-located with the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018

Y2 - 9 November 2018

ER -

Contract discovery from black-box components

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this