Type-driven verification of non-functional properties

Christopher Mark Brown; Adam David Barwell; Yoann Marquer; Celine Minh; Olivier Zendra

doi:10.1145/3354166.3354171

Type-driven verification of non-functional properties

Christopher Mark Brown, Adam David Barwell, Yoann Marquer, Celine Minh, Olivier Zendra

School of Computer Science

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

Abstract

Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification frame-work, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

Original language	English
Title of host publication	Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19)
Place of Publication	New York
Publisher	ACM
Pages	1-15
Number of pages	15
ISBN (Electronic)	9781450372497
DOIs	https://doi.org/10.1145/3354166.3354171
Publication status	Published - 7 Oct 2019
Event	21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019) - Porto, Portugal Duration: 7 Oct 2019 → 9 Oct 2019 Conference number: 21 http://ppdp2019.macs.hw.ac.uk/

Conference

Conference	21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)
Abbreviated title	PPDP 2019
Country/Territory	Portugal
City	Porto
Period	7/10/19 → 9/10/19
Internet address	http://ppdp2019.macs.hw.ac.uk/

Keywords

IDRIS
C
Time
Energy
Security
Non-functional properties
Proofs
Verification
Contracts

Access to Document

10.1145/3354166.3354171

icfp2019
© 2019, Association for Computing Machinery. This work has been made available online in accordance with the publisher's policies. This is the author created accepted version manuscript following peer review and as such may differ slightly from the final published version. The final published version of this work is available at https://doi.org/10.1145/3354166.3354171
Accepted author manuscript, 605 KB

TeamPlay: H2020 ICT-5 Teamplay
Brown, C. M. (PI)
European Commission
1/01/18 → 31/12/20
Project: Standard
Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems
Thomson, J. D. (PI), Hammond, K. (CoI) & Sarkar, S. (CoI)
EPSRC
1/07/17 → 31/12/20
Project: Standard

Cite this

@inproceedings{4ea5563abf8444b6a0ae67df7d232117,

title = "Type-driven verification of non-functional properties",

abstract = "Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification frame-work, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.",

keywords = "IDRIS, C, Time, Energy, Security, Non-functional properties, Proofs, Verification, Contracts",

author = "Brown, {Christopher Mark} and Barwell, {Adam David} and Yoann Marquer and Celine Minh and Olivier Zendra",

note = "Funding: This work was supported by the EU Horizon 2020 project, Team-Play (https://www.teamplay-h2020.eu), grant number 779882, and UK EPSRC Discovery, grant number EP/P020631/1.; 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), PPDP 2019 ; Conference date: 07-10-2019 Through 09-10-2019",

year = "2019",

month = oct,

day = "7",

doi = "10.1145/3354166.3354171",

language = "English",

pages = "1--15",

booktitle = "Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19)",

publisher = "ACM",

address = "United States",

url = "http://ppdp2019.macs.hw.ac.uk/",

}

Brown, CM , Barwell, AD, Marquer, Y, Minh, C & Zendra, O 2019, Type-driven verification of non-functional properties. in Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19)., 6, ACM, New York, pp. 1-15, 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), Porto, Portugal, 7/10/19. https://doi.org/10.1145/3354166.3354171

TY - GEN

T1 - Type-driven verification of non-functional properties

AU - Brown, Christopher Mark

AU - Barwell, Adam David

AU - Marquer, Yoann

AU - Minh, Celine

AU - Zendra, Olivier

N1 - Conference code: 21

PY - 2019/10/7

Y1 - 2019/10/7

N2 - Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification frame-work, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

AB - Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification frame-work, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

KW - IDRIS

KW - C

KW - Time

KW - Energy

KW - Security

KW - Non-functional properties

KW - Proofs

KW - Verification

KW - Contracts

U2 - 10.1145/3354166.3354171

DO - 10.1145/3354166.3354171

M3 - Conference contribution

SP - 1

EP - 15

BT - Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19)

PB - ACM

CY - New York

T2 - 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)

Y2 - 7 October 2019 through 9 October 2019

ER -

Type-driven verification of non-functional properties

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

TeamPlay: H2020 ICT-5 Teamplay

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems

Cite this