Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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)ORCID iD: 0000-0002-1791-535X
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, 2016, 7733551Conference 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. 7733551
Series
I E E E International Conference on Emerging Technologies and Factory Automation. Proceedings, ISSN 1946-0740
National Category
Embedded Systems
Research subject
Embedded System
Identifiers
URN: urn:nbn:se:ltu:diva-59753DOI: 10.1109/ETFA.2016.7733551ISI: 000389524200058ScopusID: 2-s2.0-84996490222ISBN: 978-1-5090-1314-2 (print)ISBN: 978-1-5090-1313-5 (print)OAI: 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: 2017-02-21Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

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: 83 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf