Towards Certified Compilation of RTFM-core Applications
Number of Authors: 4
2016 (English)In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016, Piscataway, NJ: IEEE conference proceedings, 2016Conference paper (Refereed)
Concurrent programming is dominated by threadbased solutions with lock based critical sections. Careful attentionhas to be paid to avoid race and deadlock conditions. Real-Timefor The Masses (RTFM) takes an alternative language approach,introducing tasks and named critical sections (via resources)natively in the RTFM-core language. RTFM-core programs canbe compiled to native C-code, and efficiently executed ontosingle-core platforms under the Stack Resource Policy (SRP)by the RTFM-kernel. In this paper we formally define thewell-formedness criteria for SRP based resource management,and develop a certified (formally proven) implementation ofthe corresponding compilation from nested critical sections ofthe input RTFM-core program to a resulting flat sequence ofprimitive operations and scheduling primitives. Moreover weformalise the properties for resource ceilings under SRP anddevelop a certified algorithm for their computation.The feasibility of the described approach is shown throughthe adoption of the Why3 platform, which allows the necessaryverification conditions to be automatically generated and dischargedthrough a variety of automatic external SMT-solversand interactive theorem provers. Moreover, Why3 supports theextraction of certified Ocaml code for proven implementationsin WhyML. As a proof of concept the certified extracteddevelopment is demonstrated on an example system.
Place, publisher, year, edition, pages
Piscataway, NJ: IEEE conference proceedings, 2016.
Research subject Embedded System
IdentifiersURN: urn:nbn:se:ltu:diva-59753DOI: 10.1109/ETFA.2016.7733551ISBN: 978-1-5090-1314-2ISBN: 978-1-5090-1313-5OAI: oai:DiVA.org:ltu-59753DiVA: diva2:1037270
21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016