Skip to content

Research at St Andrews

A trustworthy framework for resource-aware embedded programming

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

Author(s)

Adam David Barwell, Christopher Mark Brown

School/Research organisations

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)
EditorsJurriën Stutterheim, Wei Ngan Chin
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 201927 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
Country/TerritorySingapore
CitySingapore
Period25/09/1927/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. Proving renaming for Haskell via dependent types: a case-study in refactoring soundness

    Barwell, A. D., Brown, C. M. & Sarkar, S., 18 Jul 2021, 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2021). p. 1-10 10 p.

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

  2. Restoration of legacy parallelism: transforming pthreads into farm and pipeline patterns

    Janjic, V., Brown, C. M. & Barwell, A., 11 Jun 2021, In: International Journal of Parallel Programming. First Online, 25 p.

    Research output: Contribution to journalArticlepeer-review

  3. Programming heterogeneous parallel machines using refactoring and Monte-Carlo tree search

    Brown, C. M., Janjic, V., Goli, M. & McCall, J., Aug 2020, In: International Journal of Parallel Programming. 48, 4, p. 583–602 20 p.

    Research output: Contribution to journalArticlepeer-review

  4. 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, (E-pub ahead of print) In: International Journal of Parallel Programming. First Online, 23 p.

    Research output: Contribution to journalArticlepeer-review

  5. 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 conferencePaperpeer-review

ID: 266448742

Top