Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
RAUK: Automatic Schedulability Analysis of RTIC Applications Using Symbolic Execution
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering.
2022 (English)Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

In this thesis, the proof-of-concept tool RAUK for automatically analyzing RTIC applications for schedulability using symbolic execution is presented. The RTIC framework provides a declarative executable model for building embedded applications, which behavior is based on established formal methods and policies. Because of this, RTIC applications are amenable for both worst-case execution time (WCET) and scheduling analysis techniques. Internally, RAUK utilizes the symbolic execution tool KLEE to generate test vectors covering all feasible execution paths in all user tasks in the RTIC application. Since KLEE also checks for possible program errors e.g. arithmetic or array indexing errors, it can be used via RAUK to verify the robustness of the application in terms of program errors. The test vectors are replayed on the target hardware to record a WCET estimation for all user tasks. These WCET measurements are used to derive a worst-case response time (WCRT) for each user task, which in turn is used to determine if the system is schedulable using formal scheduling analysis techniques. The evaluation of this tool shows a good correlation between the results from RAUK and manual measurements of the same tasks, which showcases the viability of this approach. However, the current implementation can add some substantial overhead to the measurements, and sometimes certain types of paths in the application can be completely absent from the analysis. The work in this thesis is based on previous research in this field for WCET estimation using KLEE on an older iteration of the RTIC framework. Our contributions include a focus on an RTIC 1.0 pre-release, a seamless integration with the Rust ecosystem, minimal changes required to the application itself, as well as an included automatic schedulability analyzer. Currently, RAUK can verify simple RTIC applications for both program errors and schedulability with minimal changes to the application source code. The groundwork is laid out for further improvements that are required to function on larger and more complex applications. Solutions for known problems and future work are discussed in Chapters 6, 7 respectively.

Place, publisher, year, edition, pages
2022. , p. 43
Keywords [en]
RTIC, symbolic execution, embedded systems, software verification, software analysis, schedulability
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:ltu:diva-90211OAI: oai:DiVA.org:ltu-90211DiVA, id: diva2:1652205
Educational program
Computer Science and Engineering, master's level
Supervisors
Examiners
Available from: 2022-04-19 Created: 2022-04-16 Last updated: 2022-11-11Bibliographically approved

Open Access in DiVA

fulltext(1060 kB)280 downloads
File information
File name FULLTEXT01.pdfFile size 1060 kBChecksum SHA-512
442018d8ebafe214af966eb40855f03b0ed72a975b5ad76e3aff0b3827d16ed5c7ec8a4d2f4aa92e11f1e93ece5f452dceeec7baad51268dc700ff81bfd8c018
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Håkansson, Mark
By organisation
Department of Computer Science, Electrical and Space Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 280 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 652 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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