Verification of time partitioning in the DEOS scheduler kernel

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. To conduct the experiment, a core slice of the DEOS scheduling kernel was anslated without abstraction from C++ into Promela ut language for Spin). We constructed an abstract "test-driver" environment and carefully introduced several ions into the system to support verification. Several experiments were run to attempt to verify that the system implementation adhered to the critical time partitioning requirements. During these experiments, the known error was rediscovered in the time partitioning implementation. We believe this case study provides several insights into how to develop cost-effective ...

• Type: Conference
• Year: 2000
• Where: ICSE
• Authors: John Penix, Willem Visser, Eric Engstrom, Aaron Larson, Nicholas Weininger
• Keywords: ICSE 2000, Model Checking, Scheduling Kernel, Software Engineering, Subtle Implementation Error