Skip to content

Research at St Andrews

A trustworthy framework for resource-aware embedded programming

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

Abstract

Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.
Close

Details

Original languageEnglish
Title of host publicationProceedings of International Symposium on Implementation and Application of Functional Languages (IFL'19)
PublisherACM
DOIs
Publication statusAccepted/In press - 11 Feb 2020
EventThe 31st symposium on Implementation and Application of Functional Languages (IFL 2019) - Singapore, Singapore
Duration: 25 Sep 201527 Sep 2019
Conference number: 31
http://2019.iflconference.org

Conference

ConferenceThe 31st symposium on Implementation and Application of Functional Languages (IFL 2019)
Abbreviated titleIFL 2019
CountrySingapore
CitySingapore
Period25/09/1527/09/19
Internet address

    Research areas

  • Dependent types, Idris, LIghtweight verification, Non-functional properties, Abstract interpretation, Proof-carrying code, Embedded systems

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Refactoring GrPPI: generic refactoring for generic parallelism in C++

    Brown, C. M., Janjic, V., Barwell, A. D., Garcia, J. D. & MacKenzie, K., 10 Jul 2020, In : International Journal of Parallel Programming. First Online, 23 p.

    Research output: Contribution to journalArticle

  2. Restoration of legacy parallelism in C and C++ applications

    Brown, C. M., Barwell, A. D. & Janjic, V., 1 Jul 2020, (Accepted/In press).

    Research output: Contribution to conferencePaper

  3. A hybrid approach to parallel pattern discovery in C++

    Brown, C. M., Janjic, V., Barwell, A. D., Thomson, J. D., Castañeda Lozano, R., Cole, M., Franke, B., Garcia-Sanchez, J. D., Del Rio Astorga, D. & MacKenzie, K., 14 May 2020, 2020 28th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP). IEEE Computer Society, 5 p. 9092377. (Proceedings - Euromicro Workshop on Parallel and Distributed Processing).

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

  4. Reasoning about non-functional properties using compiler intrinsic function annotations

    Jadhav, S., Roth, M., Falk, H., Brown, C. M. & Barwell, A. D., 6 Nov 2019, Proceedings of the 13th Junior Researcher Workshop on Real-Time Computing. INP ENSEEIHT/IRIT, p. 25-28 4 p.

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

  5. Type-driven verification of non-functional properties

    Brown, C. M., Barwell, A. D., Marquer, Y., Minh, C. & Zendra, O., 7 Oct 2019, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19). New York: ACM, p. 1-15 15 p. 6

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

ID: 266448742

Top