Verification of Real-Time Systems using Statistical Model Checking

Software for airborne systems have become more and more complex, yet the need to verify correct behavior remains constant. Adding to the challenge is the fact that these systems operate in uncertain environments where the workload they must process may not be known in advance. Statistical model checking is one tool that has been shown to be useful in verification of large complex systems operating under uncertainty. One challenge area for software validation in UAS systems is the evaluation of the performance of task scheduling policies. In this paper, we apply statistical model checking to characterize the timing behavior of a system using zero-slack rate-monotonic scheduler. We compare this to the timing behavior of traditional rate-monotonic scheduling. We show that task deadline requirements can impact the relative performance of the two scheduling policies.