Change search
ReferencesLink to record
Permanent link

Direct link
Towards Certified Compilation of RTFM-core Applications
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab. (Embedded Systems)
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab. (Embedded Systems)
ISEP, Instituto Superior de Engenharia do Porto.
ISEP, Instituto Superior de Engenharia do Porto.
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)
Abstract [en]

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.
National Category
Embedded Systems
Research subject
Embedded System
Identifiers
URN: 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
Conference
21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016
Available from: 2016-10-14 Created: 2016-10-14 Last updated: 2016-11-10Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Lindgren, PerLindner, Marcus
By organisation
Embedded Internet Systems Lab
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 54 hits
ReferencesLink to record
Permanent link

Direct link