UT-FMT's colloquium

Abstract

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.

Kuan-Hsun Chen

Assistant Professor of Computer Engineering