Verification of Resource Sharing Protocol Implementations -- A Case Study in RTEMS


To avoid race conditions and ensure data integrity, resource sharing protocols have been widely studied in real-time systems for decades. However, the corresponding realization is often based on assumed abstractions and necessary adaptions in each real-time operating system. The theoretically proven properties of such a protocol may not be delivered properly, leading to serious mismatches. This talk will go through our experience in verifying official implementation of the immediate ceiling priority protocol (ICPP) and the multiprocessor resource sharing protocol (MrsP) in RTEMS, resulting in the discovery of long-stayed mismatches.

Apr 12, 2023 9:00 AM — 10:00 AM
Carré 3F, UTwente
Kuan-Hsun Chen
Kuan-Hsun Chen
Assistant Professor

As a computer scientist, I make embedded systems future-proof and future-ready.