Verification of the legOS scheduler using Uppaal. This article concentrates on the scheduler in the operating system legOS. LegOS is an open source embedded operating system for the Lego Mindstorms® system. The scheduler in legOS practices starvation of lower priority threads. In this article the validity of starvation problems is proven through tests of the scheduler and through an Uppaal model of the scheduler wherein the starvation is verified. A new scheduler is designed and modeled in Uppaal. This Uppaal model is used to verify that starvation is no longer a problem in the new design. The new design is implemented in a new scheduler and tests are performed to show that the problem with starvation is no longer present.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element