Paper Info
Title
Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder.
Abstract
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.
Year
DOI
Venue
2016
10.1007/978-3-319-47846-3_26
Lecture Notes in Computer Science
Keywords
Field
DocType
Java Pathfinder,RTEMS,Priority inheritance
Uniprocessor system,Computer science,Lock (computer science),Correctness,Deadlock,Real-time computing,Priority inheritance,Java,Mutual exclusion,RTEMS,Operating system
Conference
Volume
ISSN
Citations 
10009
0302-9743
1
PageRank 
References 
Authors
0.35
6
3
Name
Order
Citations
PageRank
Saurabh Gadia110.35
Cyrille Artho258844.46
Gedare Bloom36813.95