A Trustworthy Framework for Resource-Aware Embedded Programming. Barwell, A. D. & Brown, C. In Proceedings of the 31st Symposium on Implementation and Application of Functional Languages, of IFL '19, New York, NY, USA, 2019. Association for Computing Machinery. Paper doi abstract bibtex 2 downloads 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.
@inproceedings{10.1145/3412932.3412944,
title = {A Trustworthy Framework for Resource-Aware Embedded Programming},
author = {Barwell, Adam D. and Brown, Christopher},
year = 2019,
booktitle = {Proceedings of the 31st Symposium on Implementation and Application of Functional Languages},
location = {Singapore, Singapore},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
series = {IFL '19},
doi = {10.1145/3412932.3412944},
isbn = 9781450375627,
url = {https://www.researchgate.net/profile/Christopher-Brown-89/publication/343416568_A_Trustworthy_Framework_for_Resource-Aware_Embedded_Programming/links/5f291a34299bf134049edae9/A-Trustworthy-Framework-for-Resource-Aware-Embedded-Programming.pdf},
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.},
articleno = 12,
numpages = 12,
keywords = {lightweight verification, idris, non-functional properties, dependent types, embedded systems}
}
Downloads: 2
{"_id":"8Zjw5wuGLeyjoXybw","bibbaseid":"barwell-brown-atrustworthyframeworkforresourceawareembeddedprogramming-2019","author_short":["Barwell, A. D.","Brown, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"A Trustworthy Framework for Resource-Aware Embedded Programming","author":[{"propositions":[],"lastnames":["Barwell"],"firstnames":["Adam","D."],"suffixes":[]},{"propositions":[],"lastnames":["Brown"],"firstnames":["Christopher"],"suffixes":[]}],"year":"2019","booktitle":"Proceedings of the 31st Symposium on Implementation and Application of Functional Languages","location":"Singapore, Singapore","publisher":"Association for Computing Machinery","address":"New York, NY, USA","series":"IFL '19","doi":"10.1145/3412932.3412944","isbn":"9781450375627","url":"https://www.researchgate.net/profile/Christopher-Brown-89/publication/343416568_A_Trustworthy_Framework_for_Resource-Aware_Embedded_Programming/links/5f291a34299bf134049edae9/A-Trustworthy-Framework-for-Resource-Aware-Embedded-Programming.pdf","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.","articleno":"12","numpages":"12","keywords":"lightweight verification, idris, non-functional properties, dependent types, embedded systems","bibtex":"@inproceedings{10.1145/3412932.3412944,\r\n title = {A Trustworthy Framework for Resource-Aware Embedded Programming},\r\n author = {Barwell, Adam D. and Brown, Christopher},\r\n year = 2019,\r\n booktitle = {Proceedings of the 31st Symposium on Implementation and Application of Functional Languages},\r\n location = {Singapore, Singapore},\r\n publisher = {Association for Computing Machinery},\r\n address = {New York, NY, USA},\r\n series = {IFL '19},\r\n doi = {10.1145/3412932.3412944},\r\n isbn = 9781450375627,\r\n url = {https://www.researchgate.net/profile/Christopher-Brown-89/publication/343416568_A_Trustworthy_Framework_for_Resource-Aware_Embedded_Programming/links/5f291a34299bf134049edae9/A-Trustworthy-Framework-for-Resource-Aware-Embedded-Programming.pdf},\r\n 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.},\r\n articleno = 12,\r\n numpages = 12,\r\n keywords = {lightweight verification, idris, non-functional properties, dependent types, embedded systems}\r\n}\r\n\r\n","author_short":["Barwell, A. D.","Brown, C."],"key":"10.1145/3412932.3412944","id":"10.1145/3412932.3412944","bibbaseid":"barwell-brown-atrustworthyframeworkforresourceawareembeddedprogramming-2019","role":"author","urls":{"Paper":"https://www.researchgate.net/profile/Christopher-Brown-89/publication/343416568_A_Trustworthy_Framework_for_Resource-Aware_Embedded_Programming/links/5f291a34299bf134049edae9/A-Trustworthy-Framework-for-Resource-Aware-Embedded-Programming.pdf"},"keyword":["lightweight verification","idris","non-functional properties","dependent types","embedded systems"],"metadata":{"authorlinks":{}},"downloads":2,"html":""},"bibtype":"inproceedings","biburl":"https://files.tek.sdu.dk/public/teamplay2020/publications_08-09-2020.bib.txt.txt","dataSources":["oa7at7nJt9iLtdtKv"],"keywords":["lightweight verification","idris","non-functional properties","dependent types","embedded systems"],"search_terms":["trustworthy","framework","resource","aware","embedded","programming","barwell","brown"],"title":"A Trustworthy Framework for Resource-Aware Embedded Programming","year":2019,"downloads":2}