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
Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder
KTH. National Institute of Advanced Industrial Science and Technology, Japa.ORCID iD: 0000-0002-3656-1614
2016 (English)In: Proc. 18th Int. Conf. on Formal Engineering Methods (ICFEM 2016), Springer, 2016, Vol. 10009, 417-432 p.Conference paper (Refereed)
Abstract [en]

Scheduling and synchronization algorithms for uniprocessor real-time systems benefit from the rich theory of schedulability analysis, and yet translating these algorithms to practical implementations can be challenging. This paper presents a Java model of the priority inheritance protocol for mutual exclusion, as implemented in the RTEMS open-source real-time operating system. We verified this model using Java Pathfinder to detect potential data races, deadlocks, and priority inversions. JPF detected a known bug in the RTEMS implementation, which we modified along with the Java model. Verification of the modified model showed the absence of data races, deadlocks, and established nine protocol-specific correctness properties.

Place, publisher, year, edition, pages
Springer, 2016. Vol. 10009, 417-432 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743
National Category
Computer Science Software Engineering
Identifiers
URN: urn:nbn:se:kth:diva-199091DOI: 10.1007/978-3-319-47846-3_26ISI: 000390178300026ScopusID: 2-s2.0-84995467513ISBN: 9783319478456 (print)OAI: oai:DiVA.org:kth-199091DiVA: diva2:1062027
Conference
18th Int. Conf. on Formal Engineering Methods (ICFEM 2016)
Note

QC 20170125

Available from: 2017-01-04 Created: 2016-12-28 Last updated: 2017-03-20Bibliographically approved

Open Access in DiVA

The full text will be freely available from 2018-10-15 09:02
Available from 2018-10-15 09:02

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Artho, Cyrille
By organisation
KTH
Computer ScienceSoftware Engineering

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 18 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